Explicit numerical estimates for the factorial majorants used in the proposed Euler construction. These lemmas prove combinatorial implications; they do not assert the analytic estimates needed to apply the implications to Euler.

theorem EulerGevrey.radius_bounds {coefficientRadius inverseCost radius : ℝ} (hCoefficient : 0 ≤ coefficientRadius) (hInverse : 1 ≤ inverseCost) (hRadius : 2 * inverseCost * (coefficientRadius + 1) ≤ radius) : 1 ≤ radius ∧ coefficientRadius ≤ radius

A radius chosen for the inverse estimate dominates one and the coefficient radius.

theorem EulerGevrey.le_choose_of_interior (n k : ℕ) (hk : 0 < k) (hkn : k < n) : n ≤ n.choose k

Every interior entry of the nth binomial row is at least n.

theorem EulerGevrey.sum_inv_choose_le_three (n : ℕ) : ∑ k ∈ Finset.range (n + 1), 1 / ↑(n.choose k) ≤ 3

The reciprocal binomial row has uniformly bounded sum, including order zero.

theorem EulerGevrey.choose_le_shifted (n k d₁ d₂ : ℕ) (hkn : k ≤ n) : n.choose k ≤ (n + d₁ + d₂).choose (k + d₁)

Adding nonnegative shifts to both lower factorial indices enlarges the binomial coefficient.

theorem EulerGevrey.choose_ratio_le_inv (n k d₁ d₂ : ℕ) (hkn : k ≤ n) : ↑(n.choose k) / ↑((n + d₁ + d₂).choose (k + d₁)) ^ 2 ≤ 1 / ↑(n.choose k)

The exact reciprocal-binomial comparison used in the shifted product estimate.

theorem EulerGevrey.shifted_factorial_kernel_le (n k d₁ d₂ : ℕ) (hkn : k ≤ n) : ↑(n.choose k) * ↑(k + d₁).factorial ^ 2 * ↑(n - k + d₂).factorial ^ 2 ≤ ↑(n + d₁ + d₂).factorial ^ 2 / ↑(n.choose k)

A term of the shifted factorial convolution gains the reciprocal binomial coefficient.

def EulerGevrey.majorant (R : ℝ) (d n : ℕ) : ℝ

The Gevrey-two factorial majorant with a nonnegative integer shift.

Equations

• EulerGevrey.majorant R d n = R ^ (n + d) * ↑(n + d).factorial ^ 2

theorem EulerGevrey.majorant_nonneg (R : ℝ) (hR : 0 ≤ R) (d n : ℕ) : 0 ≤ majorant R d n

theorem EulerGevrey.majorant_product_term (R : ℝ) (hR : 0 ≤ R) (n k d₁ d₂ : ℕ) (hkn : k ≤ n) : ↑(n.choose k) * majorant R d₁ k * majorant R d₂ (n - k) ≤ majorant R (d₁ + d₂) n * (1 / ↑(n.choose k))

A single Leibniz term obeys the uniform shifted estimate.

theorem EulerGevrey.majorant_convolution (R : ℝ) (hR : 0 ≤ R) (n d₁ d₂ : ℕ) : ∑ k ∈ Finset.range (n + 1), ↑(n.choose k) * majorant R d₁ k * majorant R d₂ (n - k) ≤ 3 * majorant R (d₁ + d₂) n

The product constant is exactly 3, independently of order and both shifts.

theorem EulerGevrey.majorant_product_term_le (R : ℝ) (hR : 0 ≤ R) (n k d₁ d₂ : ℕ) (hkn : k ≤ n) : ↑(n.choose k) * majorant R d₁ k * majorant R d₂ (n - k) ≤ majorant R (d₁ + d₂) n

Discarding the reciprocal binomial gain is valid for each admissible split.

theorem EulerGevrey.majorant_shift_le (R : ℝ) (hR : 0 ≤ R) (d n : ℕ) : R * majorant R d n ≤ majorant R (d + 1) n

One spare factorial shift supplies a factor of at least R.

theorem EulerGevrey.geometric_tail_le_two_mul (q : ℝ) (hq : 0 ≤ q) (hhalf : q ≤ 1 / 2) (n : ℕ) : ∑ k ∈ Finset.range n, q ^ (k + 1) ≤ 2 * q

The geometric tail is bounded uniformly in the truncation length.

theorem EulerGevrey.majorant_coefficient_term (R Rc q : ℝ) (hR : 0 ≤ R) (hRc : 0 ≤ Rc) (hq : 0 ≤ q) (hscale : Rc ≤ q * R) (n k d : ℕ) (hkn : k ≤ n) : ↑(n.choose k) * Rc ^ k * ↑k.factorial ^ 2 * majorant R d (n - k) ≤ q ^ k * majorant R d n

A coefficient of radius Rc ≤ q R has the geometric gain q^k.

theorem EulerGevrey.triangular_inverse_majorant (A Rc R : ℝ) (hA : 1 ≤ A) (hRc : 0 ≤ Rc) (hlarge : 2 * A * (Rc + 1) ≤ R) (d : ℕ) (F Z : ℕ → ℝ) (hF : ∀ (n : ℕ), F n ≤ majorant R d n) (hZ : ∀ (n : ℕ), Z n ≤ A * (F n + ∑ k ∈ Finset.range n, ↑(n.choose (k + 1)) * Rc ^ (k + 1) * ↑(k + 1).factorial ^ 2 * Z (n - (k + 1)))) (n : ℕ) : Z n ≤ majorant R (d + 1) n

The triangular inverse rule with an explicit sufficient radius, uniform in the derivative order and in the input shift. The recurrence sums the indices 1,…,n as k + 1 for k ∈ range n. No sign assumption on F or Z is needed.

theorem EulerGevrey.triangular_inverse_polynomial_radius (P : ℝ) (hP : 2 ≤ P) (c d : ℕ) (F Z : ℕ → ℝ) (hF : ∀ (n : ℕ), F n ≤ majorant (P ^ (2 * c + 2)) d n) (hZ : ∀ (n : ℕ), Z n ≤ P ^ c * (F n + ∑ k ∈ Finset.range n, ↑(n.choose (k + 1)) * (P ^ c) ^ (k + 1) * ↑(k + 1).factorial ^ 2 * Z (n - (k + 1)))) (n : ℕ) : Z n ≤ majorant (P ^ (2 * c + 2)) (d + 1) n

For coefficient and inverse size P^c, the single polynomial radius P^(2c+2) suffices.

theorem EulerGevrey.sequence_product_majorant (R A B : ℝ) (hR : 0 ≤ R) (hA : 0 ≤ A) (hB : 0 ≤ B) (d₁ d₂ : ℕ) (f g : ℕ → ℝ) (hf : ∀ (n : ℕ), |f n| ≤ A * majorant R d₁ n) (hg : ∀ (n : ℕ), |g n| ≤ B * majorant R d₂ n) (n : ℕ) : |∑ k ∈ Finset.range (n + 1), ↑(n.choose k) * f k * g (n - k)| ≤ 3 * A * B * majorant R (d₁ + d₂) n

The shifted product rule applies directly to arbitrary real sequences bounded in absolute value.