One-time coefficient absorption for a genuine fixed-Sobolev inverse

Only the given operator coefficients use tensor bounds. Forcing and solved fields retain their literal fixed-base ordered-word blocks at the same radius.

def EulerParameterWordGevrey.inverseBlockCost (ι : Type u_1) [Fintype ι] (q : ℕ) (I Rc C D : ℝ) : ℝ

For fixed q this is an explicit polynomial in the original inverse, coefficient, and forcing constants. It has no grade dependence.

Equations

• One or more equations did not get rendered due to their size.

theorem EulerParameterWordGevrey.inverse_block_gevrey_of_tensor {P : Type u_1} {E : Type u_2} {ι : Type u_3} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] [Fintype ι] (directions : ι → P) (hd : ∀ (i : ι), ‖directions i‖ ≤ 1) (q : ℕ) (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) (inverse : P → E →L[ℝ] E) (hleft : ∀ (x : P) (v : E), (inverse x) ((A x) v) = v) (I Rc C D R : ℝ) (hRc : 0 ≤ Rc) (hC : 0 ≤ C) (hD : 0 ≤ D) (hinv : ∀ (x : P), ‖inverse x‖ ≤ I) (hcoeff : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n A x‖ ≤ C * EulerGevrey.majorant Rc 0 n) (hR : 2 * inverseBlockCost ι q I Rc C D * (sobolevCoefficientRadius ι Rc + 1) ≤ R) (d : ℕ) (hforce : ∀ (n : ℕ) (x : P), block directions q f n x ≤ D * EulerGevrey.majorant R d n) (n : ℕ) (x : P) : block directions q u n x ≤ EulerGevrey.majorant R (d + 1) n

The source radius is chosen once from coefficient data; each inverse application increases the grade by one without changing that radius.