Spatial regularity of the actual source mean inverse #
Every strong realization of the constructed source solver has the same fixed coordinate velocity. Its spatial regularity is therefore supplied by the actual variational inverse, then passed through the proved Gram inverse and physical frame. No spatial regularity of the unknown fields is assumed.
Identification of the strong mean velocity with the fixed derivative variable #
The actual AC label has its actual L² velocity as derivative and zero terminal trace. Terminal-primitive uniqueness therefore identifies every strong realization with the same fixed-coordinate derivative field. Spatial estimates for the fixed inverse consequently apply to the constructed physical velocity.
theorem
EulerMeanVariationalInverse.StrongMeanEvolution.terminalPrimitive_velocityLp
{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)
(t : ↑(Set.Icc 0 T))
:
The actual strong label is exactly the terminal primitive of its L² velocity.
theorem
EulerMeanVariationalInverse.StrongMeanEvolution.productDerivative_velocityLp
{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)
(hF : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT F) (F₁ t) (Set.Icc 0 T) ↑t)
(hRight : ∀ (t : ↑(Set.Icc 0 T)) (x : ↥EulerMeanSolenoidal.L2), (F t) ((FInv t) x) = x)
:
(EulerTimeH1OperatorProduct.productDerivative T hT (solenoidalFrame T F) (solenoidalFrame T F₁)) s.velocityLp = u
Differentiating the reconstructed displacement gives the original genuine variational derivative field.
theorem
EulerMeanVariationalInverse.StrongMeanEvolution.velocityLp_eq_meanBackward
(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 : ↥(meanDerivatives T hT FInv))
(f : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2))
(s : StrongMeanEvolution T hT FInv F F₁ A L (↑u) f)
(hInv : ∀ (t : ↑(Set.Icc 0 T)) (x : ↥EulerMeanSolenoidal.L2), (FInv t) ((F t) x) = x)
(hF : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT F) (F₁ t) (Set.Icc 0 T) ↑t)
(hRight : ∀ (t : ↑(Set.Icc 0 T)) (x : ↥EulerMeanSolenoidal.L2), (F t) ((FInv t) x) = x)
:
The strong velocity is exactly the canonical fixed-coordinate derivative, not merely another solution of a similar equation.
theorem
EulerMeanSourceSpatialRegularity.velocity_eq_sourceCoordinates
(T : ℝ)
(hT : 0 ≤ T)
(ℓ : ℝ)
(hℓ : 0 < ℓ)
(F F₁ H :
EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))
(M0 : EulerMeanCoefficients.BoundedSmoothField (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))
(FInv : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2))
(Be Bc L r : ℝ)
(hBe : 0 ≤ Be)
(hBc : 0 ≤ Bc)
(hL : EulerMeanHarmonic.boundaryLocalizationC1 * Bc ≤ L)
(hr : 0 ≤ r)
(hrquarter : r ≤ 1 / 4)
(hext :
∀ (x : EulerSmoothLimit.Space),
r ≤ ‖ℓ • x‖ → ∀ (v : EulerSmoothLimit.Space), -Be * ‖v‖ ^ 2 ≤ inner ℝ ((M0.field x) v) v)
(hcore :
∀ (x : EulerSmoothLimit.Space),
‖ℓ • x‖ < r → ∀ (v : EulerSmoothLimit.Space), -Bc * ‖v‖ ^ 2 ≤ inner ℝ ((M0.field x) v) v)
(hInv :
∀ (t : ↑(Set.Icc 0 T)) (x : ↥EulerMeanSolenoidal.L2),
(FInv t) (((EulerMeanCoefficients.operatorPath T F.field) t) x) = x)
(hF :
∀ (t : ↑(Set.Icc 0 T)),
HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (EulerMeanCoefficients.operatorPath T F.field))
((EulerMeanCoefficients.operatorPath T F₁.field) t) (Set.Icc 0 T) ↑t)
(hRight :
∀ (t : ↑(Set.Icc 0 T)) (x : ↥EulerMeanSolenoidal.L2),
((EulerMeanCoefficients.operatorPath T F.field) t) ((FInv t) x) = x)
(K : ℝ)
(hK : 0 ≤ K)
(hF0 : FInv ⟨0, ⋯⟩ = ContinuousLinearMap.id ℝ ↥EulerMeanSolenoidal.L2)
(hH : ∀ (t : ↑(Set.Icc 0 T)) (x v : EulerSmoothLimit.Space), inner ℝ (((H.field t) x) v) v ≤ K * ‖v‖ ^ 2)
(hsmall : K * (T ^ 2 / 2) + Be * T + EulerMeanHarmonic.boundaryLocalizationC2 * Bc * r ^ 3 * T ≤ 1 / 2)
(f : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2))
(s :
EulerMeanVariationalInverse.StrongMeanEvolution T hT FInv (EulerMeanCoefficients.operatorPath T F.field)
(EulerMeanCoefficients.operatorPath T F₁.field)
(EulerMeanBoundary.boundaryOperator (EulerMeanBoundary.scaledCutoff ℓ hℓ)) L
(↑((EulerMeanSourceInverse.sourceMeanSolver T hT ℓ hℓ ⇑M0.field ⋯ ‖M0.field‖₊ ⋯ Be Bc L r hBe hBc hL hr hrquarter
hext hcore FInv (EulerMeanCoefficients.operatorPath T H.field) K hK hF0 ⋯ hsmall)
f))
f)
:
s.velocityLp = (EulerMeanSourceFixedInverse.sourceCoordinateSolver T hT ℓ hℓ F F₁ H M0 FInv Be Bc L r hBe hBc hL hr hrquarter hext
hcore hInv hF K hK hF0 hH hsmall)
f
The actual strong velocity is the constructed fixed-coordinate source solve.
theorem
EulerMeanSourceSpatialRegularity.velocity_translation_contDiff
(T : ℝ)
(hT : 0 ≤ T)
(ℓ : ℝ)
(hℓ : 0 < ℓ)
(F F₁ H :
EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))
(M0 : EulerMeanCoefficients.BoundedSmoothField (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))
(FInv : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2))
(Be Bc L r : ℝ)
(hBe : 0 ≤ Be)
(hBc : 0 ≤ Bc)
(hL : EulerMeanHarmonic.boundaryLocalizationC1 * Bc ≤ L)
(hr : 0 ≤ r)
(hrquarter : r ≤ 1 / 4)
(hext :
∀ (x : EulerSmoothLimit.Space),
r ≤ ‖ℓ • x‖ → ∀ (v : EulerSmoothLimit.Space), -Be * ‖v‖ ^ 2 ≤ inner ℝ ((M0.field x) v) v)
(hcore :
∀ (x : EulerSmoothLimit.Space),
‖ℓ • x‖ < r → ∀ (v : EulerSmoothLimit.Space), -Bc * ‖v‖ ^ 2 ≤ inner ℝ ((M0.field x) v) v)
(hInv :
∀ (t : ↑(Set.Icc 0 T)) (x : ↥EulerMeanSolenoidal.L2),
(FInv t) (((EulerMeanCoefficients.operatorPath T F.field) t) x) = x)
(hF :
∀ (t : ↑(Set.Icc 0 T)),
HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (EulerMeanCoefficients.operatorPath T F.field))
((EulerMeanCoefficients.operatorPath T F₁.field) t) (Set.Icc 0 T) ↑t)
(hRight :
∀ (t : ↑(Set.Icc 0 T)) (x : ↥EulerMeanSolenoidal.L2),
((EulerMeanCoefficients.operatorPath T F.field) t) ((FInv t) x) = x)
(K : ℝ)
(hK : 0 ≤ K)
(hF0 : FInv ⟨0, ⋯⟩ = ContinuousLinearMap.id ℝ ↥EulerMeanSolenoidal.L2)
(hH : ∀ (t : ↑(Set.Icc 0 T)) (x v : EulerSmoothLimit.Space), inner ℝ (((H.field t) x) v) v ≤ K * ‖v‖ ^ 2)
(hsmall : K * (T ^ 2 / 2) + Be * T + EulerMeanHarmonic.boundaryLocalizationC2 * Bc * r ^ 3 * T ≤ 1 / 2)
(f : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2))
(s :
EulerMeanVariationalInverse.StrongMeanEvolution T hT FInv (EulerMeanCoefficients.operatorPath T F.field)
(EulerMeanCoefficients.operatorPath T F₁.field)
(EulerMeanBoundary.boundaryOperator (EulerMeanBoundary.scaledCutoff ℓ hℓ)) L
(↑((EulerMeanSourceInverse.sourceMeanSolver T hT ℓ hℓ ⇑M0.field ⋯ ‖M0.field‖₊ ⋯ Be Bc L r hBe hBc hL hr hrquarter
hext hcore FInv (EulerMeanCoefficients.operatorPath T H.field) K hK hF0 ⋯ hsmall)
f))
f)
(hf : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeTranslation T a) f)
:
ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeSolenoidalTranslation T a) s.velocityLp
Actual coordinate-velocity spatial regularity follows from the source assumptions.
theorem
EulerMeanSourceSpatialRegularity.acceleration_translation_contDiff
(T : ℝ)
(hT : 0 ≤ T)
(ℓ : ℝ)
(hℓ : 0 < ℓ)
(F F₁ H :
EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))
(M0 : EulerMeanCoefficients.BoundedSmoothField (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))
(FInv : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2))
(Be Bc L r : ℝ)
(hBe : 0 ≤ Be)
(hBc : 0 ≤ Bc)
(hL : EulerMeanHarmonic.boundaryLocalizationC1 * Bc ≤ L)
(hr : 0 ≤ r)
(hrquarter : r ≤ 1 / 4)
(hext :
∀ (x : EulerSmoothLimit.Space),
r ≤ ‖ℓ • x‖ → ∀ (v : EulerSmoothLimit.Space), -Be * ‖v‖ ^ 2 ≤ inner ℝ ((M0.field x) v) v)
(hcore :
∀ (x : EulerSmoothLimit.Space),
‖ℓ • x‖ < r → ∀ (v : EulerSmoothLimit.Space), -Bc * ‖v‖ ^ 2 ≤ inner ℝ ((M0.field x) v) v)
(hInv :
∀ (t : ↑(Set.Icc 0 T)) (x : ↥EulerMeanSolenoidal.L2),
(FInv t) (((EulerMeanCoefficients.operatorPath T F.field) t) x) = x)
(hF :
∀ (t : ↑(Set.Icc 0 T)),
HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (EulerMeanCoefficients.operatorPath T F.field))
((EulerMeanCoefficients.operatorPath T F₁.field) t) (Set.Icc 0 T) ↑t)
(hRight :
∀ (t : ↑(Set.Icc 0 T)) (x : ↥EulerMeanSolenoidal.L2),
((EulerMeanCoefficients.operatorPath T F.field) t) ((FInv t) x) = x)
(K : ℝ)
(hK : 0 ≤ K)
(hF0 : FInv ⟨0, ⋯⟩ = ContinuousLinearMap.id ℝ ↥EulerMeanSolenoidal.L2)
(hH : ∀ (t : ↑(Set.Icc 0 T)) (x v : EulerSmoothLimit.Space), inner ℝ (((H.field t) x) v) v ≤ K * ‖v‖ ^ 2)
(hsmall : K * (T ^ 2 / 2) + Be * T + EulerMeanHarmonic.boundaryLocalizationC2 * Bc * r ^ 3 * T ≤ 1 / 2)
(f : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2))
(s :
EulerMeanVariationalInverse.StrongMeanEvolution T hT FInv (EulerMeanCoefficients.operatorPath T F.field)
(EulerMeanCoefficients.operatorPath T F₁.field)
(EulerMeanBoundary.boundaryOperator (EulerMeanBoundary.scaledCutoff ℓ hℓ)) L
(↑((EulerMeanSourceInverse.sourceMeanSolver T hT ℓ hℓ ⇑M0.field ⋯ ‖M0.field‖₊ ⋯ Be Bc L r hBe hBc hL hr hrquarter
hext hcore FInv (EulerMeanCoefficients.operatorPath T H.field) K hK hF0 ⋯ hsmall)
f))
f)
(hf : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeTranslation T a) f)
:
ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) =>
(EulerMeanTimeTranslation.timeSolenoidalTranslation T a) s.acceleration
The actual acceleration has genuine spatial regularity, supplied by the uniformly coercive translated Gram solve.
theorem
EulerMeanSourceSpatialRegularity.physical_translation_contDiff
(T : ℝ)
(hT : 0 ≤ T)
(ℓ : ℝ)
(hℓ : 0 < ℓ)
(F F₁ H :
EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))
(M0 : EulerMeanCoefficients.BoundedSmoothField (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))
(FInv : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2))
(Be Bc L r : ℝ)
(hBe : 0 ≤ Be)
(hBc : 0 ≤ Bc)
(hL : EulerMeanHarmonic.boundaryLocalizationC1 * Bc ≤ L)
(hr : 0 ≤ r)
(hrquarter : r ≤ 1 / 4)
(hext :
∀ (x : EulerSmoothLimit.Space),
r ≤ ‖ℓ • x‖ → ∀ (v : EulerSmoothLimit.Space), -Be * ‖v‖ ^ 2 ≤ inner ℝ ((M0.field x) v) v)
(hcore :
∀ (x : EulerSmoothLimit.Space),
‖ℓ • x‖ < r → ∀ (v : EulerSmoothLimit.Space), -Bc * ‖v‖ ^ 2 ≤ inner ℝ ((M0.field x) v) v)
(hInv :
∀ (t : ↑(Set.Icc 0 T)) (x : ↥EulerMeanSolenoidal.L2),
(FInv t) (((EulerMeanCoefficients.operatorPath T F.field) t) x) = x)
(hF :
∀ (t : ↑(Set.Icc 0 T)),
HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (EulerMeanCoefficients.operatorPath T F.field))
((EulerMeanCoefficients.operatorPath T F₁.field) t) (Set.Icc 0 T) ↑t)
(hRight :
∀ (t : ↑(Set.Icc 0 T)) (x : ↥EulerMeanSolenoidal.L2),
((EulerMeanCoefficients.operatorPath T F.field) t) ((FInv t) x) = x)
(K : ℝ)
(hK : 0 ≤ K)
(hF0 : FInv ⟨0, ⋯⟩ = ContinuousLinearMap.id ℝ ↥EulerMeanSolenoidal.L2)
(hH : ∀ (t : ↑(Set.Icc 0 T)) (x v : EulerSmoothLimit.Space), inner ℝ (((H.field t) x) v) v ≤ K * ‖v‖ ^ 2)
(hsmall : K * (T ^ 2 / 2) + Be * T + EulerMeanHarmonic.boundaryLocalizationC2 * Bc * r ^ 3 * T ≤ 1 / 2)
(f : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2))
(s :
EulerMeanVariationalInverse.StrongMeanEvolution T hT FInv (EulerMeanCoefficients.operatorPath T F.field)
(EulerMeanCoefficients.operatorPath T F₁.field)
(EulerMeanBoundary.boundaryOperator (EulerMeanBoundary.scaledCutoff ℓ hℓ)) L
(↑((EulerMeanSourceInverse.sourceMeanSolver T hT ℓ hℓ ⇑M0.field ⋯ ‖M0.field‖₊ ⋯ Be Bc L r hBe hBc hL hr hrquarter
hext hcore FInv (EulerMeanCoefficients.operatorPath T H.field) K hK hF0 ⋯ hsmall)
f))
f)
(hf : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeTranslation T a) f)
:
(ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeTranslation T a) s.velocityField) ∧ (ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) =>
(EulerMeanTimeTranslation.timeTranslation T a) s.velocityDerivative) ∧ ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeTranslation T a) s.pressureResidual
Both actual physical fields B and B_t, and their pressure residual, have smooth spatial translation orbits.
theorem
EulerMeanSourceSpatialRegularity.continuousVelocity_translation_contDiff
(T : ℝ)
(hT : 0 ≤ T)
(ℓ : ℝ)
(hℓ : 0 < ℓ)
(F F₁ H :
EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))
(M0 : EulerMeanCoefficients.BoundedSmoothField (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))
(FInv : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2))
(Be Bc L r : ℝ)
(hBe : 0 ≤ Be)
(hBc : 0 ≤ Bc)
(hL : EulerMeanHarmonic.boundaryLocalizationC1 * Bc ≤ L)
(hr : 0 ≤ r)
(hrquarter : r ≤ 1 / 4)
(hext :
∀ (x : EulerSmoothLimit.Space),
r ≤ ‖ℓ • x‖ → ∀ (v : EulerSmoothLimit.Space), -Be * ‖v‖ ^ 2 ≤ inner ℝ ((M0.field x) v) v)
(hcore :
∀ (x : EulerSmoothLimit.Space),
‖ℓ • x‖ < r → ∀ (v : EulerSmoothLimit.Space), -Bc * ‖v‖ ^ 2 ≤ inner ℝ ((M0.field x) v) v)
(hInv :
∀ (t : ↑(Set.Icc 0 T)) (x : ↥EulerMeanSolenoidal.L2),
(FInv t) (((EulerMeanCoefficients.operatorPath T F.field) t) x) = x)
(hF :
∀ (t : ↑(Set.Icc 0 T)),
HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (EulerMeanCoefficients.operatorPath T F.field))
((EulerMeanCoefficients.operatorPath T F₁.field) t) (Set.Icc 0 T) ↑t)
(hRight :
∀ (t : ↑(Set.Icc 0 T)) (x : ↥EulerMeanSolenoidal.L2),
((EulerMeanCoefficients.operatorPath T F.field) t) ((FInv t) x) = x)
(K : ℝ)
(hK : 0 ≤ K)
(hF0 : FInv ⟨0, ⋯⟩ = ContinuousLinearMap.id ℝ ↥EulerMeanSolenoidal.L2)
(hH : ∀ (t : ↑(Set.Icc 0 T)) (x v : EulerSmoothLimit.Space), inner ℝ (((H.field t) x) v) v ≤ K * ‖v‖ ^ 2)
(hsmall : K * (T ^ 2 / 2) + Be * T + EulerMeanHarmonic.boundaryLocalizationC2 * Bc * r ^ 3 * T ≤ 1 / 2)
(f : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2))
(s :
EulerMeanVariationalInverse.StrongMeanEvolution T hT FInv (EulerMeanCoefficients.operatorPath T F.field)
(EulerMeanCoefficients.operatorPath T F₁.field)
(EulerMeanBoundary.boundaryOperator (EulerMeanBoundary.scaledCutoff ℓ hℓ)) L
(↑((EulerMeanSourceInverse.sourceMeanSolver T hT ℓ hℓ ⇑M0.field ⋯ ‖M0.field‖₊ ⋯ Be Bc L r hBe hBc hL hr hrquarter
hext hcore FInv (EulerMeanCoefficients.operatorPath T H.field) K hK hF0 ⋯ hsmall)
f))
f)
(hf : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeTranslation T a) f)
:
ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) =>
(EulerMeanTimeContinuousTranslation.pathTranslation T a) s.continuousVelocity
The actual reconstructed velocity has a smooth spatial orbit uniformly in time.
theorem
EulerMeanSourceSpatialRegularity.physicalPath_translation_contDiff
(T : ℝ)
(hT : 0 ≤ T)
(ℓ : ℝ)
(hℓ : 0 < ℓ)
(F F₁ H :
EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))
(M0 : EulerMeanCoefficients.BoundedSmoothField (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))
(FInv : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2))
(Be Bc L r : ℝ)
(hBe : 0 ≤ Be)
(hBc : 0 ≤ Bc)
(hL : EulerMeanHarmonic.boundaryLocalizationC1 * Bc ≤ L)
(hr : 0 ≤ r)
(hrquarter : r ≤ 1 / 4)
(hext :
∀ (x : EulerSmoothLimit.Space),
r ≤ ‖ℓ • x‖ → ∀ (v : EulerSmoothLimit.Space), -Be * ‖v‖ ^ 2 ≤ inner ℝ ((M0.field x) v) v)
(hcore :
∀ (x : EulerSmoothLimit.Space),
‖ℓ • x‖ < r → ∀ (v : EulerSmoothLimit.Space), -Bc * ‖v‖ ^ 2 ≤ inner ℝ ((M0.field x) v) v)
(hInv :
∀ (t : ↑(Set.Icc 0 T)) (x : ↥EulerMeanSolenoidal.L2),
(FInv t) (((EulerMeanCoefficients.operatorPath T F.field) t) x) = x)
(hF :
∀ (t : ↑(Set.Icc 0 T)),
HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (EulerMeanCoefficients.operatorPath T F.field))
((EulerMeanCoefficients.operatorPath T F₁.field) t) (Set.Icc 0 T) ↑t)
(hRight :
∀ (t : ↑(Set.Icc 0 T)) (x : ↥EulerMeanSolenoidal.L2),
((EulerMeanCoefficients.operatorPath T F.field) t) ((FInv t) x) = x)
(K : ℝ)
(hK : 0 ≤ K)
(hF0 : FInv ⟨0, ⋯⟩ = ContinuousLinearMap.id ℝ ↥EulerMeanSolenoidal.L2)
(hH : ∀ (t : ↑(Set.Icc 0 T)) (x v : EulerSmoothLimit.Space), inner ℝ (((H.field t) x) v) v ≤ K * ‖v‖ ^ 2)
(hsmall : K * (T ^ 2 / 2) + Be * T + EulerMeanHarmonic.boundaryLocalizationC2 * Bc * r ^ 3 * T ≤ 1 / 2)
(f : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2))
(s :
EulerMeanVariationalInverse.StrongMeanEvolution T hT FInv (EulerMeanCoefficients.operatorPath T F.field)
(EulerMeanCoefficients.operatorPath T F₁.field)
(EulerMeanBoundary.boundaryOperator (EulerMeanBoundary.scaledCutoff ℓ hℓ)) L
(↑((EulerMeanSourceInverse.sourceMeanSolver T hT ℓ hℓ ⇑M0.field ⋯ ‖M0.field‖₊ ⋯ Be Bc L r hBe hBc hL hr hrquarter
hext hcore FInv (EulerMeanCoefficients.operatorPath T H.field) K hK hF0 ⋯ hsmall)
f))
f)
(hTpos : 0 < T)
(hf : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeTranslation T a) f)
(t : ↑(Set.Icc 0 T))
:
ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanSolenoidal.translation a) (s.physicalPath ↑t)
Every actual time slice, including the initial slice, has a smooth spatial translation orbit.
theorem
EulerMeanSourceSpatialRegularity.physicalPath_smooth_representative
(T : ℝ)
(hT : 0 ≤ T)
(ℓ : ℝ)
(hℓ : 0 < ℓ)
(F F₁ H :
EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))
(M0 : EulerMeanCoefficients.BoundedSmoothField (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))
(FInv : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2))
(Be Bc L r : ℝ)
(hBe : 0 ≤ Be)
(hBc : 0 ≤ Bc)
(hL : EulerMeanHarmonic.boundaryLocalizationC1 * Bc ≤ L)
(hr : 0 ≤ r)
(hrquarter : r ≤ 1 / 4)
(hext :
∀ (x : EulerSmoothLimit.Space),
r ≤ ‖ℓ • x‖ → ∀ (v : EulerSmoothLimit.Space), -Be * ‖v‖ ^ 2 ≤ inner ℝ ((M0.field x) v) v)
(hcore :
∀ (x : EulerSmoothLimit.Space),
‖ℓ • x‖ < r → ∀ (v : EulerSmoothLimit.Space), -Bc * ‖v‖ ^ 2 ≤ inner ℝ ((M0.field x) v) v)
(hInv :
∀ (t : ↑(Set.Icc 0 T)) (x : ↥EulerMeanSolenoidal.L2),
(FInv t) (((EulerMeanCoefficients.operatorPath T F.field) t) x) = x)
(hF :
∀ (t : ↑(Set.Icc 0 T)),
HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (EulerMeanCoefficients.operatorPath T F.field))
((EulerMeanCoefficients.operatorPath T F₁.field) t) (Set.Icc 0 T) ↑t)
(hRight :
∀ (t : ↑(Set.Icc 0 T)) (x : ↥EulerMeanSolenoidal.L2),
((EulerMeanCoefficients.operatorPath T F.field) t) ((FInv t) x) = x)
(K : ℝ)
(hK : 0 ≤ K)
(hF0 : FInv ⟨0, ⋯⟩ = ContinuousLinearMap.id ℝ ↥EulerMeanSolenoidal.L2)
(hH : ∀ (t : ↑(Set.Icc 0 T)) (x v : EulerSmoothLimit.Space), inner ℝ (((H.field t) x) v) v ≤ K * ‖v‖ ^ 2)
(hsmall : K * (T ^ 2 / 2) + Be * T + EulerMeanHarmonic.boundaryLocalizationC2 * Bc * r ^ 3 * T ≤ 1 / 2)
(f : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2))
(s :
EulerMeanVariationalInverse.StrongMeanEvolution T hT FInv (EulerMeanCoefficients.operatorPath T F.field)
(EulerMeanCoefficients.operatorPath T F₁.field)
(EulerMeanBoundary.boundaryOperator (EulerMeanBoundary.scaledCutoff ℓ hℓ)) L
(↑((EulerMeanSourceInverse.sourceMeanSolver T hT ℓ hℓ ⇑M0.field ⋯ ‖M0.field‖₊ ⋯ Be Bc L r hBe hBc hL hr hrquarter
hext hcore FInv (EulerMeanCoefficients.operatorPath T H.field) K hK hF0 ⋯ hsmall)
f))
f)
(hTpos : 0 < T)
(hf : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeTranslation T a) f)
(t : ↑(Set.Icc 0 T))
:
∃ (b : EulerSmoothLimit.Space → EulerSmoothLimit.Space),
ContDiff ℝ (↑⊤) b ∧ ↑↑(s.physicalPath ↑t) =ᵐ[MeasureTheory.volume] b
Each physical time slice has a genuine smooth representative on ordinary R³.