The actual mean strong equation and initial velocity condition

The time variational solution is upgraded to genuine H² solenoidal coordinates using its derived AC momentum and the constructed coercive Gram inverse. The initial momentum trace then cancels the original M0 boundary term. The final fields contain the actual projected equation (9) and z_t(0)=L A z(0).

structure EulerMeanVariationalInverse.StrongMeanEvolution (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)) : Type

The source's strong mean evolution, with actual time functions and actual Bochner L² acceleration. Every derivative assertion concerns these functions.

• label : ℝ → ↥EulerMeanSolenoidal.solenoidalSpace

  Label of StrongMeanEvolution, of type ℝ → solenoidalSpace.

• velocity : ℝ → ↥EulerMeanSolenoidal.solenoidalSpace

  Velocity field of StrongMeanEvolution, of type ℝ → solenoidalSpace.

• velocityLp : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)

  Velocity Lᵖ of StrongMeanEvolution, of type TimeLp T solenoidalSpace.

• velocity_ae : ↑↑self.velocityLp =ᵐ[EulerTimeLp.timeMeasure T] self.velocity
• acceleration : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)

  Acceleration of StrongMeanEvolution, of type TimeLp T solenoidalSpace.

• label_eq (t : ↑(Set.Icc 0 T)) : ↑(self.label ↑t) = (FInv t) (EulerTerminalTimePrimitive.realPrimitive T u ↑t)
• label_ac : AbsolutelyContinuousOnInterval self.label 0 T
• velocity_ac : AbsolutelyContinuousOnInterval self.velocity 0 T
• terminal : self.label T = 0
• initial_velocity : ↑(self.velocity 0) = L • A ↑(self.label 0)
• label_derivative : ∀ᵐ (t : ℝ) ∂EulerTimeLp.timeMeasure T, HasDerivAt self.label (self.velocity t) t
• velocity_derivative : ∀ᵐ (t : ℝ) ∂EulerTimeLp.timeMeasure T, HasDerivAt self.velocity (↑↑self.acceleration t) t
• equation : ∀ᵐ (t : ℝ) ∂EulerTimeLp.timeMeasure T, EulerMeanSolenoidal.solenoidalProjection ((ContinuousLinearMap.adjoint (EulerVolterraConvolution.extendPath T hT F t)) ((EulerVolterraConvolution.extendPath T hT F t) ↑(↑↑self.acceleration t))) = EulerMeanSolenoidal.solenoidalProjection ((ContinuousLinearMap.adjoint (EulerVolterraConvolution.extendPath T hT F t)) (↑↑f t - 2 • (EulerVolterraConvolution.extendPath T hT F₁ t) ↑(self.velocity t)))

theorem EulerMeanVariationalInverse.initial_momentum_cancellation (F₀ F₁ M0 A : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2) (L : ℝ) (hF₀ : F₀ = ContinuousLinearMap.id ℝ ↥EulerMeanSolenoidal.L2) (hF₁ : F₁ = M0) (z v : ↥EulerMeanSolenoidal.solenoidalSpace) (hAz : A ↑z ∈ EulerMeanSolenoidal.solenoidalSpace) (hm : (EulerTransverseGramInverse.gram (F₀ ∘SL EulerMeanSolenoidal.solenoidalSpace.subtypeL)) v + (ContinuousLinearMap.adjoint (F₀ ∘SL EulerMeanSolenoidal.solenoidalSpace.subtypeL)) (F₁ ↑z) = (ContinuousLinearMap.adjoint (F₀ ∘SL EulerMeanSolenoidal.solenoidalSpace.subtypeL)) ((M0 + L • A) ↑z)) : ↑v = L • A ↑z

At the initial identity frame, the derived momentum condition cancels M0. The range assumption here is only the genuine solenoidal range of A.

theorem EulerMeanVariationalInverse.ordinary_projected_equation (F F₁ : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2) (f : ↥EulerMeanSolenoidal.L2) (a v : ↥EulerMeanSolenoidal.solenoidalSpace) (h : (EulerTransverseGramInverse.gram (F ∘SL EulerMeanSolenoidal.solenoidalSpace.subtypeL)) a = (ContinuousLinearMap.adjoint (F ∘SL EulerMeanSolenoidal.solenoidalSpace.subtypeL)) (f - 2 • F₁ ↑v)) : EulerMeanSolenoidal.solenoidalProjection ((ContinuousLinearMap.adjoint F) (F ↑a)) = EulerMeanSolenoidal.solenoidalProjection ((ContinuousLinearMap.adjoint F) (f - 2 • F₁ ↑v))

A frame Gram equation on L²σ is exactly the ordinary projected spatial equation.

theorem EulerMeanVariationalInverse.meanWeakSolution_strong (T : ℝ) (hT : 0 ≤ T) (FInv F F₁ F₂ H : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (M0 A : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2) (L : ℝ) (hF : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT F) (F₁ t) (Set.Icc 0 T) ↑t) (hF₁ : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT F₁) (F₂ t) (Set.Icc 0 T) ↑t) (hInv : ∀ (t : ↑(Set.Icc 0 T)) (x : ↥EulerMeanSolenoidal.L2), (FInv t) ((F t) x) = x) (hRight : ∀ (t : ↑(Set.Icc 0 T)) (x : ↥EulerMeanSolenoidal.L2), (F t) ((FInv t) x) = x) (hFInv₀ : FInv ⟨0, ⋯⟩ = ContinuousLinearMap.id ℝ ↥EulerMeanSolenoidal.L2) (hF₁₀ : F₁ ⟨0, ⋯⟩ = M0) (hODE : ∀ (t : ↑(Set.Icc 0 T)), F₂ t = -H t ∘SL F t) (hAσ : ∀ z ∈ EulerMeanSolenoidal.solenoidalSpace, A z ∈ EulerMeanSolenoidal.solenoidalSpace) (u : ↥(meanDerivatives T hT FInv)) (f : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)) (hu : ∀ (w : ↥(meanDerivatives T hT FInv)), inner ℝ ↑u ↑w - inner ℝ ((EulerTimeLp.timeMultiplier T hT H) ((meanPrimitive T hT FInv) u)) ((meanPrimitive T hT FInv) w) + inner ℝ (M0 ((meanTrace T hT FInv) u)) ((meanTrace T hT FInv) w) + L * inner ℝ (A ((meanTrace T hT FInv) u)) ((meanTrace T hT FInv) w) = -inner ℝ f ((meanPrimitive T hT FInv) w)) : Nonempty (StrongMeanEvolution T hT FInv F F₁ A L (↑u) f)

A genuine mean weak solution has actual H² label coordinates, the literal projected equation, and the original initial velocity condition.