Genuine inverse Gram calculus in the uniform time norm

The previously constructed continuous Gram inverse is an actual inverse in the Banach algebra of continuous operator paths. Its external-parameter smoothness follows from inversion at units of that algebra. No smoothness of a pre-existing inverse is assumed.

noncomputable def EulerContinuousGramPath.gramPathUnit {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (Q : C(↑(Set.Icc 0 T), U →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (v : U), c * ‖v‖ ^ 2 ≤ ‖(Q t) v‖ ^ 2) : C(↑(Set.Icc 0 T), U →L[ℝ] U)ˣ

The actual Gram path and its actual continuous inverse form a unit.

Equations

• EulerContinuousGramPath.gramPathUnit T Q c hc hQ = { val := EulerTransverseGramPath.gramPath T Q, inv := EulerTransverseGramPath.gramInversePath T Q c hc hQ, val_inv := ⋯, inv_val := ⋯ }

theorem EulerContinuousGramPath.gramInversePath_eq_ringInverse {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (Q : C(↑(Set.Icc 0 T), U →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (v : U), c * ‖v‖ ^ 2 ≤ ‖(Q t) v‖ ^ 2) : EulerTransverseGramPath.gramInversePath T Q c hc hQ = Ring.inverse (EulerTransverseGramPath.gramPath T Q)

The constructed path is exactly Banach-algebra inversion of the Gram coefficient.

noncomputable def EulerContinuousGramPath.solve {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (Q : C(↑(Set.Icc 0 T), U →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (v : U), c * ‖v‖ ^ 2 ≤ ‖(Q t) v‖ ^ 2) : C(↑(Set.Icc 0 T), U) →L[ℝ] C(↑(Set.Icc 0 T), U)

The actual inverse acting on continuous forcing paths.

Equations

• EulerContinuousGramPath.solve T Q c hc hQ = EulerContinuousTimeIntegral.multiplier (EulerTransverseGramPath.gramInversePath T Q c hc hQ)

theorem EulerContinuousGramPath.solve_equation {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (Q : C(↑(Set.Icc 0 T), U →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (v : U), c * ‖v‖ ^ 2 ≤ ‖(Q t) v‖ ^ 2) (f : C(↑(Set.Icc 0 T), U)) : (EulerContinuousTimeIntegral.multiplier (EulerTransverseGramPath.gramPath T Q)) ((solve T Q c hc hQ) f) = f

The continuous solution satisfies the actual coefficient equation.

theorem EulerContinuousGramPath.solve_left_inverse {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (Q : C(↑(Set.Icc 0 T), U →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (v : U), c * ‖v‖ ^ 2 ≤ ‖(Q t) v‖ ^ 2) (f : C(↑(Set.Icc 0 T), U)) : (solve T Q c hc hQ) ((EulerContinuousTimeIntegral.multiplier (EulerTransverseGramPath.gramPath T Q)) f) = f

The constructed inverse is also a left inverse in the uniform path space.

theorem EulerContinuousGramPath.solve_norm {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (Q : C(↑(Set.Icc 0 T), U →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (v : U), c * ‖v‖ ^ 2 ≤ ‖(Q t) v‖ ^ 2) : ‖solve T Q c hc hQ‖ ≤ c⁻¹

The uniform-in-time inverse has the same genuine coercive bound.

theorem EulerContinuousGramPath.gramPath_contDiff {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) {P : Type u_3} [NormedAddCommGroup P] [NormedSpace ℝ P] (Qp : P → C(↑(Set.Icc 0 T), U →L[ℝ] E)) {n : WithTop ℕ∞} (hQp : ContDiff ℝ n Qp) : ContDiff ℝ n fun (x : P) => EulerTransverseGramPath.gramPath T (Qp x)

The actual Gram path is smoothly parameterized in the uniform time norm.

theorem EulerContinuousGramPath.gramInversePath_contDiff {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T c : ℝ) (hc : 0 < c) {P : Type u_3} [NormedAddCommGroup P] [NormedSpace ℝ P] (Qp : P → C(↑(Set.Icc 0 T), U →L[ℝ] E)) (hLower : ∀ (x : P) (t : ↑(Set.Icc 0 T)) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Qp x) t) v‖ ^ 2) {n : WithTop ℕ∞} (hQp : ContDiff ℝ n Qp) : ContDiff ℝ n fun (x : P) => EulerTransverseGramPath.gramInversePath T (Qp x) c hc ⋯

Actual inverse-path regularity follows from the constructed Banach-algebra unit.

theorem EulerContinuousGramPath.solve_contDiff {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T c : ℝ) (hc : 0 < c) {P : Type u_3} [NormedAddCommGroup P] [NormedSpace ℝ P] (Qp : P → C(↑(Set.Icc 0 T), U →L[ℝ] E)) (hLower : ∀ (x : P) (t : ↑(Set.Icc 0 T)) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Qp x) t) v‖ ^ 2) (f : P → C(↑(Set.Icc 0 T), U)) {n : WithTop ℕ∞} (hQp : ContDiff ℝ n Qp) (hf : ContDiff ℝ n f) : ContDiff ℝ n fun (x : P) => (solve T (Qp x) c hc ⋯) (f x)

The genuinely constructed uniform-time solution is smoothly parameterized.

theorem EulerContinuousGramPath.gramPath_bound {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) {P : Type u_3} [NormedAddCommGroup P] [NormedSpace ℝ P] (Qp : P → C(↑(Set.Icc 0 T), U →L[ℝ] E)) (hQp : ContDiff ℝ (↑⊤) Qp) (R C : ℝ) (hR : 0 ≤ R) (hC : 0 ≤ C) (hb : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n Qp x‖ ≤ C * EulerGevrey.majorant R 0 n) (n : ℕ) (x : P) : ‖iteratedFDeriv ℝ n (fun (y : P) => EulerTransverseGramPath.gramPath T (Qp y)) x‖ ≤ 3 * C ^ 2 * EulerGevrey.majorant R 0 n

The actual Gram coefficient has the uniform factorial product bound.