The actual mean variational inverse on a fixed Hilbert space

The fixed space is ordinary solenoidal Bochner L² time. The transported operator contains the original kinetic, potential, and nonlocal initial-trace terms. Its coercive inverse is constructed and identified with the original mean solve, so coefficient comparisons can use a common domain without assuming an inverse.

@[instance_reducible]

noncomputable def EulerMeanFixedSpaceInverse.instMeanFixedSpaceInverse1 : NormedAddCommGroup ↥EulerMeanSolenoidal.solenoidalSpace

Cache the standard NormedAddCommGroup solenoidalSpace instance to shorten typeclass synthesis.

Equations

• EulerMeanFixedSpaceInverse.instMeanFixedSpaceInverse1 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanFixedSpaceInverse.instMeanFixedSpaceInverse2 : InnerProductSpace ℝ ↥EulerMeanSolenoidal.solenoidalSpace

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

Equations

• EulerMeanFixedSpaceInverse.instMeanFixedSpaceInverse2 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanFixedSpaceInverse.instMeanFixedSpaceInverse3 (T : ℝ) : NormedAddCommGroup ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)

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

Equations

• EulerMeanFixedSpaceInverse.instMeanFixedSpaceInverse3 T = inferInstance

@[instance_reducible]

noncomputable def EulerMeanFixedSpaceInverse.instMeanFixedSpaceInverse4 (T : ℝ) : InnerProductSpace ℝ ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)

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

Equations

• EulerMeanFixedSpaceInverse.instMeanFixedSpaceInverse4 T = inferInstance

@[instance_reducible]

noncomputable def EulerMeanFixedSpaceInverse.instMeanFixedSpaceInverse5 (T : ℝ) : NormedAddCommGroup ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)

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

Equations

• EulerMeanFixedSpaceInverse.instMeanFixedSpaceInverse5 T = inferInstance

@[instance_reducible]

noncomputable def EulerMeanFixedSpaceInverse.instMeanFixedSpaceInverse6 (T : ℝ) : InnerProductSpace ℝ ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)

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

Equations

• EulerMeanFixedSpaceInverse.instMeanFixedSpaceInverse6 T = inferInstance

noncomputable def EulerMeanFixedSpaceInverse.fixedMeanDerivative (T : ℝ) (hT : 0 ≤ T) (F F₁ : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace) →L[ℝ] ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)

Actual physical derivative on the fixed solenoidal coordinate space.

Equations

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

noncomputable def EulerMeanFixedSpaceInverse.fixedMeanPrimitive (T : ℝ) (hT : 0 ≤ T) (F F₁ : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace) →L[ℝ] ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)

Actual physical displacement on the fixed coordinate space.

Equations

• EulerMeanFixedSpaceInverse.fixedMeanPrimitive T hT F F₁ = EulerTerminalTimePrimitive.primitiveTimeLp T hT ∘SL EulerMeanFixedSpaceInverse.fixedMeanDerivative T hT F F₁

noncomputable def EulerMeanFixedSpaceInverse.fixedMeanTrace (T : ℝ) (hT : 0 ≤ T) (F F₁ : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace) →L[ℝ] ↥EulerMeanSolenoidal.L2

Actual physical initial trace on the fixed coordinate space.

Equations

• EulerMeanFixedSpaceInverse.fixedMeanTrace T hT F F₁ = EulerTerminalTimePrimitive.initialTrace T hT ∘SL EulerMeanFixedSpaceInverse.fixedMeanDerivative T hT F F₁

noncomputable def EulerMeanFixedSpaceInverse.fixedMeanOperator (T : ℝ) (hT : 0 ≤ T) (F F₁ H : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (M0 A : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2) (L : ℝ) : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace) →L[ℝ] ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)

The full original mean form as an operator on one fixed Hilbert space.

Equations

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

theorem EulerMeanFixedSpaceInverse.fixedMeanOperator_inner (T : ℝ) (hT : 0 ≤ T) (F F₁ H : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (M0 A : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2) (L : ℝ) (u v : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)) : inner ℝ ((fixedMeanOperator T hT F F₁ H M0 A L) u) v = inner ℝ ((fixedMeanDerivative T hT F F₁) u) ((fixedMeanDerivative T hT F F₁) v) - inner ℝ ((EulerTimeLp.timeMultiplier T hT H) ((fixedMeanPrimitive T hT F F₁) u)) ((fixedMeanPrimitive T hT F F₁) v) + inner ℝ ((M0 + L • A) ((fixedMeanTrace T hT F F₁) u)) ((fixedMeanTrace T hT F F₁) v)

The transported operator has precisely the original mean bilinear form.

noncomputable def EulerMeanFixedSpaceInverse.fixedMeanCoercivity (T : ℝ) (F F₁ FInv : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) : ℝ

An explicit positive coercivity constant from the proved mean transport bound.

Equations

• EulerMeanFixedSpaceInverse.fixedMeanCoercivity T F F₁ FInv = (EulerMeanVariationalInverse.meanTransportCost T FInv F F₁)⁻¹ ^ 2 / 2

theorem EulerMeanFixedSpaceInverse.fixedMeanCoercivity_pos (T : ℝ) (hT : 0 ≤ T) (F F₁ FInv : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) : 0 < fixedMeanCoercivity T F F₁ FInv

The fixed-space coercivity constant is positive.

theorem EulerMeanFixedSpaceInverse.fixedMeanOperator_coercive (T : ℝ) (hT : 0 ≤ T) (F F₁ H : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (M0 A : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2) (L : ℝ) (FInv : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (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) (K B : ℝ) (hK : 0 ≤ K) (hB : 0 ≤ B) (hFInv₀ : 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) (v : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)) : fixedMeanCoercivity T F F₁ FInv * ‖v‖ ^ 2 ≤ inner ℝ ((fixedMeanOperator T hT F F₁ H M0 A L) v) v

The source smallness and actual transport bounds prove fixed-space coercivity.

noncomputable def EulerMeanFixedSpaceInverse.fixedMeanInverse (T : ℝ) (hT : 0 ≤ T) (F F₁ H : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (M0 A : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2) (L : ℝ) (FInv : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (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) (K B : ℝ) (hK : 0 ≤ K) (hB : 0 ≤ B) (hFInv₀ : 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.solenoidalSpace) →L[ℝ] ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)

The actual fixed-space inverse operator.

Equations

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

noncomputable def EulerMeanFixedSpaceInverse.fixedMeanSolver (T : ℝ) (hT : 0 ≤ T) (F F₁ H : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (M0 A : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2) (L : ℝ) (FInv : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (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) (K B : ℝ) (hK : 0 ≤ K) (hB : 0 ≤ B) (hFInv₀ : 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[ℝ] ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)

The actual forcing-to-coordinate-derivative map on the fixed space.

Equations

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

theorem EulerMeanFixedSpaceInverse.fixedMeanInverse_norm (T : ℝ) (hT : 0 ≤ T) (F F₁ H : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (M0 A : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2) (L : ℝ) (FInv : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (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) (K B : ℝ) (hK : 0 ≤ K) (hB : 0 ≤ B) (hFInv₀ : 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) : ‖fixedMeanInverse T hT F F₁ H M0 A L FInv hInv hF K B hK hB hFInv₀ hH hboundary hsmall‖ ≤ (fixedMeanCoercivity T F F₁ FInv)⁻¹

The fixed inverse has its actual quantitative coercive norm bound.

theorem EulerMeanFixedSpaceInverse.fixedMeanSolver_weak (T : ℝ) (hT : 0 ≤ T) (F F₁ H : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (M0 A : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2) (L : ℝ) (FInv : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (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) (K B : ℝ) (hK : 0 ≤ K) (hB : 0 ≤ B) (hFInv₀ : 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 : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)) : have u := (fixedMeanSolver T hT F F₁ H M0 A L FInv hInv hF K B hK hB hFInv₀ hH hboundary hsmall) f; inner ℝ ((fixedMeanDerivative T hT F F₁) u) ((fixedMeanDerivative T hT F F₁) v) - inner ℝ ((EulerTimeLp.timeMultiplier T hT H) ((fixedMeanPrimitive T hT F F₁) u)) ((fixedMeanPrimitive T hT F F₁) v) + inner ℝ ((M0 + L • A) ((fixedMeanTrace T hT F F₁) u)) ((fixedMeanTrace T hT F F₁) v) = -inner ℝ f ((fixedMeanPrimitive T hT F F₁) v)

The constructed fixed-space solution satisfies the full original form.

theorem EulerMeanFixedSpaceInverse.fixedMeanSolver_unique (T : ℝ) (hT : 0 ≤ T) (F F₁ H : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (M0 A : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2) (L : ℝ) (FInv : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (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) (K B : ℝ) (hK : 0 ≤ K) (hB : 0 ≤ B) (hFInv₀ : 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 : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)) (hu : ∀ (v : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)), inner ℝ ((fixedMeanDerivative T hT F F₁) u) ((fixedMeanDerivative T hT F F₁) v) - inner ℝ ((EulerTimeLp.timeMultiplier T hT H) ((fixedMeanPrimitive T hT F F₁) u)) ((fixedMeanPrimitive T hT F F₁) v) + inner ℝ ((M0 + L • A) ((fixedMeanTrace T hT F F₁) u)) ((fixedMeanTrace T hT F F₁) v) = -inner ℝ f ((fixedMeanPrimitive T hT F F₁) v)) : u = (fixedMeanSolver T hT F F₁ H M0 A L FInv hInv hF K B hK hB hFInv₀ hH hboundary hsmall) f

Uniqueness is on the same fixed Hilbert space.

theorem EulerMeanFixedSpaceInverse.fixedMeanSolver_eq_mean (T : ℝ) (hT : 0 ≤ T) (F F₁ H : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (M0 A : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2) (L : ℝ) (FInv : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (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) (K B : ℝ) (hK : 0 ≤ K) (hB : 0 ≤ B) (hFInv₀ : 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) (hRight : ∀ (t : ↑(Set.Icc 0 T)) (x : ↥EulerMeanSolenoidal.L2), (F t) ((FInv t) x) = x) (f : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)) : (fixedMeanSolver T hT F F₁ H M0 A L FInv hInv hF K B hK hB hFInv₀ hH hboundary hsmall) f = (EulerMeanVariationalInverse.meanBackward T hT FInv F F₁ hInv) ((EulerMeanVariationalInverse.meanSolver T hT FInv H M0 A L K B hK hB hFInv₀ hH hboundary hsmall) f)

The fixed inverse is precisely the coordinate transport of the original actual solve.