Analytic estimates

Uniform bounds on the Niven auxiliary polynomials, controlling the size of the integral appearing in Niven's proof of the transcendence of π.

theorem Fp_bounded (T : Polynomial ℤ) (a : ℂ) : ∃ (M : ℝ), 0 ≤ M ∧ ∀ (p : ℕ), ∀ t ∈ Set.uIoc 0 1, ‖(Polynomial.aeval (↑t * a)) (Fp T p)‖ ≤ ‖a‖ ^ (p - 1) * M ^ p

There is a uniform bound ‖Fₚ(t a)‖ ≤ ‖a‖ᵖ⁻¹ Mᵖ for 0 < t ≤ 1.

theorem Fp_cexp_bounded (T : Polynomial ℤ) (a : ℂ) : ∃ (M : ℝ), 0 ≤ M ∧ ∀ (p : ℕ), 0 < p → ∀ t ∈ Set.uIoc 0 1, ‖a * Complex.exp (-(↑t * a)) * (Polynomial.aeval (↑t * a)) (Fp T p)‖ ≤ ‖a‖ ^ p * Real.exp ‖a‖ * M ^ p

There is a uniform bound ‖a * exp(-(t a)) * Fₚ(t a)‖ ≤ ‖a‖ᵖ * exp(‖a‖) * Mᵖ for 0 < t ≤ 1.

theorem intExpNegPoly_bounded (T : Polynomial ℤ) (a : ℂ) : ∃ (M : ℝ), 0 ≤ M ∧ ∀ (p : ℕ), 0 < p → ‖intExpNegPoly (Fp T p) a‖ ≤ ‖a‖ ^ p * Real.exp ‖a‖ * M ^ p

The integral ``∫₀¹ a * exp(-(t a)) * T(t a) dtis≤ ‖a‖ᵖ * exp(‖a‖) * Mᵖ`.

theorem sum_intExpNegPoly_bound (n : ℕ) (T : Polynomial ℤ) (hn : 0 < n) (a b : Fin n → ℂ) : ∃ (A : ℝ) (B : ℝ), 0 ≤ A ∧ 0 ≤ B ∧ ∀ (p : ℕ), 0 < p → ‖∑ i : Fin n, b i * Complex.exp (a i) * intExpNegPoly (Fp T p) (a i)‖ ≤ A * B ^ p

The weighted sum ∑ᵢ bᵢ exp(aᵢ) ∫₀¹ aᵢ * exp(-(t aᵢ)) * T(t aᵢ) dt is ≤ A Bᵖ.

theorem sum_intExpNegPoly_asym_ubound (n : ℕ) (T : Polynomial ℤ) (hn : 0 < n) (a b : Fin n → ℂ) (c : ℂ) : ∀ᶠ (p : ℕ) in Filter.atTop, ‖c ^ p * ∑ i : Fin n, b i * Complex.exp (a i) * intExpNegPoly (Fp T p) (a i)‖ < ↑(p - 1).factorial

For p large, cᵖ ‖∑ᵢ bᵢ exp(aᵢ) ∫₀¹ aᵢ * exp(-(t aᵢ)) * T(t aᵢ) dt‖ is ≤ (p - 1)!.

theorem sum_cexp_simp (n p : ℕ) (T : Polynomial ℤ) (a b : Fin n → ℂ) (hn : 0 < n) (hp : 0 < p) (ha : ∀ (i : Fin n), a i ≠ 0) (hroot : ∀ (i : Fin n), a i ∈ T.aroots ℂ) : (Polynomial.aeval 0) (Fpd T p) * ∑ i : Fin n, b i * Complex.exp (a i) - ∑ i : Fin n, b i * (Polynomial.aeval (a i)) (Fpd T p) = (↑(p - 1).factorial * (Polynomial.aeval 0) T ^ p + ↑p.factorial * (Polynomial.aeval 0) (Gp T p)) * ∑ i : Fin n, b i * Complex.exp (a i) - ↑p.factorial * ∑ i : Fin n, b i * (Polynomial.aeval (a i)) (Gp T p)

We have that F_{p,d}(0) ∑ᵢ₌₀ⁿ⁻¹ bᵢ eᵃⁱ − ∑ᵢ₌₀ⁿ⁻¹ bᵢ F_{p,d}(aᵢ) can be written as ((p−1)! T(0)ᵖ + p! Gₚ(0)) ∑ᵢ₌₀ⁿ⁻¹ bᵢ eᵃⁱ − p! ∑ᵢ₌₀ⁿ⁻¹ bᵢ Gₚ(aᵢ).

theorem intExpNegPoly_eq (n p : ℕ) (T : Polynomial ℤ) (a b : Fin n → ℂ) (hn : 0 < n) (hp : 0 < p) (ha : ∀ (i : Fin n), a i ≠ 0) (hroot : ∀ (i : Fin n), a i ∈ T.aroots ℂ) : ∑ i : Fin n, b i * Complex.exp (a i) * intExpNegPoly (Fp T p) (a i) = (↑(p - 1).factorial * (Polynomial.aeval 0) T ^ p + ↑p.factorial * (Polynomial.aeval 0) (Gp T p)) * ∑ i : Fin n, b i * Complex.exp (a i) - ↑p.factorial * ∑ i : Fin n, b i * (Polynomial.aeval (a i)) (Gp T p)

The sum ∑ᵢ bᵢ exp(aᵢ) ∫₀¹ aᵢ * exp(-(t aᵢ)) * T(t aᵢ) dt can be as ((p−1)! T(0)ᵖ + p! Gₚ(0)) ∑ᵢ₌₀ⁿ⁻¹ bᵢ eᵃⁱ − p! ∑ᵢ₌₀ⁿ⁻¹ bᵢ Gₚ(aᵢ).

theorem sum_cexp_eq (n p : ℕ) (T : Polynomial ℤ) (a b : Fin n → ℂ) (c k : ℤ) (f : ℕ → ℤ) (hp : 0 < p) (hfp : ↑c ^ p * ∑ i : Fin n, b i * (Polynomial.aeval (a i)) (Gp T p) = ↑(f p)) : ↑c ^ p * ((↑(p - 1).factorial * (Polynomial.aeval 0) T ^ p + ↑p.factorial * (Polynomial.aeval 0) (Gp T p)) * -↑k - ↑p.factorial * ∑ i : Fin n, b i * (Polynomial.aeval (a i)) (Gp T p)) = ↑(p - 1).factorial * -(↑k * (↑c ^ p * ↑(T.coeff 0) ^ p) + ↑p * (↑k * (↑c ^ p * ↑((Gp T p).coeff 0)) + ↑(f p)))

If cᵖ ∑ᵢ₌₀ⁿ⁻¹ bᵢ Gₚ(aᵢ) = f(p) ∈ ℤ, then cᵖ (((p−1)! T(0)ᵖ + p! Gₚ(0)) · (-k) − p! ∑ᵢ₌₀ⁿ⁻¹ bᵢ Gₚ(aᵢ)) is equal to − (p−1)! (k cᵖ T(0)ᵖ + p (k cᵖ Gₚ(0) + f(p))).

theorem sum_Gp_asym_lbound (n : ℕ) (T : Polynomial ℤ) (a b : Fin n → ℂ) (c k : ℤ) (f : ℕ → ℤ) (hc : c ≠ 0) (hk : k ≠ 0) (hT : (Polynomial.aeval 0) T ≠ 0) (hf : ∀ᶠ (p : { p : ℕ // Nat.Prime p }) in Filter.atTop, ↑c ^ ↑p * ∑ i : Fin n, b i * (Polynomial.aeval (a i)) (Gp T ↑p) = ↑(f ↑p)) : ∀ᶠ (p : { p : ℕ // Nat.Prime p }) in Filter.atTop, ‖↑c ^ ↑p * ((↑(↑p - 1).factorial * (Polynomial.aeval 0) T ^ ↑p + ↑(↑p).factorial * (Polynomial.aeval 0) (Gp T ↑p)) * -↑k - ↑(↑p).factorial * ∑ i : Fin n, b i * (Polynomial.aeval (a i)) (Gp T ↑p))‖ ≥ ↑(↑p - 1).factorial

If cᵖ ∑ᵢ₌₀ⁿ⁻¹ bᵢ Gₚ(aᵢ) = f(p) ∈ ℤ, then for sufficiently large primes p, ‖cᵖ (((p−1)! T(0)ᵖ + p! Gₚ(0)) · (-k) − p! ∑ᵢ₌₀ⁿ⁻¹ bᵢ Gₚ(aᵢ))‖ ≥ (p - 1)!.