A genuine mean time-variational inverse on ordinary spatial L²

The Hilbert variable is the time derivative of the physical displacement η. Terminal integration constructs η, and the closed constraints require FInv(t) η(t) to be an actual ordinary-space solenoidal field at every time. The exact initial form is M0 + L A, not a replacement boundary condition.

The lower bound for this given boundary operator on solenoidal fields remains an explicit input. In the source it must be proved from the concrete cutoff operator and harmonic localization. This file does not claim that step, the strong interior equation, or the initial derivative boundary identity. The recovered z=FInv η is continuous here; its H¹ regularity additionally uses the source's C¹-in-time inverse deformation.

def EulerMeanVariationalInverse.meanDerivatives (T : ℝ) (hT : 0 ≤ T) (FInv : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) : Submodule ℝ ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)

Derivatives whose actual terminal primitives obey the solenoidal label constraint.

Equations

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

theorem EulerMeanVariationalInverse.derivative_mem_of_ac (T : ℝ) (hT : 0 ≤ T) (FInv : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (u : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)) (η : ℝ → ↥EulerMeanSolenoidal.L2) (hη : AbsolutelyContinuousOnInterval η 0 T) (hder : ∀ᵐ (t : ℝ) ∂EulerTimeLp.timeMeasure T, HasDerivAt η (↑↑u t) t) (hterminal : η T = 0) (hsolenoidal : ∀ (t : ↑(Set.Icc 0 T)), (FInv t) (η ↑t) ∈ EulerMeanSolenoidal.solenoidalSpace) : u ∈ meanDerivatives T hT FInv

Every genuine absolutely continuous terminal-zero path with an L² derivative and the label-solenoidal constraint is represented in this Hilbert space.

theorem EulerMeanVariationalInverse.meanDerivatives_closed (T : ℝ) (hT : 0 ≤ T) (FInv : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) : IsClosed ↑(meanDerivatives T hT FInv)

Every time constraint is the preimage of the actual closed solenoidal subspace.

instance EulerMeanVariationalInverse.meanDerivatives_complete (T : ℝ) (hT : 0 ≤ T) (FInv : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) : CompleteSpace ↥(meanDerivatives T hT FInv)

The genuine closed constraint space is a complete Hilbert space.

noncomputable def EulerMeanVariationalInverse.meanPrimitive (T : ℝ) (hT : 0 ≤ T) (FInv : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) : ↥(meanDerivatives T hT FInv) →L[ℝ] ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)

The actual displacement primitive, restricted to the mean constraint space.

Equations

• EulerMeanVariationalInverse.meanPrimitive T hT FInv = EulerTerminalTimePrimitive.primitiveTimeLp T hT ∘SL (EulerMeanVariationalInverse.meanDerivatives T hT FInv).subtypeL

noncomputable def EulerMeanVariationalInverse.meanTrace (T : ℝ) (hT : 0 ≤ T) (FInv : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) : ↥(meanDerivatives T hT FInv) →L[ℝ] ↥EulerMeanSolenoidal.L2

The actual initial trace on that same constraint space.

Equations

• EulerMeanVariationalInverse.meanTrace T hT FInv = EulerTerminalTimePrimitive.initialTrace T hT ∘SL (EulerMeanVariationalInverse.meanDerivatives T hT FInv).subtypeL

theorem EulerMeanVariationalInverse.meanPrimitive_norm_sq (T : ℝ) (hT : 0 ≤ T) (FInv : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (u : ↥(meanDerivatives T hT FInv)) : ‖(meanPrimitive T hT FInv) u‖ ^ 2 ≤ T ^ 2 / 2 * ‖u‖ ^ 2

The sharp source Poincaré estimate survives restriction to the constraint space.

theorem EulerMeanVariationalInverse.meanTrace_norm_sq (T : ℝ) (hT : 0 ≤ T) (FInv : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (u : ↥(meanDerivatives T hT FInv)) : ‖(meanTrace T hT FInv) u‖ ^ 2 ≤ T * ‖u‖ ^ 2

The source initial trace estimate is an estimate of this literal trace.

theorem EulerMeanVariationalInverse.meanTrace_mem (T : ℝ) (hT : 0 ≤ T) (FInv : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (hF0 : FInv ⟨0, ⋯⟩ = ContinuousLinearMap.id ℝ ↥EulerMeanSolenoidal.L2) (u : ↥(meanDerivatives T hT FInv)) : (meanTrace T hT FInv) u ∈ EulerMeanSolenoidal.solenoidalSpace

The normalization of the deformation makes the initial physical trace solenoidal.

theorem EulerMeanVariationalInverse.meanTrace_boundary (T : ℝ) (hT : 0 ≤ T) (FInv : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (M0 A : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2) (L B : ℝ) (hF0 : FInv ⟨0, ⋯⟩ = ContinuousLinearMap.id ℝ ↥EulerMeanSolenoidal.L2) (hboundary : ∀ z ∈ EulerMeanSolenoidal.solenoidalSpace, -B * ‖z‖ ^ 2 ≤ inner ℝ (M0 z) z + L * inner ℝ (A z) z) (u : ↥(meanDerivatives T hT FInv)) : -B * ‖(meanTrace T hT FInv) u‖ ^ 2 ≤ inner ℝ ((M0 + L • A) ((meanTrace T hT FInv) u)) ((meanTrace T hT FInv) u)

Only the boundary lower bound on actual solenoidal traces is needed.

theorem EulerMeanVariationalInverse.meanPrimitive_norm_le (T : ℝ) (hT : 0 ≤ T) (FInv : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) : ‖meanPrimitive T hT FInv‖ ≤ T

A polynomial operator bound for the actual terminal primitive.

theorem EulerMeanVariationalInverse.meanPrimitive_ae (T : ℝ) (hT : 0 ≤ T) (FInv : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (u : ↥(meanDerivatives T hT FInv)) : ↑↑((meanPrimitive T hT FInv) u) =ᵐ[EulerTimeLp.timeMeasure T] EulerTerminalTimePrimitive.realPrimitive T ↑u

The mean-space primitive has the same genuine integral representative.

theorem EulerMeanVariationalInverse.meanPotential_inner_eq_integral (T : ℝ) (hT : 0 ≤ T) (FInv H : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (u v : ↥(meanDerivatives T hT FInv)) : inner ℝ ((EulerTimeLp.timeMultiplier T hT H) ((meanPrimitive T hT FInv) u)) ((meanPrimitive T hT FInv) v) = ∫ (t : ℝ), inner ℝ ((H (Set.projIcc 0 T hT t)) (EulerTerminalTimePrimitive.realPrimitive T (↑u) t)) (EulerTerminalTimePrimitive.realPrimitive T (↑v) t) ∂EulerTimeLp.timeMeasure T

The potential pairing is the literal time integral on the actual displacement paths.

theorem EulerMeanVariationalInverse.meanForcing_inner_eq_integral (T : ℝ) (hT : 0 ≤ T) (FInv : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (f : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)) (v : ↥(meanDerivatives T hT FInv)) : inner ℝ f ((meanPrimitive T hT FInv) v) = ∫ (t : ℝ), inner ℝ (↑↑f t) (EulerTerminalTimePrimitive.realPrimitive T (↑v) t) ∂EulerTimeLp.timeMeasure T

The forcing pairing is the literal time integral against the actual test displacement.

theorem EulerMeanVariationalInverse.weak_integral_of_weak (T : ℝ) (hT : 0 ≤ T) (FInv H : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (M0 A : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2) (L : ℝ) (u v : ↥(meanDerivatives T hT FInv)) (f : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)) (h : inner ℝ ↑u ↑v - inner ℝ ((EulerTimeLp.timeMultiplier T hT H) ((meanPrimitive T hT FInv) u)) ((meanPrimitive T hT FInv) v) + inner ℝ (M0 ((meanTrace T hT FInv) u)) ((meanTrace T hT FInv) v) + L * inner ℝ (A ((meanTrace T hT FInv) u)) ((meanTrace T hT FInv) v) = -inner ℝ f ((meanPrimitive T hT FInv) v)) : ∫ (t : ℝ), inner ℝ (↑↑↑u t) (↑↑↑v t) ∂EulerTimeLp.timeMeasure T - ∫ (t : ℝ), inner ℝ ((H (Set.projIcc 0 T hT t)) (EulerTerminalTimePrimitive.realPrimitive T (↑u) t)) (EulerTerminalTimePrimitive.realPrimitive T (↑v) t) ∂EulerTimeLp.timeMeasure T + inner ℝ (M0 ((meanTrace T hT FInv) u)) ((meanTrace T hT FInv) v) + L * inner ℝ (A ((meanTrace T hT FInv) u)) ((meanTrace T hT FInv) v) = -∫ (t : ℝ), inner ℝ (↑↑f t) (EulerTerminalTimePrimitive.realPrimitive T (↑v) t) ∂EulerTimeLp.timeMeasure T

Rewriting the form as actual time integrals is independent of how its argument was constructed. This also keeps the integral interface lightweight.

noncomputable def EulerMeanVariationalInverse.meanSolver (T : ℝ) (hT : 0 ≤ T) (FInv 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) : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2) →L[ℝ] ↥(meanDerivatives T hT FInv)

The mean forcing-to-displacement-derivative map is constructed by Lax--Milgram.

Equations

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

noncomputable def EulerMeanVariationalInverse.meanEta (T : ℝ) (hT : 0 ≤ T) (FInv 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) : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2) →L[ℝ] C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2)

The physical displacement is the actual terminal primitive of the solved derivative.

Equations

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

noncomputable def EulerMeanVariationalInverse.meanDisplacement (T : ℝ) (hT : 0 ≤ T) (FInv 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)) : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2)

Recover the actual continuous solenoidal label displacement z=FInv η.

Equations

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

theorem EulerMeanVariationalInverse.meanDisplacement_solenoidal (T : ℝ) (hT : 0 ≤ T) (FInv 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)) (t : ↑(Set.Icc 0 T)) : (meanDisplacement T hT FInv H M0 A L K B hK hB hF0 hH hboundary hsmall f) t ∈ EulerMeanSolenoidal.solenoidalSpace

The recovered label displacement is genuinely solenoidal at every time.

theorem EulerMeanVariationalInverse.meanEta_terminal (T : ℝ) (hT : 0 ≤ T) (FInv 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)) : ((meanEta T hT FInv H M0 A L K B hK hB hF0 hH hboundary hsmall) f) ⟨T, ⋯⟩ = 0

The actual physical displacement has zero terminal trace.

theorem EulerMeanVariationalInverse.meanDisplacement_terminal (T : ℝ) (hT : 0 ≤ T) (FInv 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)) : (meanDisplacement T hT FInv H M0 A L K B hK hB hF0 hH hboundary hsmall f) ⟨T, ⋯⟩ = 0

The recovered label displacement also has zero terminal trace.

theorem EulerMeanVariationalInverse.meanEta_hasDerivAt_ae (T : ℝ) (hT : 0 ≤ T) (FInv 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)) : ∀ᵐ (t : ℝ) ∂EulerTimeLp.timeMeasure T, HasDerivAt (EulerTerminalTimePrimitive.realPrimitive T ↑((meanSolver T hT FInv H M0 A L K B hK hB hF0 hH hboundary hsmall) f)) (↑↑↑((meanSolver T hT FInv H M0 A L K B hK hB hF0 hH hboundary hsmall) f) t) t

The solved derivative is the actual a.e. derivative of the physical displacement.

theorem EulerMeanVariationalInverse.meanEta_absolutelyContinuous (T : ℝ) (hT : 0 ≤ T) (FInv 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)) : AbsolutelyContinuousOnInterval (EulerTerminalTimePrimitive.realPrimitive T ↑((meanSolver T hT FInv H M0 A L K B hK hB hF0 hH hboundary hsmall) f)) 0 T

The physical displacement is a genuine absolutely continuous time path.

theorem EulerMeanVariationalInverse.meanSolver_weak (T : ℝ) (hT : 0 ≤ T) (FInv 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)) (v : ↥(meanDerivatives T hT FInv)) : have u := (meanSolver T hT FInv H M0 A L K B hK hB hF0 hH hboundary hsmall) f; inner ℝ ↑u ↑v - inner ℝ ((EulerTimeLp.timeMultiplier T hT H) ((meanPrimitive T hT FInv) u)) ((meanPrimitive T hT FInv) v) + inner ℝ (M0 ((meanTrace T hT FInv) u)) ((meanTrace T hT FInv) v) + L * inner ℝ (A ((meanTrace T hT FInv) u)) ((meanTrace T hT FInv) v) = -inner ℝ f ((meanPrimitive T hT FInv) v)

The exact mean form with the two original initial boundary terms.

theorem EulerMeanVariationalInverse.meanSolver_norm (T : ℝ) (hT : 0 ≤ T) (FInv 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)) : ‖(meanSolver T hT FInv H M0 A L K B hK hB hF0 hH hboundary hsmall) f‖ ≤ 2 * T * ‖f‖

The solved mean derivative obeys a polynomial finite-time norm bound.

theorem EulerMeanVariationalInverse.meanSolver_weak_integral (T : ℝ) (hT : 0 ≤ T) (FInv 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)) (v : ↥(meanDerivatives T hT FInv)) : have u := (meanSolver T hT FInv H M0 A L K B hK hB hF0 hH hboundary hsmall) f; ∫ (t : ℝ), inner ℝ (↑↑↑u t) (↑↑↑v t) ∂EulerTimeLp.timeMeasure T - ∫ (t : ℝ), inner ℝ ((H (Set.projIcc 0 T hT t)) (EulerTerminalTimePrimitive.realPrimitive T (↑u) t)) (EulerTerminalTimePrimitive.realPrimitive T (↑v) t) ∂EulerTimeLp.timeMeasure T + inner ℝ (M0 ((meanTrace T hT FInv) u)) ((meanTrace T hT FInv) v) + L * inner ℝ (A ((meanTrace T hT FInv) u)) ((meanTrace T hT FInv) v) = -∫ (t : ℝ), inner ℝ (↑↑f t) (EulerTerminalTimePrimitive.realPrimitive T (↑v) t) ∂EulerTimeLp.timeMeasure T

The weak equation is an equality of genuine time integrals, including the two actual initial boundary terms from the source.

theorem EulerMeanVariationalInverse.meanSolver_unique (T : ℝ) (hT : 0 ≤ T) (FInv 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)) (u : ↥(meanDerivatives T hT FInv)) (hu : ∀ (v : ↥(meanDerivatives T hT FInv)), inner ℝ ↑u ↑v - inner ℝ ((EulerTimeLp.timeMultiplier T hT H) ((meanPrimitive T hT FInv) u)) ((meanPrimitive T hT FInv) v) + inner ℝ (M0 ((meanTrace T hT FInv) u)) ((meanTrace T hT FInv) v) + L * inner ℝ (A ((meanTrace T hT FInv) u)) ((meanTrace T hT FInv) v) = -inner ℝ f ((meanPrimitive T hT FInv) v)) : u = (meanSolver T hT FInv H M0 A L K B hK hB hF0 hH hboundary hsmall) f

No other admissible derivative solves this same genuine mean form.

theorem EulerMeanVariationalInverse.existsUnique_mean_weak_solution (T : ℝ) (hT : 0 ≤ T) (FInv 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)) : ∃! u : ↥(meanDerivatives T hT FInv), ∀ (v : ↥(meanDerivatives T hT FInv)), inner ℝ ↑u ↑v - inner ℝ ((EulerTimeLp.timeMultiplier T hT H) ((meanPrimitive T hT FInv) u)) ((meanPrimitive T hT FInv) v) + inner ℝ (M0 ((meanTrace T hT FInv) u)) ((meanTrace T hT FInv) v) + L * inner ℝ (A ((meanTrace T hT FInv) u)) ((meanTrace T hT FInv) v) = -inner ℝ f ((meanPrimitive T hT FInv) v)

Existence and uniqueness for the source's mean form, conditional on the explicit coefficient and solenoidal boundary lower bounds.