A polynomial base controls every surviving finite packet grade after the final factorial split.

def EulerPacketCoarseMajorant.gradeBase (R : ℝ) (N : ℕ) : ℝ

Its N-degree is 220, leaving room in the source's exponent 300 for finite sums.

Equations

• EulerPacketCoarseMajorant.gradeBase R N = (4 * R * (550 * ↑N) ^ 2) ^ 110

theorem EulerPacketCoarseMajorant.gradeBase_nonneg (R : ℝ) (N : ℕ) : 0 ≤ gradeBase R N

theorem EulerPacketCoarseMajorant.gradeBase_ge_one (R : ℝ) (hR : 1 ≤ R) (N : ℕ) (hN : 1 ≤ N) : 1 ≤ gradeBase R N

theorem EulerPacketCoarseMajorant.factorial_le_grade_power (N p d : ℕ) (hN : 1 ≤ N) (hp : p ≤ 2 * N + 2) (hd : d ≤ 110 * (p + 1)) : ↑d.factorial ≤ (550 * ↑N) ^ d

theorem EulerPacketCoarseMajorant.majorant_grade_bound (R : ℝ) (hR : 1 ≤ R) (N p d n : ℕ) (hN : 1 ≤ N) (hp : p ≤ 2 * N + 2) (hd : d ≤ 110 * (p + 1)) : EulerGevrey.majorant R d n ≤ gradeBase R N ^ (p + 1) * EulerGevrey.majorant (4 * R) 0 n

The external derivative radius is enlarged once; all grade dependence is in one polynomial base.