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

StrongPNT_conditional

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)

  89theorem StrongPNT_conditional (hRH : True) -- RH placeholder
  90    (hStrong : ∃ C > 0, (ψ - id) =O[atTop] fun x ↦ Real.sqrt x * (Real.log x) ^ 2) :
  91    ∃ C > 0, (ψ - id) =O[atTop] fun x ↦ Real.sqrt x * (Real.log x) ^ 2
  92  := hStrong

proof body

Term-mode proof.

  93
  94/-! ## Consequences for Prime Counting -/
  95
  96/-- **TECHNICAL SCAFFOLD**: Prime between consecutive integers for large N. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (5)

Lean names referenced from this declaration's body.