A fixed Hilbert derivative space for the actual mean inverse

The fixed space is TimeLp T solenoidalSpace: the terminal condition is built into its primitive and the initial value is free. Forward transport differentiates F times that primitive; backward transport uses the constructed Gram left inverse. These maps are proved inverse, so no parameter-dependent test space is hidden when comparing translated or differentiated coefficients.

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

Actual bounded derivative transport back to the fixed solenoidal Hilbert space.

Equations

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

theorem EulerMeanVariationalInverse.meanBackward_forward (T : ℝ) (hT : 0 ≤ T) (FInv F F₁ : 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) (v : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)) : (meanBackward T hT FInv F F₁ hInv) ((meanTestMap T hT FInv F F₁ hF hInv) v) = v

Forward then backward transport recovers every fixed derivative field.

theorem EulerMeanVariationalInverse.meanForward_backward (T : ℝ) (hT : 0 ≤ T) (FInv F F₁ : 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) (hRight : ∀ (t : ↑(Set.Icc 0 T)) (x : ↥EulerMeanSolenoidal.L2), (F t) ((FInv t) x) = x) (u : ↥(meanDerivatives T hT FInv)) : (meanTestMap T hT FInv F F₁ hF hInv) ((meanBackward T hT FInv F F₁ hInv) u) = u

Backward then forward transport recovers every admissible mean derivative.

noncomputable def EulerMeanVariationalInverse.meanTransportEquiv (T : ℝ) (hT : 0 ≤ T) (FInv F F₁ : 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) (hRight : ∀ (t : ↑(Set.Icc 0 T)) (x : ↥EulerMeanSolenoidal.L2), (F t) ((FInv t) x) = x) : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace) ≃L[ℝ] ↥(meanDerivatives T hT FInv)

A genuine continuous linear equivalence to a coefficient-independent mean space.

Equations

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

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

Explicit polynomial transport cost for the mean fixed-space formulation.

Equations

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

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

The actual transport cost is positive.

theorem EulerMeanVariationalInverse.meanForward_norm_sq_lower (T : ℝ) (hT : 0 ≤ T) (FInv F F₁ : 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) (v : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)) : (meanTransportCost T FInv F F₁)⁻¹ ^ 2 * ‖v‖ ^ 2 ≤ ‖(meanTestMap T hT FInv F F₁ hF hInv) v‖ ^ 2

The forward transport retains a quantitative lower kinetic bound.