Uniform factorial estimates for the actual time Gram inverse

The lower frame bound and actual coefficient derivatives give the estimates for the inverse appearing in the strong acceleration equation. No derivative bounds on a pre-existing inverse are assumed.

noncomputable def EulerTimeLpGramGevrey.gramCost (c C D : ℝ) : ℝ

A polynomial top constant for coefficient amplitude 3 C² and forcing amplitude D.

Equations

• EulerTimeLpGramGevrey.gramCost c C D = 1 + c⁻¹ * (3 * C ^ 2 + D + 1)

theorem EulerTimeLpGramGevrey.gramSolution_contDiff {P : Type u_1} {U : Type u_2} {E : Type u_3} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (Q : P → C(↑(Set.Icc 0 T), U →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hLower : ∀ (x : P) (t : ↑(Set.Icc 0 T)) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q x) t) v‖ ^ 2) (f : P → ↥(EulerTimeLp.TimeLp T U)) {n : WithTop ℕ∞} (hQ : ContDiff ℝ n Q) (hf : ContDiff ℝ n f) : ContDiff ℝ n fun (x : P) => (EulerTimeLpGramInverse.gramSolver T hT (Q x) c hc ⋯) (f x)

The Gram solve is the actual smoothly parameterized coercive solution.

theorem EulerTimeLpGramGevrey.gramSolution_gevrey {P : Type u_1} {U : Type u_2} {E : Type u_3} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (Q : P → C(↑(Set.Icc 0 T), U →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hLower : ∀ (x : P) (t : ↑(Set.Icc 0 T)) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q x) t) v‖ ^ 2) (hQ : ContDiff ℝ (↑⊤) Q) (Rc C : ℝ) (hRc : 0 ≤ Rc) (hC : 0 ≤ C) (hbQ : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n Q x‖ ≤ C * EulerGevrey.majorant Rc 0 n) (f : P → ↥(EulerTimeLp.TimeLp T U)) (hf : ContDiff ℝ (↑⊤) f) (D R : ℝ) (hD : 0 ≤ D) (hR : 2 * gramCost c C D * (Rc + 1) ≤ R) (d : ℕ) (hbf : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n f x‖ ≤ D * EulerGevrey.majorant R d n) (n : ℕ) (x : P) : ‖iteratedFDeriv ℝ n (fun (y : P) => (EulerTimeLpGramInverse.gramSolver T hT (Q y) c hc ⋯) (f y)) x‖ ≤ EulerGevrey.majorant R (d + 1) n

One factorial shift for the genuine Gram inverse, with an explicit polynomial radius condition.

theorem EulerTimeLpGramGevrey.inverseGramMultiplier_gevrey {P : Type u_1} {U : Type u_2} {E : Type u_3} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (Q : P → C(↑(Set.Icc 0 T), U →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hLower : ∀ (x : P) (t : ↑(Set.Icc 0 T)) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q x) t) v‖ ^ 2) (hQ : ContDiff ℝ (↑⊤) Q) (Rc C : ℝ) (hRc : 0 ≤ Rc) (hC : 0 ≤ C) (hbQ : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n Q x‖ ≤ C * EulerGevrey.majorant Rc 0 n) (f : P → ↥(EulerTimeLp.TimeLp T U)) (hf : ContDiff ℝ (↑⊤) f) (D R : ℝ) (hD : 0 ≤ D) (hR : 2 * gramCost c C D * (Rc + 1) ≤ R) (d : ℕ) (hbf : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n f x‖ ≤ D * EulerGevrey.majorant R d n) (n : ℕ) (x : P) : ‖iteratedFDeriv ℝ n (fun (y : P) => (EulerTimeLp.timeMultiplier T hT (EulerTransverseGramPath.gramInversePath T (Q y) c hc ⋯)) (f y)) x‖ ≤ EulerGevrey.majorant R (d + 1) n

The same estimate applies to the explicit inverse-Gram multiplier in the strong equation.