Chebyshev estimates needed for the ζ(3) irrationality argument

This file ports the elementary, sorry-free Chebyshev estimate used by the upstream PrimeNumberTheoremAnd development. It gives an eventual bound ψ x ≤ 1.13 x, enough to control the lcm denominator in Beukers' proof.

noncomputable def LeanPool.Zeta3Irrational.ChebyshevAux.T (x : ℝ) : ℝ

The logarithm of ⌊x⌋₊!, written as a sum of log n for 1 ≤ n ≤ x.

Equations

• LeanPool.Zeta3Irrational.ChebyshevAux.T x = ∑ n ∈ Finset.Icc 1 ⌊x⌋₊, Real.log ↑n

theorem LeanPool.Zeta3Irrational.ChebyshevAux.T.le (x : ℝ) (hx : 1 ≤ x) : T x ≤ x * Real.log x - x + 1 + Real.log x

theorem LeanPool.Zeta3Irrational.ChebyshevAux.T.ge (x : ℝ) (hx : 1 ≤ x) : T x ≥ x * Real.log x - x + 1 - Real.log x

theorem LeanPool.Zeta3Irrational.ChebyshevAux.T.eq_sum_Lambda (x : ℝ) : T x = ∑ n ∈ Finset.Icc 1 ⌊x⌋₊, ArithmeticFunction.vonMangoldt n * ↑⌊x / ↑n⌋₊

noncomputable def LeanPool.Zeta3Irrational.ChebyshevAux.E (ν : ℕ →₀ ℝ) (x : ℝ) : ℝ

The floor-sum transform associated to a finitely supported weight ν.

Equations

• LeanPool.Zeta3Irrational.ChebyshevAux.E ν x = ν.sum fun (m : ℕ) (w : ℝ) => w * ↑⌊x / ↑m⌋₊

theorem LeanPool.Zeta3Irrational.ChebyshevAux.T.weighted_eq_sum (ν : ℕ →₀ ℝ) (x : ℝ) : (ν.sum fun (m : ℕ) (w : ℝ) => w * T (x / ↑m)) = ∑ n ∈ Finset.Icc 1 ⌊x⌋₊, ArithmeticFunction.vonMangoldt n * E ν (x / ↑n)

noncomputable def LeanPool.Zeta3Irrational.ChebyshevAux.ν : ℕ →₀ ℝ

Chebyshev's finite-difference weight used to compare ψ x with ψ (x / 6).

Equations

• LeanPool.Zeta3Irrational.ChebyshevAux.ν = Finsupp.single 1 1 - Finsupp.single 2 1 - Finsupp.single 3 1 - Finsupp.single 5 1 + Finsupp.single 30 1

theorem LeanPool.Zeta3Irrational.ChebyshevAux.nu_sum_div_eq_zero : (ν.sum fun (n : ℕ) (w : ℝ) => w / ↑n) = 0

theorem LeanPool.Zeta3Irrational.ChebyshevAux.E_nu_eq_one (x : ℝ) (hx : x ∈ Set.Ico 1 6) : E ν x = 1

theorem LeanPool.Zeta3Irrational.ChebyshevAux.E_nu_period (x : ℝ) (hx : x ≥ 0) : E ν (x + 30) = E ν x

theorem LeanPool.Zeta3Irrational.ChebyshevAux.E_nu_bound (x : ℝ) (hx : x ≥ 0) : 0 ≤ E ν x ∧ E ν x ≤ 1

noncomputable def LeanPool.Zeta3Irrational.ChebyshevAux.U (x : ℝ) : ℝ

The weighted logarithmic factorial sum used to bound increments of ψ.

Equations

• LeanPool.Zeta3Irrational.ChebyshevAux.U x = LeanPool.Zeta3Irrational.ChebyshevAux.ν.sum fun (m : ℕ) (w : ℝ) => w * LeanPool.Zeta3Irrational.ChebyshevAux.T (x / ↑m)

theorem LeanPool.Zeta3Irrational.ChebyshevAux.psi_ge_weighted (x : ℝ) (hx : x > 0) : Chebyshev.psi x ≥ U x

theorem LeanPool.Zeta3Irrational.ChebyshevAux.psi_diff_le_weighted (x : ℝ) (hx : x > 0) : Chebyshev.psi x - Chebyshev.psi (x / 6) ≤ U x

noncomputable def LeanPool.Zeta3Irrational.ChebyshevAux.a : ℝ

The main linear coefficient in the Chebyshev increment estimate.

Equations

• LeanPool.Zeta3Irrational.ChebyshevAux.a = -LeanPool.Zeta3Irrational.ChebyshevAux.ν.sum fun (m : ℕ) (w : ℝ) => w * Real.log ↑m / ↑m

theorem LeanPool.Zeta3Irrational.ChebyshevAux.a_simpl : a = 7 / 15 * Real.log 2 + 3 / 10 * Real.log 3 + 1 / 6 * Real.log 5

theorem LeanPool.Zeta3Irrational.ChebyshevAux.a_bound : a ∈ Set.Icc 0.92129 0.92130

noncomputable def LeanPool.Zeta3Irrational.ChebyshevAux.e (x : ℝ) : ℝ

The error term in Stirling's integral approximation for T x.

Equations

• LeanPool.Zeta3Irrational.ChebyshevAux.e x = LeanPool.Zeta3Irrational.ChebyshevAux.T x - (x * Real.log x - x + 1)

theorem LeanPool.Zeta3Irrational.ChebyshevAux.U_bound.lemma_1 (x : ℝ) : T x = x * Real.log x - x + 1 + e x

theorem LeanPool.Zeta3Irrational.ChebyshevAux.U_bound.lemma_2 (x : ℝ) (hx : 1 ≤ x) : |e x| ≤ Real.log x

theorem LeanPool.Zeta3Irrational.ChebyshevAux.U_bound.lemma_3 (x : ℝ) : U x = (((ν.sum fun (m : ℕ) (w : ℝ) => w * (x / ↑m * Real.log (x / ↑m))) - ν.sum fun (m : ℕ) (w : ℝ) => w * (x / ↑m)) + ν.sum fun (_m : ℕ) (w : ℝ) => w) + ν.sum fun (m : ℕ) (w : ℝ) => w * e (x / ↑m)

theorem LeanPool.Zeta3Irrational.ChebyshevAux.U_bound.lemma_4 (x : ℝ) (hx : 0 < x) : (ν.sum fun (m : ℕ) (w : ℝ) => w * (x / ↑m * Real.log (x / ↑m))) = a * x

theorem LeanPool.Zeta3Irrational.ChebyshevAux.U_bound.lemma_5 (x : ℝ) : (ν.sum fun (m : ℕ) (w : ℝ) => w * (x / ↑m)) = 0

theorem LeanPool.Zeta3Irrational.ChebyshevAux.U_bound.lemma_6 : (ν.sum fun (x : ℕ) (w : ℝ) => w) = -1

theorem LeanPool.Zeta3Irrational.ChebyshevAux.Finsupp.abs_sum_le (A : Type u_1) (ν : A →₀ ℝ) (g : A → ℝ → ℝ) : |ν.sum g| ≤ ν.sum |g|

theorem LeanPool.Zeta3Irrational.ChebyshevAux.U_bound (x : ℝ) (hx : 30 ≤ x) : |U x - a * x| ≤ 5 * Real.log x - 5

theorem LeanPool.Zeta3Irrational.ChebyshevAux.psi_diff_upper (x : ℝ) (hx : 30 ≤ x) : Chebyshev.psi x - Chebyshev.psi (x / 6) ≤ a * x + 5 * Real.log x - 5

theorem LeanPool.Zeta3Irrational.ChebyshevAux.psi_upper_coarse (x : ℝ) (hx : 30 ≤ x) : Chebyshev.psi x ≤ 6 * a * x / 5 + ↑⌊Real.log (x / 5) / Real.log 6⌋₊ * (5 * Real.log x - 5) + 180

theorem LeanPool.Zeta3Irrational.ChebyshevAux.eventually_psi_le_mul : ∀ᶠ (x : ℝ) in Filter.atTop, Chebyshev.psi x ≤ 113 / 100 * x