Actual continuous coordinate-velocity spatial orbits #
The coordinate velocity is reconstructed from its genuine L² value and acceleration. Consequently its uniform-time spatial derivatives have the same fixed H¹ trace bound as the physical velocity.
noncomputable def
EulerMeanCoordinatePath.coordinatePathTranslation
(T : ℝ)
(a : EulerSmoothLimit.Space)
:
Spatial translation of continuous solenoidal coordinate paths.
Equations
Instances For
@[simp]
theorem
EulerMeanCoordinatePath.coordinatePathTranslation_apply
(T : ℝ)
(a : EulerSmoothLimit.Space)
(p : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.solenoidalSpace))
(t : ↑(Set.Icc 0 T))
:
theorem
EulerMeanCoordinatePath.reconstruction_translation
(T : ℝ)
(hT : 0 ≤ T)
(a : EulerSmoothLimit.Space)
(p q : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace))
:
theorem
EulerMeanVariationalInverse.StrongMeanEvolution.coordinateVelocityPath_eq_reconstruction
{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)
:
theorem
EulerMeanVariationalInverse.StrongMeanEvolution.coordinateVelocityPath_orbit_eq
{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)
:
(fun (a : EulerSmoothLimit.Space) => (EulerMeanCoordinatePath.coordinatePathTranslation T a) s.coordinateVelocityPath) = fun (a : EulerSmoothLimit.Space) =>
(EulerTimeH1Reconstruction.reconstruction T hT)
((EulerMeanTimeTranslation.timeSolenoidalTranslation T a) s.velocityLp, (EulerMeanTimeTranslation.timeSolenoidalTranslation T a) s.acceleration)
theorem
EulerMeanVariationalInverse.StrongMeanEvolution.coordinateVelocityPath_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)
{n : WithTop ℕ∞}
(hv :
ContDiff ℝ n fun (a : EulerSmoothLimit.Space) =>
(EulerMeanTimeTranslation.timeSolenoidalTranslation T a) s.velocityLp)
(ha :
ContDiff ℝ n fun (a : EulerSmoothLimit.Space) =>
(EulerMeanTimeTranslation.timeSolenoidalTranslation T a) s.acceleration)
:
ContDiff ℝ n fun (a : EulerSmoothLimit.Space) =>
(EulerMeanCoordinatePath.coordinatePathTranslation T a) s.coordinateVelocityPath
Uniform-time coordinate orbit regularity comes from the actual H¹ data.
theorem
EulerMeanVariationalInverse.StrongMeanEvolution.coordinateVelocityPath_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)
(hv :
ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) =>
(EulerMeanTimeTranslation.timeSolenoidalTranslation T a) s.velocityLp)
(ha :
ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) =>
(EulerMeanTimeTranslation.timeSolenoidalTranslation T a) s.acceleration)
(R Cv Ca : ℝ)
(hR : 0 ≤ R)
(hCv : 0 ≤ Cv)
(hCa : 0 ≤ Ca)
(d : ℕ)
(hvb :
∀ (n : ℕ) (a : EulerSmoothLimit.Space),
‖iteratedFDeriv ℝ n
(fun (b : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeSolenoidalTranslation T b) s.velocityLp)
a‖ ≤ Cv * EulerGevrey.majorant R d n)
(hab :
∀ (n : ℕ) (a : EulerSmoothLimit.Space),
‖iteratedFDeriv ℝ n
(fun (b : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeSolenoidalTranslation T b) s.acceleration)
a‖ ≤ Ca * EulerGevrey.majorant R d n)
(n : ℕ)
(a : EulerSmoothLimit.Space)
:
‖iteratedFDeriv ℝ n
(fun (b : EulerSmoothLimit.Space) =>
(EulerMeanCoordinatePath.coordinatePathTranslation T b) s.coordinateVelocityPath)
a‖ ≤ (T⁻¹ * √T * Cv + 2 * √T * Ca) * EulerGevrey.majorant R d n
Every spatial coordinate-velocity derivative has the same uniform-time trace cost.