Prove2Me

Prime saving: Φn≥e(λK−δ)n\Phi_n\ge e^{(\lambda_K-\delta)n} from KK intervals of deleted primes

Proved
PiIrrationality.ZZEven.phi_lower

by moona3k · Oct 5, 2026 · Mathlib 0df444a (Lean v4.33.1)

number-theorypiprime-number-theorem

For every K≥0K\ge0 and every δ>0\delta>0, for all sufficiently large nn,

Φn ≥ exp⁡((λK−δ)n),λK=∑k=0K−1(42k+1−63k+2),\Phi_n\ \ge\ \exp\Bigl(\bigl(\lambda_K-\delta\bigr)n\Bigr),\qquad \lambda_K=\sum_{k=0}^{K-1}\Bigl(\frac{4}{2k+1}-\frac{6}{3k+2}\Bigr),

where Φn\Phi_n is the product of Bai's deleted primes for the exponents (2,4,6)(2,4,6), as in the definition file PiIrrationality_ZZEvenForms.

For each kk, every prime pp in the interval (6n3k+2,4n2k+1]\bigl(\tfrac{6n}{3k+2},\tfrac{4n}{2k+1}\bigr] that exceeds max⁡(5,8n)\max(5,\sqrt{8n}) is a deleted prime. Indeed {2n/p}=ω∈[12,23)\{2n/p\}=\omega\in[\tfrac12,\tfrac23), and the defining inequality becomes 5ω−52<3ω−15\omega-\tfrac52<3\omega-1. The prime number theorem gives these intervals a total logarithmic weight (42k+1−63k+2)n+o(n)\bigl(\tfrac{4}{2k+1}-\tfrac{6}{3k+2}\bigr)n+o(n). The values are λ1=1\lambda_1=1, λ2=17/15\lambda_2=17/15, λ3=17/15+1/20=71/60\lambda_3=17/15+1/20=71/60, increasing to 2(π23−log⁡334)=1.29055…2\bigl(\tfrac{\pi}{2\sqrt3}-\log\tfrac{3\sqrt3}{4}\bigr)=1.29055\ldots, which is Zeilberger–Zudilin's (10) at index 2n2n.

Preamble
import Definitions.Def_PiIrrationality_ZZEvenForms
import Mathlib.Analysis.SpecialFunctions.Exp
import Mathlib.Order.Filter.AtTopBot.Basic
Formal statement
theorem PiIrrationality.ZZEven.phi_lower (K : ℕ) (δ : ℝ) (hδ : 0 < δ) :
    ∀ᶠ n : ℕ in Filter.atTop,
      Real.exp (((∑ k ∈ Finset.range K,
          ((4 : ℝ) / (2 * k + 1) - 6 / (3 * k + 2))) - δ) * (n : ℝ)) ≤
        (PiIrrationality.ZZEven.Phi n : ℝ) := by
  sorry
Source
D. Zeilberger and W. Zudilin, The irrationality measure of π is at most 7.103205334137…, Moscow J. Combin. Number Theory 9 (2020), no. 4, 407–419, arXiv:1912.06345, Lemma 3 and equation (10) (citing Hata, Lemma 2.2); Y. Bai, The irrationality measure of π is at most 7.101862832357, arXiv:2609.11276 (v2, 11 Sep 2026), Section 3 (removable-prime saving), with (a,b,c)=(2,4,6).

View graph