The actual scalar normal coefficient as a one-column Gram inverse

The column r↦r m has Gram matrix ‖m‖². Its genuinely constructed bounded-field left inverse is therefore exactly v↦⟪m,v⟫/‖m‖². This derives uniform time-space regularity and factorial multiplier bounds from the normal field and its positive lower bound, without assuming regularity of a reciprocal field.

noncomputable def EulerSourceNormalCoefficient.normalColumn {K : Type u_1} {E : Type u_2} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [InnerProductSpace ℝ E] (m : EulerMeanCoefficients.SmoothCoefficientPath K E) : EulerMeanCoefficients.SmoothCoefficientPath K (ℝ →L[ℝ] E)

The normal vector as a genuine scalar-to-vector coefficient path.

Equations

• EulerSourceNormalCoefficient.normalColumn m = EulerMeanCoefficients.SmoothCoefficientPath.map (ContinuousLinearMap.toSpanSingletonLIE ℝ E).toLinearIsometry.toContinuousLinearMap m

@[simp]

theorem EulerSourceNormalCoefficient.normalColumn_apply {K : Type u_1} {E : Type u_2} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [InnerProductSpace ℝ E] (m : EulerMeanCoefficients.SmoothCoefficientPath K E) (t : K) (x : EulerSmoothLimit.Space) (r : ℝ) : (((normalColumn m).field t) x) r = r • (m.field t) x

theorem EulerSourceNormalCoefficient.normalColumn_lower {K : Type u_1} {E : Type u_2} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [InnerProductSpace ℝ E] (m : EulerMeanCoefficients.SmoothCoefficientPath K E) (c : ℝ) (hm : ∀ (t : K) (x : EulerSmoothLimit.Space), c ≤ ‖(m.field t) x‖ ^ 2) (t : K) (x : EulerSmoothLimit.Space) (r : ℝ) : c * ‖r‖ ^ 2 ≤ ‖(((normalColumn m).field t) x) r‖ ^ 2

noncomputable def EulerSourceNormalCoefficient.normalFunctional {K : Type u_1} {E : Type u_2} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (m : EulerMeanCoefficients.SmoothCoefficientPath K E) (c : ℝ) (hc : 0 < c) (hm : ∀ (t : K) (x : EulerSmoothLimit.Space), c ≤ ‖(m.field t) x‖ ^ 2) : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (E →L[ℝ] ℝ))

The actual scalar coefficient used by the pressure in equation (11).

Equations

• EulerSourceNormalCoefficient.normalFunctional m c hc hm = EulerSourceForwardCoefficient.sourceForcing (EulerSourceNormalCoefficient.normalColumn m) c hc ⋯

theorem EulerSourceNormalCoefficient.normalFunctional_apply {K : Type u_1} {E : Type u_2} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (m : EulerMeanCoefficients.SmoothCoefficientPath K E) (c : ℝ) (hc : 0 < c) (hm : ∀ (t : K) (x : EulerSmoothLimit.Space), c ≤ ‖(m.field t) x‖ ^ 2) (t : K) (x : EulerSmoothLimit.Space) (v : E) : (((normalFunctional m c hc hm) t) x) v = inner ℝ ((m.field t) x) v / ‖(m.field t) x‖ ^ 2

The constructed Gram left inverse is precisely the literal normal quotient.

theorem EulerSourceNormalCoefficient.normalFunctional_translation_contDiff {K : Type u_1} {E : Type u_2} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (m : EulerMeanCoefficients.SmoothCoefficientPath K E) (c : ℝ) (hc : 0 < c) (hm : ∀ (t : K) (x : EulerSmoothLimit.Space), c ≤ ‖(m.field t) x‖ ^ 2) : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath (normalFunctional m c hc hm))

The pressure coefficient has genuine translated uniform-path regularity.

theorem EulerSourceNormalCoefficient.normalFunctional_translation_bound {K : Type u_1} {E : Type u_2} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (m : EulerMeanCoefficients.SmoothCoefficientPath K E) (c : ℝ) (hc : 0 < c) (hm : ∀ (t : K) (x : EulerSmoothLimit.Space), c ≤ ‖(m.field t) x‖ ^ 2) (Rc C Ri : ℝ) (hRc : 0 ≤ Rc) (hC : 0 ≤ C) (hRi : 2 * EulerTimeLpGramGevrey.gramCost c C 1 * (Rc + 1) ≤ Ri) (hbm : ∀ (n : ℕ) (t : K) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(m.field t)) x‖ ≤ C * EulerGevrey.majorant Rc 0 n) (n : ℕ) (a : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath (normalFunctional m c hc hm)) a‖ ≤ 3 * Ri * C * EulerGevrey.majorant (4 * Ri) 0 n