Source indexedtheorem · leanprover/lean4:v4.32.0

FKS2.Table4Ext.Epi_le_admissible_on_midrange

PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4Ext · PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4Ext.lean:127 to 138

Source documentation

The Corollary 22 mid-range: on [exp 10, exp 20000] the prime counting error Eπ is bounded by the Corollary 22 admissible curve. The trusted input is allCells_trusted (paper table data); everything else is machine-checked: the cell inequalities by dyadic interval arithmetic (allCells_checked), the grid contiguity by evaluation (allCells_chain, allCells_last), and the transport to the curve by cell_Epi_le_admissible.

Exact Lean statement

theorem Epi_le_admissible_on_midrange {x : ℝ}
    (hx : x ∈ Set.Icc (exp (10 : ℝ)) (exp (20000 : ℝ))) :
    Eπ x ≤ admissible_bound (Aq : ℝ) (3 / 2) (Cq : ℝ) 1 x

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem Epi_le_admissible_on_midrange {x : ℝ}    (hx : x ∈ Set.Icc (exp (10 : ℝ)) (exp (20000 : ℝ))) :    Eπ x ≤ admissible_bound (Aq : ℝ) (3 / 2) (Cq : ℝ) 1 x := by  have hx_lo : exp ((10 : ℕ) : ℝ) ≤ x := by    simpa using hx.1  have hx_hi : x ≤ exp ((lastB 10 allCells : ℕ) : ℝ) := by    rw [allCells_last]    simpa using hx.2  obtain ⟨c, hcmem, hcx⟩ :=    cover_of_chainOk allCells 10 allCells_ne_nil allCells_chain hx_lo hx_hi  exact cell_Epi_le_admissible c (allCells_checked c hcmem)    (allCells_trusted c hcmem) x hcx