Actual all-order estimates for a coercive inverse

At a parameter value x, freeze the inverse of A x and write u y = (A x)⁻¹ (f y - (A y - A x) (u y)). The coefficient difference vanishes at x, so differentiating gives a triangular estimate with no highest-order solution term on the right. The factorial estimate below is therefore derived from genuine derivatives of the constructed inverse.

theorem EulerHilbertCoerciveGevrey.derivative_recurrence {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 : ∀ (y : P), (A y) (u y) = f y) (x : P) (I : E →L[ℝ] E) (hI : ∀ (v : E), I ((A x) v) = v) (n : ℕ) : ‖iteratedFDeriv ℝ n u x‖ ≤ ‖I‖ * (‖iteratedFDeriv ℝ n f x‖ + ∑ j ∈ Finset.range n, ↑(n.choose (j + 1)) * ‖iteratedFDeriv ℝ (j + 1) A x‖ * ‖iteratedFDeriv ℝ (n - (j + 1)) u x‖)

Freezing the coefficient gives the actual triangular derivative bound.

theorem EulerHilbertCoerciveGevrey.coerciveSolution_derivative_recurrence {P : Type u_1} {E : Type u_2} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (A : P → E →L[ℝ] E) (c : P → ℝ) (hc : ∀ (x : P), 0 < c x) (hcoercive : ∀ (x : P) (v : E), c x * ‖v‖ ^ 2 ≤ inner ℝ ((A x) v) v) (f : P → E) (hA : ContDiff ℝ (↑⊤) A) (hf : ContDiff ℝ (↑⊤) f) (x : P) (n : ℕ) : ‖iteratedFDeriv ℝ n (fun (y : P) => (EulerCoerciveProjection.coerciveInverse (A y) (c y) ⋯ ⋯) (f y)) x‖ ≤ (c x)⁻¹ * (‖iteratedFDeriv ℝ n f x‖ + ∑ j ∈ Finset.range n, ↑(n.choose (j + 1)) * ‖iteratedFDeriv ℝ (j + 1) A x‖ * ‖iteratedFDeriv ℝ (n - (j + 1)) (fun (y : P) => (EulerCoerciveProjection.coerciveInverse (A y) (c y) ⋯ ⋯) (f y)) x‖)

The recurrence for the actual Lax--Milgram inverse, with its coercivity bound.

theorem EulerHilbertCoerciveGevrey.coerciveSolution_gevrey {P : Type u_1} {E : Type u_2} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (A : P → E →L[ℝ] E) (c : P → ℝ) (hc : ∀ (x : P), 0 < c x) (hcoercive : ∀ (x : P) (v : E), c x * ‖v‖ ^ 2 ≤ inner ℝ ((A x) v) v) (f : P → E) (hA : ContDiff ℝ (↑⊤) A) (hf : ContDiff ℝ (↑⊤) f) (M Rc R : ℝ) (hM : 1 ≤ M) (hRc : 0 ≤ Rc) (hR : 2 * M * (Rc + 1) ≤ R) (hinv : ∀ (x : P), (c x)⁻¹ ≤ M) (hcoeff : ∀ (j : ℕ) (x : P), ‖iteratedFDeriv ℝ (j + 1) A x‖ ≤ Rc ^ (j + 1) * ↑(j + 1).factorial ^ 2) (d : ℕ) (hforce : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n f x‖ ≤ EulerGevrey.majorant R d n) (n : ℕ) (x : P) : ‖iteratedFDeriv ℝ n (fun (y : P) => (EulerCoerciveProjection.coerciveInverse (A y) (c y) ⋯ ⋯) (f y)) x‖ ≤ EulerGevrey.majorant R (d + 1) n

A single factorial shift controls every actual derivative of the inverse solve.

theorem EulerHilbertCoerciveGevrey.coerciveSolution_gevrey_amplitudes {P : Type u_1} {E : Type u_2} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (A : P → E →L[ℝ] E) (c : P → ℝ) (hc : ∀ (x : P), 0 < c x) (hcoercive : ∀ (x : P) (v : E), c x * ‖v‖ ^ 2 ≤ inner ℝ ((A x) v) v) (f : P → E) (hA : ContDiff ℝ (↑⊤) A) (hf : ContDiff ℝ (↑⊤) f) (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) (hinv : ∀ (x : P), (c 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 (fun (y : P) => (EulerCoerciveProjection.coerciveInverse (A y) (c y) ⋯ ⋯) (f y)) x‖ ≤ EulerGevrey.majorant R (d + 1) n

Polynomial coefficient and forcing amplitudes enter only the fixed top constant, not the derivative-order radius.