Actual coefficient adapters for the mean solenoidal frame

A bounded inverse deformation supplies a strictly positive lower frame bound on the ordinary infinite-dimensional solenoidal Hilbert space. The actual mean constraint supplies the range property needed to reconstruct coordinates.

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

A concrete positive Gram lower-bound constant from the actual inverse path.

Equations

• EulerMeanVariationalInverse.meanFrameCoercivity T FInv = ((‖FInv‖ + 1) ^ 2)⁻¹

theorem EulerMeanVariationalInverse.meanFrameCoercivity_pos (T : ℝ) (FInv : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) : 0 < meanFrameCoercivity T FInv

theorem EulerMeanVariationalInverse.solenoidalFrame_lower (T : ℝ) (FInv 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) (t : ↑(Set.Icc 0 T)) (z : ↥EulerMeanSolenoidal.solenoidalSpace) : meanFrameCoercivity T FInv * ‖z‖ ^ 2 ≤ ‖((solenoidalFrame T F) t) z‖ ^ 2

Bounded left inversion of F gives genuine coercivity of the solenoidal frame.

theorem EulerMeanVariationalInverse.meanPrimitive_in_frame_range (T : ℝ) (hT : 0 ≤ T) (FInv F : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (hRight : ∀ (t : ↑(Set.Icc 0 T)) (x : ↥EulerMeanSolenoidal.L2), (F t) ((FInv t) x) = x) (u : ↥(meanDerivatives T hT FInv)) (t : ↑(Set.Icc 0 T)) : ∃ (z : ↥EulerMeanSolenoidal.solenoidalSpace), ((solenoidalFrame T F) t) z = EulerTerminalTimePrimitive.realPrimitive T ↑u ↑t

The actual mean constraint and right inversion place every physical primitive in the range of the solenoidal frame, at every time.

theorem EulerMeanVariationalInverse.solenoidalFrame_ode (T : ℝ) (F F₂ H : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (hODE : ∀ (t : ↑(Set.Icc 0 T)), F₂ t = -H t ∘SL F t) (t : ↑(Set.Icc 0 T)) : (solenoidalFrame T F₂) t = -H t ∘SL (solenoidalFrame T F) t

The genuine deformation ODE descends to its restriction to solenoidal fields.