pith. machine review for the scientific record. sign in
theorem proved term proof

prime_counting_asymptotic

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 128theorem prime_counting_asymptotic :
 129    ((fun x ↦ (Nat.primeCounting ⌊x⌋₊ : ℝ)) ~[atTop] (fun x ↦ x / Real.log x)) →
 130    ((fun x ↦ (Nat.primeCounting ⌊x⌋₊ : ℝ)) ~[atTop] (fun x ↦ x / Real.log x)) := by

proof body

Term-mode proof.

 131  intro hPNT
 132  exact prime_counting_asymptotic_pnt hPNT
 133
 134end IndisputableMonolith.NumberTheory.Port.PNT

depends on (2)

Lean names referenced from this declaration's body.