Uniform-time factorial bounds for the actual Gram inverse

The inverse is a genuinely smooth continuous operator path. Applying the frozen-coefficient recurrence in the uniform norm gives actual inverse-path and solution estimates, without a Hilbert structure on the path space.

@[instance_reducible]

noncomputable def EulerContinuousGramGevrey.instContinuousGramGevrey1 {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] : NormedAddCommGroup (U →L[ℝ] U)

Cache the standard NormedAddCommGroup (U →L[ℝ] U) instance to shorten typeclass synthesis.

Equations

• EulerContinuousGramGevrey.instContinuousGramGevrey1 = inferInstance

@[instance_reducible]

noncomputable def EulerContinuousGramGevrey.instContinuousGramGevrey2 {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] : NormedSpace ℝ (U →L[ℝ] U)

Cache the standard NormedSpace ℝ (U →L[ℝ] U) instance to shorten typeclass synthesis.

Equations

• EulerContinuousGramGevrey.instContinuousGramGevrey2 = inferInstance

@[instance_reducible]

noncomputable def EulerContinuousGramGevrey.instContinuousGramGevrey3 {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (T : ℝ) : NormedAddCommGroup C(↑(Set.Icc 0 T), U →L[ℝ] U)

Cache the standard NormedAddCommGroup C(Icc (0 : ℝ) T,U →L[ℝ] U) instance to shorten typeclass synthesis.

Equations

• EulerContinuousGramGevrey.instContinuousGramGevrey3 T = inferInstance

@[instance_reducible]

noncomputable def EulerContinuousGramGevrey.instContinuousGramGevrey4 {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (T : ℝ) : NormedSpace ℝ C(↑(Set.Icc 0 T), U →L[ℝ] U)

Cache the standard NormedSpace ℝ C(Icc (0 : ℝ) T,U →L[ℝ] U) instance to shorten typeclass synthesis.

Equations

• EulerContinuousGramGevrey.instContinuousGramGevrey4 T = inferInstance

@[instance_reducible]

noncomputable def EulerContinuousGramGevrey.instContinuousGramGevrey5 {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (T : ℝ) : NormedAddCommGroup (C(↑(Set.Icc 0 T), U →L[ℝ] U) →L[ℝ] C(↑(Set.Icc 0 T), U →L[ℝ] U))

Cache the standard NormedAddCommGroup (C(Icc (0 : ℝ) T,U →L[ℝ] U) →L[ℝ] C(Icc (0 : ℝ) T,U →L[ℝ] U)) instance to shorten typeclass synthesis.

Equations

• EulerContinuousGramGevrey.instContinuousGramGevrey5 T = inferInstance

@[instance_reducible]

noncomputable def EulerContinuousGramGevrey.instContinuousGramGevrey6 {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (T : ℝ) : NormedSpace ℝ (C(↑(Set.Icc 0 T), U →L[ℝ] U) →L[ℝ] C(↑(Set.Icc 0 T), U →L[ℝ] U))

Cache the standard NormedSpace ℝ (C(Icc (0 : ℝ) T,U →L[ℝ] U) →L[ℝ] C(Icc (0 : ℝ) T,U →L[ℝ] U)) instance to shorten typeclass synthesis.

Equations

• EulerContinuousGramGevrey.instContinuousGramGevrey6 T = inferInstance

noncomputable def EulerContinuousGramGevrey.leftMultiplicationMap {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (T : ℝ) : C(↑(Set.Icc 0 T), U →L[ℝ] U) →L[ℝ] C(↑(Set.Icc 0 T), U →L[ℝ] U) →L[ℝ] C(↑(Set.Icc 0 T), U →L[ℝ] U)

Bounded left multiplication on continuous endomorphism paths, as a bounded linear function of the actual coefficient path.

Equations

• EulerContinuousGramGevrey.leftMultiplicationMap T = EulerContinuousPathCalculus.coefficientMap ∘SL EulerContinuousPathComposition.compositionLift

theorem EulerContinuousGramGevrey.leftMultiplicationMap_norm {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (T : ℝ) : ‖leftMultiplicationMap T‖ ≤ 1

theorem EulerContinuousGramGevrey.inversePath_gevrey {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {P : Type u_3} [NormedAddCommGroup P] [NormedSpace ℝ P] (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) (R : ℝ) (hR : 2 * EulerTimeLpGramGevrey.gramCost c C 1 * (Rc + 1) ≤ R) (n : ℕ) (x : P) : ‖iteratedFDeriv ℝ n (fun (y : P) => EulerTransverseGramPath.gramInversePath T (Q y) c hc ⋯) x‖ ≤ EulerGevrey.majorant R 1 n

The actual continuous inverse path has one factorial shift, uniformly in time.

theorem EulerContinuousGramGevrey.solution_gevrey {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {P : Type u_3} [NormedAddCommGroup P] [NormedSpace ℝ P] (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 → C(↑(Set.Icc 0 T), U)) (hf : ContDiff ℝ (↑⊤) f) (D R : ℝ) (hD : 0 ≤ D) (hR : 2 * EulerTimeLpGramGevrey.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) => (EulerContinuousGramPath.solve T (Q y) c hc ⋯) (f y)) x‖ ≤ EulerGevrey.majorant R (d + 1) n

The actual continuous solution has the same one-shift inverse estimate.