A single polynomial base absorbs the finite residual multiplicity and the fixed profile envelope, before the geometric tail is summed.

def EulerPacketCoarseMajorant.tailBase (R H C : ℝ) (N : ℕ) : ℝ

Tail base, given by (1+C*(1+18*((N+2 : ℕ) : ℝ)^2))*H^2*gradeBase R N.

Equations

• EulerPacketCoarseMajorant.tailBase R H C N = (1 + C * (1 + 18 * ↑(N + 2) ^ 2)) * H ^ 2 * EulerPacketCoarseMajorant.gradeBase R N

theorem EulerPacketCoarseMajorant.tailBase_nonneg (R H C : ℝ) (hC : 0 ≤ C) (N : ℕ) : 0 ≤ tailBase R H C N

theorem EulerPacketCoarseMajorant.tailBase_ge_one (R H C : ℝ) (hR : 1 ≤ R) (hH : 1 ≤ H) (hC : 0 ≤ C) (N : ℕ) (hN : 1 ≤ N) : 1 ≤ tailBase R H C N

theorem EulerPacketCoarseMajorant.tailBase_absorption (R H C : ℝ) (hC : 0 ≤ C) (N n : ℕ) : (1 + 18 * ↑(N + 2) ^ 2) * C * H ^ (2 * n + 2) * gradeBase R N ^ (n + 1) ≤ tailBase R H C N ^ (n + 1)

The envelope is absorbed once into the base, with no dependence on the surviving grade in that base.

def EulerPacketCoarseMajorant.tailPolynomialConstant (R H C : ℝ) : ℝ

Tail polynomial constant, given by (1+163*C)*H^2*(4*R*550^2)^110.

Equations

• EulerPacketCoarseMajorant.tailPolynomialConstant R H C = (1 + 163 * C) * H ^ 2 * (4 * R * 550 ^ 2) ^ 110

theorem EulerPacketCoarseMajorant.tailPolynomialConstant_nonneg (R H C : ℝ) (hC : 0 ≤ C) : 0 ≤ tailPolynomialConstant R H C

theorem EulerPacketCoarseMajorant.gradeBase_polynomial (R : ℝ) (N : ℕ) : gradeBase R N = (4 * R * 550 ^ 2) ^ 110 * ↑N ^ 220

theorem EulerPacketCoarseMajorant.tailBase_polynomial_bound (R H C : ℝ) (hC : 0 ≤ C) (N : ℕ) (hN : 1 ≤ N) : tailBase R H C N ≤ tailPolynomialConstant R H C * ↑N ^ 222

Finite multiplicity raises the degree of the base from 220 to 222.