Source indexedtheorem · leanprover/lean4:v4.32.0

FKS2.Floor.corollary_22_of_midrange

PrimeNumberTheoremAnd.IEANTN.FKS2Floor.Cor22Floor · PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean:202 to 213

Source documentation

Full Corollary 22, reduced to the remaining mid-range table-data theorem. The small range is corollary_22_floor; the asymptotic tail is FKS2.corollary_22_tail.

Exact Lean statement

theorem corollary_22_of_midrange
    (hmid : ∀ x ∈ Set.Icc (exp 10) (exp 20000),
      Eπ x ≤ admissible_bound 9.2211 (3 / 2) 0.8476 1 x) :
    Eπ.classicalBound 9.2211 (3 / 2) 0.8476 1 2

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem corollary_22_of_midrange    (hmid : ∀ x ∈ Set.Icc (exp 10) (exp 20000),      Eπ x ≤ admissible_bound 9.2211 (3 / 2) 0.8476 1 x) :    Eπ.classicalBound 9.2211 (3 / 2) 0.8476 1 2 := by  intro x hx  by_cases hsmall : x ≤ exp 10  · exact corollary_22_floor x ⟨hx, hsmall⟩  · by_cases htail : exp 20000 ≤ x    · exact _root_.FKS2.corollary_22_tail x htail    · have hx_lo : exp 10 ≤ x := le_of_lt (lt_of_not_ge hsmall)      have hx_hi : x ≤ exp 20000 := le_of_not_ge htail      exact hmid x ⟨hx_lo, hx_hi⟩