Related estimates used together by the same construction modules.
All-order estimates for the genuine strong mean fields #
The actual coordinate velocity estimate supplied by the weak inverse gives the next-shift acceleration estimate and the physical B, B_t estimates. The constants are fixed polynomials in the coefficient amplitudes and the proved inverse bound; none depends on the derivative order.
Enlarging the integer shift preserves a factorial bound when the radius is at least one.
theorem
EulerMeanVariationalInverse.StrongMeanEvolution.acceleration_orbit_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)
(c : ℝ)
(hc : 0 < c)
(hLower :
∀ (t : ↑(Set.Icc 0 T)) (v : ↥EulerMeanSolenoidal.solenoidalSpace), c * ‖v‖ ^ 2 ≤ ‖((solenoidalFrame T F) t) v‖ ^ 2)
(hF : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => EulerMeanOperatorTranslation.translatePath T a F)
(hF₁ : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => EulerMeanOperatorTranslation.translatePath T a F₁)
(hv :
ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) =>
(EulerMeanTimeTranslation.timeSolenoidalTranslation T a) s.velocityLp)
(hf : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeTranslation T a) f)
:
ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) =>
(EulerMeanTimeTranslation.timeSolenoidalTranslation T a) s.acceleration
The genuine acceleration is spatially smooth once the solved coordinate velocity and prescribed coefficients and forcing are.
theorem
EulerMeanVariationalInverse.StrongMeanEvolution.spatial_gevrey_bounds
{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)
(c : ℝ)
(hc : 0 < c)
(hLower :
∀ (t : ↑(Set.Icc 0 T)) (v : ↥EulerMeanSolenoidal.solenoidalSpace), c * ‖v‖ ^ 2 ≤ ‖((solenoidalFrame T F) t) v‖ ^ 2)
(hF : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => EulerMeanOperatorTranslation.translatePath T a F)
(hF₁ : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => EulerMeanOperatorTranslation.translatePath T a F₁)
(hv :
ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) =>
(EulerMeanTimeTranslation.timeSolenoidalTranslation T a) s.velocityLp)
(hf : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeTranslation T a) f)
(Rc R CF CF₁ Cf : ℝ)
(hRc : 0 ≤ Rc)
(hR : 1 ≤ R)
(hRcR : Rc ≤ R)
(hCF : 0 ≤ CF)
(hCF₁ : 0 ≤ CF₁)
(hCf : 0 ≤ Cf)
(hstrong : 2 * EulerTimeLpGramGevrey.gramCost c CF (3 * CF * (Cf + 6 * CF₁)) * (Rc + 1) ≤ R)
(hFb :
∀ (n : ℕ) (a : EulerSmoothLimit.Space),
‖iteratedFDeriv ℝ n (fun (b : EulerSmoothLimit.Space) => EulerMeanOperatorTranslation.translatePath T b F) a‖ ≤ CF * EulerGevrey.majorant Rc 0 n)
(hF₁b :
∀ (n : ℕ) (a : EulerSmoothLimit.Space),
‖iteratedFDeriv ℝ n (fun (b : EulerSmoothLimit.Space) => EulerMeanOperatorTranslation.translatePath T b F₁) a‖ ≤ CF₁ * EulerGevrey.majorant Rc 0 n)
(d : ℕ)
(hfb :
∀ (n : ℕ) (a : EulerSmoothLimit.Space),
‖iteratedFDeriv ℝ n (fun (b : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeTranslation T b) f) a‖ ≤ Cf * EulerGevrey.majorant R d n)
(hvb :
∀ (n : ℕ) (a : EulerSmoothLimit.Space),
‖iteratedFDeriv ℝ n
(fun (b : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeSolenoidalTranslation T b) s.velocityLp)
a‖ ≤ EulerGevrey.majorant R (d + 1) n)
:
(∀ (n : ℕ) (a : EulerSmoothLimit.Space),
‖iteratedFDeriv ℝ n
(fun (b : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeSolenoidalTranslation T b) s.acceleration)
a‖ ≤ EulerGevrey.majorant R (d + 2) n) ∧ (∀ (n : ℕ) (a : EulerSmoothLimit.Space),
‖iteratedFDeriv ℝ n
(fun (b : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeTranslation T b) s.velocityField) a‖ ≤ 3 * CF * EulerGevrey.majorant R (d + 1) n) ∧ ∀ (n : ℕ) (a : EulerSmoothLimit.Space),
‖iteratedFDeriv ℝ n
(fun (b : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeTranslation T b) s.velocityDerivative)
a‖ ≤ 3 * (CF₁ + CF) * EulerGevrey.majorant R (d + 2) n
The actual strong fields have the source's successive factorial shifts.
theorem
EulerMeanVariationalInverse.StrongMeanEvolution.continuousVelocity_spatial_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)
(c : ℝ)
(hc : 0 < c)
(hLower :
∀ (t : ↑(Set.Icc 0 T)) (v : ↥EulerMeanSolenoidal.solenoidalSpace), c * ‖v‖ ^ 2 ≤ ‖((solenoidalFrame T F) t) v‖ ^ 2)
(hF : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => EulerMeanOperatorTranslation.translatePath T a F)
(hF₁ : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => EulerMeanOperatorTranslation.translatePath T a F₁)
(hv :
ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) =>
(EulerMeanTimeTranslation.timeSolenoidalTranslation T a) s.velocityLp)
(hf : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeTranslation T a) f)
(Rc R CF CF₁ Cf : ℝ)
(hRc : 0 ≤ Rc)
(hR : 1 ≤ R)
(hRcR : Rc ≤ R)
(hCF : 0 ≤ CF)
(hCF₁ : 0 ≤ CF₁)
(hCf : 0 ≤ Cf)
(hstrong : 2 * EulerTimeLpGramGevrey.gramCost c CF (3 * CF * (Cf + 6 * CF₁)) * (Rc + 1) ≤ R)
(hFb :
∀ (n : ℕ) (a : EulerSmoothLimit.Space),
‖iteratedFDeriv ℝ n (fun (b : EulerSmoothLimit.Space) => EulerMeanOperatorTranslation.translatePath T b F) a‖ ≤ CF * EulerGevrey.majorant Rc 0 n)
(hF₁b :
∀ (n : ℕ) (a : EulerSmoothLimit.Space),
‖iteratedFDeriv ℝ n (fun (b : EulerSmoothLimit.Space) => EulerMeanOperatorTranslation.translatePath T b F₁) a‖ ≤ CF₁ * EulerGevrey.majorant Rc 0 n)
(d : ℕ)
(hfb :
∀ (n : ℕ) (a : EulerSmoothLimit.Space),
‖iteratedFDeriv ℝ n (fun (b : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeTranslation T b) f) a‖ ≤ Cf * EulerGevrey.majorant R d n)
(hvb :
∀ (n : ℕ) (a : EulerSmoothLimit.Space),
‖iteratedFDeriv ℝ n
(fun (b : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeSolenoidalTranslation T b) s.velocityLp)
a‖ ≤ EulerGevrey.majorant R (d + 1) n)
(hTpos : 0 < T)
(n : ℕ)
(a : EulerSmoothLimit.Space)
:
‖iteratedFDeriv ℝ n
(fun (b : EulerSmoothLimit.Space) =>
(EulerMeanTimeContinuousTranslation.pathTranslation T b) s.continuousVelocity)
a‖ ≤ (T⁻¹ * √T * (3 * CF) + 2 * √T * (3 * (CF₁ + CF))) * EulerGevrey.majorant R (d + 2) n
The actual continuous-time velocity has the same fixed factorial radius.
Classical spatial representatives of the actual mean time evolution #
The actual continuous velocity and continuous time derivative have smooth spatial translation orbits. The bounded time-integral identity commutes with those spatial derivatives, giving genuine jointly continuous spatial representatives and their pointwise classical time derivative.
theorem
EulerMeanClassicalSpatialTime.exists_classical_pair
(T : ℝ)
(hT : 0 ≤ T)
(p q : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2))
(hp : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation T a) p)
(hq : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation T a) q)
(hder : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT p) (q t) (Set.Icc 0 T) ↑t)
:
∃ (B : ↑(Set.Icc 0 T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (Bt :
↑(Set.Icc 0 T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space),
(Continuous fun (z : ↑(Set.Icc 0 T) × EulerSmoothLimit.Space) => B z.1 z.2) ∧ (Continuous fun (z : ↑(Set.Icc 0 T) × EulerSmoothLimit.Space) => Bt z.1 z.2) ∧ (∀ (t : ↑(Set.Icc 0 T)), ContDiff ℝ (↑⊤) (B t)) ∧ (∀ (t : ↑(Set.Icc 0 T)), ContDiff ℝ (↑⊤) (Bt t)) ∧ (∀ (t : ↑(Set.Icc 0 T)), ↑↑(p t) =ᵐ[MeasureTheory.volume] B t) ∧ (∀ (t : ↑(Set.Icc 0 T)), ↑↑(q t) =ᵐ[MeasureTheory.volume] Bt t) ∧ ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space),
HasDerivWithinAt (fun (r : ℝ) => B (Set.projIcc 0 T hT r) x) (Bt t x) (Set.Icc 0 T) ↑t
Actual smooth representatives of a continuous L² path and its genuine continuous derivative, with no separate mixed-derivative hypothesis.
theorem
EulerMeanVariationalInverse.StrongMeanEvolution.continuousVelocity_hasDerivWithinAt
{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)
(c : ℝ)
(hc : 0 < c)
(hLower :
∀ (t : ↑(Set.Icc 0 T)) (v : ↥EulerMeanSolenoidal.solenoidalSpace), c * ‖v‖ ^ 2 ≤ ‖((solenoidalFrame T F) t) v‖ ^ 2)
(fC : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2))
(hTpos : 0 < T)
(hf : ↑↑f =ᵐ[EulerTimeLp.timeMeasure T] EulerVolterraConvolution.extendPath T hT fC)
(hFTime : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT F) (F₁ t) (Set.Icc 0 T) ↑t)
(t : ↑(Set.Icc 0 T))
:
HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT s.continuousVelocity)
((s.classicalPhysicalDerivative c hc hLower fC) t) (Set.Icc 0 T) ↑t
The reconstructed velocity path has its actual continuous derivative at every time, including within-interval endpoint derivatives.
theorem
EulerMeanVariationalInverse.StrongMeanEvolution.exists_classical_spatial_pair
{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)
(c : ℝ)
(hc : 0 < c)
(hLower :
∀ (t : ↑(Set.Icc 0 T)) (v : ↥EulerMeanSolenoidal.solenoidalSpace), c * ‖v‖ ^ 2 ≤ ‖((solenoidalFrame T F) t) v‖ ^ 2)
(fC : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2))
(hTpos : 0 < T)
(hf : ↑↑f =ᵐ[EulerTimeLp.timeMeasure T] EulerVolterraConvolution.extendPath T hT fC)
(hFTime : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT F) (F₁ t) (Set.Icc 0 T) ↑t)
(hF : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => EulerMeanOperatorTranslation.translatePath T a F)
(hF₁ : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => EulerMeanOperatorTranslation.translatePath T a F₁)
(hv :
ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) =>
(EulerMeanTimeTranslation.timeSolenoidalTranslation T a) s.velocityLp)
(ha :
ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) =>
(EulerMeanTimeTranslation.timeSolenoidalTranslation T a) s.acceleration)
(hfC : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation T a) fC)
:
∃ (B : ↑(Set.Icc 0 T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (Bt :
↑(Set.Icc 0 T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space),
(Continuous fun (z : ↑(Set.Icc 0 T) × EulerSmoothLimit.Space) => B z.1 z.2) ∧ (Continuous fun (z : ↑(Set.Icc 0 T) × EulerSmoothLimit.Space) => Bt z.1 z.2) ∧ (∀ (t : ↑(Set.Icc 0 T)), ContDiff ℝ (↑⊤) (B t)) ∧ (∀ (t : ↑(Set.Icc 0 T)), ContDiff ℝ (↑⊤) (Bt t)) ∧ (∀ (t : ↑(Set.Icc 0 T)), ↑↑(s.physicalPath ↑t) =ᵐ[MeasureTheory.volume] B t) ∧ (∀ (t : ↑(Set.Icc 0 T)),
↑↑((s.classicalPhysicalDerivative c hc hLower fC) t) =ᵐ[MeasureTheory.volume] Bt t) ∧ ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space),
HasDerivWithinAt (fun (r : ℝ) => B (Set.projIcc 0 T hT r) x) (Bt t x) (Set.Icc 0 T) ↑t
Genuine space-time classical mean fields are obtained from the actual solved coordinate velocity and acceleration orbits.