Genuine derivative estimates for bounded inverses on normed spaces

The triangular derivative estimate only needs an actual bounded left inverse of the frozen operator. This form applies to continuous path spaces as well as Hilbert spaces, without assigning a Hilbert structure to a uniform norm.

theorem EulerBoundedInverseGevrey.solution_gevrey {P : Type u_1} {E : Type u_2} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] (A : P → E →L[ℝ] E) (u f : P → E) (hA : ContDiff ℝ (↑⊤) A) (hu : ContDiff ℝ (↑⊤) u) (hf : ContDiff ℝ (↑⊤) f) (heq : ∀ (x : P), (A x) (u x) = f x) (inverse : P → E →L[ℝ] E) (hleft : ∀ (x : P) (v : E), (inverse x) ((A x) v) = v) (I C D M Rc R : ℝ) (hC : 0 ≤ C) (hD : 0 ≤ D) (hM : 1 ≤ M) (hMC : I * C ≤ M) (hMD : I * D ≤ M) (hRc : 0 ≤ Rc) (hR : 2 * M * (Rc + 1) ≤ R) (hinverse : ∀ (x : P), ‖inverse x‖ ≤ I) (hcoeff : ∀ (j : ℕ) (x : P), ‖iteratedFDeriv ℝ (j + 1) A x‖ ≤ C * (Rc ^ (j + 1) * ↑(j + 1).factorial ^ 2)) (d : ℕ) (hforce : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n f x‖ ≤ D * EulerGevrey.majorant R d n) (n : ℕ) (x : P) : ‖iteratedFDeriv ℝ n u x‖ ≤ EulerGevrey.majorant R (d + 1) n

Actual smooth solutions of an invertible operator family satisfy the same factorial estimate, using the genuine frozen inverse bound.