Genuine H¹ label displacements and mean variational tests

The mean Hilbert model uses derivatives of the physical displacement. A C¹ inverse deformation converts its terminal primitive to an actual H¹ solenoidal label path, with a constructed Bochner L² derivative. Conversely, each genuine solenoidal terminal primitive yields an admissible physical test through F.

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

The actual L² time derivative of the label path FInv η.

Equations

• EulerMeanVariationalInverse.labelDerivative T hT FInv FInv' = EulerTimeH1OperatorProduct.productDerivative T hT FInv FInv' ∘SL (EulerMeanVariationalInverse.meanDerivatives T hT FInv).subtypeL

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

The real representative of the label displacement.

Equations

• EulerMeanVariationalInverse.labelPath T hT FInv u = EulerTimeH1OperatorProduct.productPrimitive T hT FInv ↑u

theorem EulerMeanVariationalInverse.labelPath_solenoidal (T : ℝ) (hT : 0 ≤ T) (FInv : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (u : ↥(meanDerivatives T hT FInv)) (t : ℝ) (ht : t ∈ Set.Icc 0 T) : labelPath T hT FInv u t ∈ EulerMeanSolenoidal.solenoidalSpace

The label path takes values in the actual ordinary solenoidal space.

theorem EulerMeanVariationalInverse.labelPath_absolutelyContinuous (T : ℝ) (hT : 0 ≤ T) (FInv FInv' : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (hFInv : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT FInv) (FInv' t) (Set.Icc 0 T) ↑t) (u : ↥(meanDerivatives T hT FInv)) : AbsolutelyContinuousOnInterval (labelPath T hT FInv u) 0 T

The actual label displacement is absolutely continuous.

theorem EulerMeanVariationalInverse.labelPath_hasDerivAt_ae (T : ℝ) (hT : 0 ≤ T) (FInv FInv' : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (hFInv : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT FInv) (FInv' t) (Set.Icc 0 T) ↑t) (u : ↥(meanDerivatives T hT FInv)) : ∀ᵐ (t : ℝ) ∂EulerTimeLp.timeMeasure T, HasDerivAt (labelPath T hT FInv u) (↑↑((labelDerivative T hT FInv FInv') u) t) t

Its L² derivative is obtained from the literal product rule.

theorem EulerMeanVariationalInverse.labelPath_eq_realPrimitive (T : ℝ) (hT : 0 ≤ T) (FInv FInv' : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (hFInv : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT FInv) (FInv' t) (Set.Icc 0 T) ↑t) (u : ↥(meanDerivatives T hT FInv)) (t : ℝ) (ht : t ∈ Set.Icc 0 T) : labelPath T hT FInv u t = EulerTerminalTimePrimitive.realPrimitive T ((labelDerivative T hT FInv FInv') u) t

Integration recovers the actual H¹ label path from that derivative.

theorem EulerMeanVariationalInverse.labelDerivative_solenoidal_ae (T : ℝ) (hT : 0 ≤ T) (FInv FInv' : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (hFInv : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT FInv) (FInv' t) (Set.Icc 0 T) ↑t) (u : ↥(meanDerivatives T hT FInv)) : ∀ᵐ (t : ℝ) ∂EulerTimeLp.timeMeasure T, ↑↑((labelDerivative T hT FInv FInv') u) t ∈ EulerMeanSolenoidal.solenoidalSpace

Differentiating a path in the closed solenoidal subspace preserves its constraint almost everywhere; this is an actual L² membership statement.

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

The norm comparison required by the source H¹ model follows from the actual coefficient bounds and the sharp terminal Poincaré bound.

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

Squaring the genuine derivative comparison gives the source energy control.

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

Restrict the physical deformation to actual solenoidal label fields.

Equations

• EulerMeanVariationalInverse.solenoidalFrame T F = { toFun := fun (t : ↑(Set.Icc 0 T)) => F t ∘SL EulerMeanSolenoidal.solenoidalSpace.subtypeL, continuous_toFun := ⋯ }

theorem EulerMeanVariationalInverse.solenoidalFrame_hasDerivWithinAt (T : ℝ) (hT : 0 ≤ T) (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) (t : ↑(Set.Icc 0 T)) : HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (solenoidalFrame T F)) ((solenoidalFrame T F') t) (Set.Icc 0 T) ↑t

Differentiating the restricted frame is literal bounded-map composition.

theorem EulerMeanVariationalInverse.productDerivative_mem_mean (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) (v : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)) : (EulerTimeH1OperatorProduct.productDerivative T hT (solenoidalFrame T F) (solenoidalFrame T F')) v ∈ meanDerivatives T hT FInv

Every solenoidal terminal H¹ path supplies an admissible physical test.

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

A genuine bounded map from solenoidal label derivatives to admissible mean tests.

Equations

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

@[simp]

theorem EulerMeanVariationalInverse.meanTestMap_coe (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) (v : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)) : ↑((meanTestMap T hT FInv F F' hF hInv) v) = (EulerTimeH1OperatorProduct.productDerivative T hT (solenoidalFrame T F) (solenoidalFrame T F')) v

The test derivative is the actual product-rule L² field.

theorem EulerMeanVariationalInverse.meanTestMap_primitive (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) (v : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)) : (meanPrimitive T hT FInv) ((meanTestMap T hT FInv F F' hF hInv) v) = (EulerTimeLp.timeMultiplier T hT (solenoidalFrame T F)) ((EulerTerminalTimePrimitive.primitiveTimeLp T hT) v)

Its displacement primitive is the actual physical test F b.

theorem EulerMeanVariationalInverse.meanTestMap_trace (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) (v : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)) : (meanTrace T hT FInv) ((meanTestMap T hT FInv F F' hF hInv) v) = (F ⟨0, ⋯⟩) ↑((EulerTerminalTimePrimitive.initialTrace T hT) v)

The initial trace of the physical test is exactly F(0) b(0).

theorem EulerMeanVariationalInverse.meanTestMap_trace_zero (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) (v : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)) (hv : (EulerTerminalTimePrimitive.initialTrace T hT) v = 0) : (meanTrace T hT FInv) ((meanTestMap T hT FInv F F' hF hInv) v) = 0

Therefore zero-endpoint label tests remove both actual initial boundary terms.