Source indexedtheorem · leanprover/lean4:v4.32.0

Buthe.table_1_to_32e12

PrimeNumberTheoremAnd.IEANTN.Buthe · PrimeNumberTheoremAnd/IEANTN/Buthe.lean:146 to 203

Mathematical statement

Exact Lean statement

@[blueprint
  "buthe-table-1-to-32e12"
  (title := "Buthe Table 1 up to 32e12")
  (statement := /-- Combining Büthe, arXiv:1511.02032v2, Section 6,
    Equation (6.2), with the rows of Table 1 up to
    $16 \cdot 10^{12}$ gives
    $-0.88 \leq (t-\psi(t))/\sqrt{t} \leq 0.86$ for
    $100 \leq t \leq 32 \cdot 10^{12}$. -/)
  (proof := /-- Use Lemma \ref{buthe-sieve-bound} up to
    $5 \cdot 10^{10}$, then chain the dyadic Table 1 intervals. -/)
  (latexEnv := "lemma")]
theorem table_1_to_32e12 :
    ∀ t ∈ Set.Icc (100 : ℝ) (32 * 10 ^ 12),
      -(0.88 : ℝ) ≤ (t - ψ t) / sqrt t ∧
        (t - ψ t) / sqrt t ≤ (0.86 : ℝ)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

@[blueprint  "buthe-table-1-to-32e12"  (title := "Buthe Table 1 up to 32e12")  (statement := /-- Combining Büthe, arXiv:1511.02032v2, Section 6,    Equation (6.2), with the rows of Table 1 up to    $16 \cdot 10^{12}$ gives    $-0.88 \leq (t-\psi(t))/\sqrt{t} \leq 0.86$ for    $100 \leq t \leq 32 \cdot 10^{12}$. -/)  (proof := /-- Use Lemma \ref{buthe-sieve-bound} up to    $5 \cdot 10^{10}$, then chain the dyadic Table 1 intervals. -/)  (latexEnv := "lemma")]theorem table_1_to_32e12 :    ∀ t ∈ Set.Icc (100 : ℝ) (32 * 10 ^ 12),      -(0.88 : ℝ) ≤ (t - ψ t) / sqrt t ∧        (t - ψ t) / sqrt t ≤ (0.86 : ℝ) := by  intro t ht  by_cases h5 : t ≤ 5 * 10 ^ 10  · have h := sieve_bound t ⟨ht.1, h5⟩    constructor <;> linarith  · by_cases h8 : t ≤ 8 * 10 ^ 10    · have h := eq_6_2 (4 * 10 ^ 10) (-0.73) 0.80        (by norm_num [table_1]) t ⟨by nlinarith, by nlinarith [h8]⟩      constructor <;> linarith    · by_cases h16 : t ≤ 16 * 10 ^ 10      · have h := eq_6_2 (8 * 10 ^ 10) (-0.80) 0.86          (by norm_num [table_1]) t ⟨by nlinarith, by nlinarith [h16]⟩        constructor <;> linarith      · by_cases h32 : t ≤ 32 * 10 ^ 10        · have h := eq_6_2 (16 * 10 ^ 10) (-0.88) 0.68            (by norm_num [table_1]) t ⟨by nlinarith, by nlinarith [h32]⟩          constructor <;> linarith        · by_cases h64 : t ≤ 64 * 10 ^ 10          · have h := eq_6_2 (32 * 10 ^ 10) (-0.88) 0.78              (by norm_num [table_1]) t ⟨by nlinarith, by nlinarith [h64]⟩            constructor <;> linarith          · by_cases h128 : t ≤ 128 * 10 ^ 10            · have h := eq_6_2 (64 * 10 ^ 10) (-0.66) 0.74                (by norm_num [table_1]) t ⟨by nlinarith, by nlinarith [h128]⟩              constructor <;> linarith            · by_cases h2e12 : t ≤ 2 * 10 ^ 12              · have h := eq_6_2 (10 ^ 12) (-0.80) 0.81                  (by norm_num [table_1]) t ⟨by nlinarith, by nlinarith [h2e12]⟩                constructor <;> linarith              · by_cases h4e12 : t ≤ 4 * 10 ^ 12                · have h := eq_6_2 (2 * 10 ^ 12) (-0.79) 0.76                    (by norm_num [table_1]) t ⟨by nlinarith, by nlinarith [h4e12]⟩                  constructor <;> linarith                · by_cases h8e12 : t ≤ 8 * 10 ^ 12                  · have h := eq_6_2 (4 * 10 ^ 12) (-0.73) 0.73                      (by norm_num [table_1]) t ⟨by nlinarith, by nlinarith [h8e12]⟩                    constructor <;> linarith                  · by_cases h16e12 : t ≤ 16 * 10 ^ 12                    · have h := eq_6_2 (8 * 10 ^ 12) (-0.80) 0.76                        (by norm_num [table_1]) t ⟨by nlinarith, by nlinarith [h16e12]⟩                      constructor <;> linarith                    · have h := eq_6_2 (16 * 10 ^ 12) (-0.80) 0.68                        (by norm_num [table_1]) t ⟨by nlinarith, by nlinarith [ht.2]⟩                      constructor <;> linarith