The mean variational solve determines its actual initial momentum trace

All solenoidal terminal-H¹ tests, including those nonzero initially, identify an explicit AC momentum representative. Its initial value is the adjoint frame applied to the original M0 + L A boundary force.

@[instance_reducible]

noncomputable def EulerMeanVariationalInverse.instMeanMomentumBoundary1 : NormedAddCommGroup ↥EulerMeanSolenoidal.solenoidalSpace

Cache the standard NormedAddCommGroup solenoidalSpace instance to shorten typeclass synthesis.

Equations

• EulerMeanVariationalInverse.instMeanMomentumBoundary1 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanVariationalInverse.instMeanMomentumBoundary2 : InnerProductSpace ℝ ↥EulerMeanSolenoidal.solenoidalSpace

Cache the standard InnerProductSpace ℝ solenoidalSpace instance to shorten typeclass synthesis.

Equations

• EulerMeanVariationalInverse.instMeanMomentumBoundary2 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanVariationalInverse.instMeanMomentumBoundary3 (T : ℝ) : NormedAddCommGroup ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)

Cache the standard NormedAddCommGroup (TimeLp T L2) instance to shorten typeclass synthesis.

Equations

• EulerMeanVariationalInverse.instMeanMomentumBoundary3 T = inferInstance

@[instance_reducible]

noncomputable def EulerMeanVariationalInverse.instMeanMomentumBoundary4 (T : ℝ) : InnerProductSpace ℝ ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)

Cache the standard InnerProductSpace ℝ (TimeLp T L2) instance to shorten typeclass synthesis.

Equations

• EulerMeanVariationalInverse.instMeanMomentumBoundary4 T = inferInstance

@[instance_reducible]

noncomputable def EulerMeanVariationalInverse.instMeanMomentumBoundary5 (T : ℝ) : NormedAddCommGroup ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)

Cache the standard NormedAddCommGroup (TimeLp T solenoidalSpace) instance to shorten typeclass synthesis.

Equations

• EulerMeanVariationalInverse.instMeanMomentumBoundary5 T = inferInstance

@[instance_reducible]

noncomputable def EulerMeanVariationalInverse.instMeanMomentumBoundary6 (T : ℝ) : InnerProductSpace ℝ ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)

Cache the standard InnerProductSpace ℝ (TimeLp T solenoidalSpace) instance to shorten typeclass synthesis.

Equations

• EulerMeanVariationalInverse.instMeanMomentumBoundary6 T = inferInstance

noncomputable def EulerMeanVariationalInverse.meanBoundaryFlux (T : ℝ) (hT : 0 ≤ T) (FInv F : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (M0 A : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2) (L : ℝ) (u : ↥(meanDerivatives T hT FInv)) : ↥EulerMeanSolenoidal.solenoidalSpace

The original initial boundary force, expressed in the actual solenoidal coordinate space.

Equations

• One or more equations did not get rendered due to their size.

theorem EulerMeanVariationalInverse.meanMomentum_full_weak (T : ℝ) (hT : 0 ≤ T) (FInv F F' : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (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) (H : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (M0 A : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2) (L : ℝ) (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)) (v : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)) : inner ℝ (EulerTransverseMomentumRegularity.momentum T hT (solenoidalFrame T F) ↑u) v + inner ℝ (EulerTransverseMomentumRegularity.momentumForcing T hT (solenoidalFrame T F) (solenoidalFrame T F') H (↑u) f) ((EulerTerminalTimePrimitive.primitiveTimeLp T hT) v) + inner ℝ (meanBoundaryFlux T hT FInv F M0 A L u) ((EulerTerminalTimePrimitive.initialTrace T hT) v) = 0

The full mean weak equation, in actual momentum variables, retains the original boundary force for every genuine solenoidal terminal-H¹ test.

theorem EulerMeanVariationalInverse.meanMomentum_with_initial (T : ℝ) (hT : 0 ≤ T) (FInv F F' : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (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) (H : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (M0 A : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2) (L : ℝ) (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)) : ∃ (p : ℝ → ↥EulerMeanSolenoidal.solenoidalSpace), AbsolutelyContinuousOnInterval p 0 T ∧ p 0 = meanBoundaryFlux T hT FInv F M0 A L u ∧ ↑↑(EulerTransverseMomentumRegularity.momentum T hT (solenoidalFrame T F) ↑u) =ᵐ[EulerTimeLp.timeMeasure T] p ∧ ∀ᵐ (t : ℝ) ∂EulerTimeLp.timeMeasure T, HasDerivAt p (↑↑(EulerTransverseMomentumRegularity.momentumForcing T hT (solenoidalFrame T F) (solenoidalFrame T F') H (↑u) f) t) t

The weak mean solution has a genuine AC momentum representative whose initial value is derived from the original boundary form.

theorem EulerMeanVariationalInverse.meanSolver_momentum_with_initial (T : ℝ) (hT : 0 ≤ T) (FInv F F' : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (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) (H : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (M0 A : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2) (L K B : ℝ) (hK : 0 ≤ K) (hB : 0 ≤ B) (hF0 : FInv ⟨0, ⋯⟩ = ContinuousLinearMap.id ℝ ↥EulerMeanSolenoidal.L2) (hH : ∀ (t : ↑(Set.Icc 0 T)) (z : ↥EulerMeanSolenoidal.L2), inner ℝ ((H t) z) z ≤ K * ‖z‖ ^ 2) (hboundary : ∀ z ∈ EulerMeanSolenoidal.solenoidalSpace, -B * ‖z‖ ^ 2 ≤ inner ℝ (M0 z) z + L * inner ℝ (A z) z) (hsmall : K * (T ^ 2 / 2) + B * T ≤ 1 / 2) (f : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)) : have u := (meanSolver T hT FInv H M0 A L K B hK hB hF0 hH hboundary hsmall) f; ∃ (p : ℝ → ↥EulerMeanSolenoidal.solenoidalSpace), AbsolutelyContinuousOnInterval p 0 T ∧ p 0 = meanBoundaryFlux T hT FInv F M0 A L u ∧ ↑↑(EulerTransverseMomentumRegularity.momentum T hT (solenoidalFrame T F) ↑u) =ᵐ[EulerTimeLp.timeMeasure T] p ∧ ∀ᵐ (t : ℝ) ∂EulerTimeLp.timeMeasure T, HasDerivAt p (↑↑(EulerTransverseMomentumRegularity.momentumForcing T hT (solenoidalFrame T F) (solenoidalFrame T F') H (↑u) f) t) t

The constructed mean inverse therefore has the genuine derived initial momentum trace, before cancellation with the initial deformation derivative.