Source indexedtheorem · leanprover/lean4:v4.32.0

BKLNW.bklnw_table_from_buthe

PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW · PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:1634 to 1651

Mathematical statement

Exact Lean statement

@[blueprint
  "bklnw-table_from_buthe"
  (title := "BKLNW table from Buthe")
  (statement := /-- One has \eqref{equ:c-Psi-C} for each aggregate row
    extracted from Buthe's finite Eratosthenes-sieve computation, Table 1,
    and Theorem 2(a). -/)
  (proof := /-- This follows from Lemma \ref{buthe-sieve-bound},
    Lemma \ref{buthe-table-1-to-32e12}, and
    Lemma \ref{buthe-theorem-2a-normalized}. -/)
  (latexEnv := "lemma")
  (discussion := 1261)]
theorem bklnw_table_from_buthe (u v c C : ℝ) (h : (u, v, c, C) ∈ table_from_buthe) : ∀ x ∈ Set.Icc u v, -c ≤ (x - ψ x) / sqrt x ∧ (x - ψ x) / sqrt x ≤ C

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

@[blueprint  "bklnw-table_from_buthe"  (title := "BKLNW table from Buthe")  (statement := /-- One has \eqref{equ:c-Psi-C} for each aggregate row    extracted from Buthe's finite Eratosthenes-sieve computation, Table 1,    and Theorem 2(a). -/)  (proof := /-- This follows from Lemma \ref{buthe-sieve-bound},    Lemma \ref{buthe-table-1-to-32e12}, and    Lemma \ref{buthe-theorem-2a-normalized}. -/)  (latexEnv := "lemma")  (discussion := 1261)]theorem bklnw_table_from_buthe (u v c C : ℝ) (h : (u, v, c, C) ∈ table_from_buthe) : ∀ x ∈ Set.Icc u v, -c ≤ (x - ψ x) / sqrt x ∧ (x - ψ x) / sqrt x ≤ C := by  simp only [table_from_buthe, List.mem_cons, List.not_mem_nil, Prod.mk.injEq] at h  rcases h with ⟨rfl, rfl, rfl, rfl⟩ | ⟨rfl, rfl, rfl, rfl⟩ | ⟨rfl, rfl, rfl, rfl⟩ | hfalse  · exact Buthe.sieve_bound  · exact Buthe.table_1_to_32e12  · exact Buthe.theorem_2a_normalized  · contradiction