Absorbing a fixed factorial shift into a coefficient radius

The factor (n+1)² costs only 4^n. Thus the one-shift estimate for an actual bounded inverse becomes a shift-zero coefficient estimate at a larger fixed radius. The enlargement is independent of the derivative order.

theorem EulerGevrey.succ_le_two_pow_real (n : ℕ) : ↑n + 1 ≤ 2 ^ n

The elementary exponential bound needed for one fixed derivative shift.

theorem EulerGevrey.majorant_one_le_radius_four (R : ℝ) (hR : 0 ≤ R) (n : ℕ) : majorant R 1 n ≤ R * majorant (4 * R) 0 n

One fixed factorial shift is a fixed radius enlargement for coefficients.