Uniform-time spatial bounds for the actual mean velocity #
The continuous velocity is reconstructed from its actual L² value and actual L² time derivative. Terminal-primitive uniqueness identifies this path with the physical velocity already constructed by the strong mean inverse.
noncomputable def
EulerMeanVariationalInverse.StrongMeanEvolution.continuousVelocity
{T : ℝ}
{hT : 0 ≤ T}
{FInv F F₁ : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)}
{A : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2}
{L : ℝ}
{u f : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)}
(s : StrongMeanEvolution T hT FInv F F₁ A L u f)
:
The continuous time path constructed from the actual B and B_t.
Equations
Instances For
theorem
EulerMeanVariationalInverse.StrongMeanEvolution.continuousVelocity_eq_physicalPath
{T : ℝ}
{hT : 0 ≤ T}
{FInv F F₁ : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)}
{A : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2}
{L : ℝ}
{u f : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)}
(s : StrongMeanEvolution T hT FInv F F₁ A L u f)
(hTpos : 0 < T)
(hF : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT F) (F₁ t) (Set.Icc 0 T) ↑t)
(t : ↑(Set.Icc 0 T))
:
This reconstruction is exactly the physical representative, at every time.
theorem
EulerMeanVariationalInverse.StrongMeanEvolution.continuousVelocity_translation_contDiff
{T : ℝ}
{hT : 0 ≤ T}
{FInv F F₁ : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)}
{A : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2}
{L : ℝ}
{u f : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)}
(s : StrongMeanEvolution T hT FInv F F₁ A L u f)
{n : WithTop ℕ∞}
(hB : ContDiff ℝ n fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeTranslation T a) s.velocityField)
(hBt :
ContDiff ℝ n fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeTranslation T a) s.velocityDerivative)
:
ContDiff ℝ n fun (a : EulerSmoothLimit.Space) =>
(EulerMeanTimeContinuousTranslation.pathTranslation T a) s.continuousVelocity
The actual continuous velocity inherits spatial regularity uniformly in time.
theorem
EulerMeanVariationalInverse.StrongMeanEvolution.physicalPath_translation_contDiff
{T : ℝ}
{hT : 0 ≤ T}
{FInv F F₁ : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)}
{A : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2}
{L : ℝ}
{u f : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)}
(s : StrongMeanEvolution T hT FInv F F₁ A L u f)
(hTpos : 0 < T)
(hF : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT F) (F₁ t) (Set.Icc 0 T) ↑t)
{n : WithTop ℕ∞}
(hB : ContDiff ℝ n fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeTranslation T a) s.velocityField)
(hBt :
ContDiff ℝ n fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeTranslation T a) s.velocityDerivative)
(t : ↑(Set.Icc 0 T))
:
ContDiff ℝ n fun (a : EulerSmoothLimit.Space) => (EulerMeanSolenoidal.translation a) (s.physicalPath ↑t)
The actual spatial orbit of B(t) is regular for every t, including both endpoints.
theorem
EulerMeanVariationalInverse.StrongMeanEvolution.continuousVelocity_translation_gevrey
{T : ℝ}
{hT : 0 ≤ T}
{FInv F F₁ : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)}
{A : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2}
{L : ℝ}
{u f : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)}
(s : StrongMeanEvolution T hT FInv F F₁ A L u f)
(hTpos : 0 < T)
(hB : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeTranslation T a) s.velocityField)
(hBt :
ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeTranslation T a) s.velocityDerivative)
(R C D : ℝ)
(hR : 0 ≤ R)
(hC : 0 ≤ C)
(hD : 0 ≤ D)
(d : ℕ)
(hBb :
∀ (n : ℕ) (a : EulerSmoothLimit.Space),
‖iteratedFDeriv ℝ n
(fun (b : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeTranslation T b) s.velocityField) a‖ ≤ C * EulerGevrey.majorant R d n)
(hBtb :
∀ (n : ℕ) (a : EulerSmoothLimit.Space),
‖iteratedFDeriv ℝ n
(fun (b : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeTranslation T b) s.velocityDerivative) a‖ ≤ D * EulerGevrey.majorant R d n)
(n : ℕ)
(a : EulerSmoothLimit.Space)
:
‖iteratedFDeriv ℝ n
(fun (b : EulerSmoothLimit.Space) =>
(EulerMeanTimeContinuousTranslation.pathTranslation T b) s.continuousVelocity)
a‖ ≤ (T⁻¹ * √T * C + 2 * √T * D) * EulerGevrey.majorant R d n
The actual uniform-time velocity has the explicit H¹ trace amplitude.
theorem
EulerMeanVariationalInverse.StrongMeanEvolution.physicalPath_translation_gevrey
{T : ℝ}
{hT : 0 ≤ T}
{FInv F F₁ : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)}
{A : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2}
{L : ℝ}
{u f : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)}
(s : StrongMeanEvolution T hT FInv F F₁ A L u f)
(hTpos : 0 < T)
(hF : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT F) (F₁ t) (Set.Icc 0 T) ↑t)
(hB : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeTranslation T a) s.velocityField)
(hBt :
ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeTranslation T a) s.velocityDerivative)
(R C D : ℝ)
(hR : 0 ≤ R)
(hC : 0 ≤ C)
(hD : 0 ≤ D)
(d : ℕ)
(hBb :
∀ (n : ℕ) (a : EulerSmoothLimit.Space),
‖iteratedFDeriv ℝ n
(fun (b : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeTranslation T b) s.velocityField) a‖ ≤ C * EulerGevrey.majorant R d n)
(hBtb :
∀ (n : ℕ) (a : EulerSmoothLimit.Space),
‖iteratedFDeriv ℝ n
(fun (b : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeTranslation T b) s.velocityDerivative) a‖ ≤ D * EulerGevrey.majorant R d n)
(t : ↑(Set.Icc 0 T))
(n : ℕ)
(a : EulerSmoothLimit.Space)
:
‖iteratedFDeriv ℝ n (fun (b : EulerSmoothLimit.Space) => (EulerMeanSolenoidal.translation b) (s.physicalPath ↑t)) a‖ ≤ (T⁻¹ * √T * C + 2 * √T * D) * EulerGevrey.majorant R d n
Every actual time slice obeys the same bound, with no extra spatial derivative loss.