structure definition def or abbrev

`WeakZFRCert`

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

formal statement (Lean)

 106structure WeakZFRCert where
 107  classical_exists : Nonempty ZeroFreeRegion
 108  defect_gives_zfr : ∀ (db : DefectBudget), ∃ c, 0 < c ∧ ∀ t, 1 < t → c / Real.log t > 0
 109

used by (1)

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

weak_zfr_cert_exists in IndisputableMonolith.NumberTheory.WeakZeroFreeRegion decl_use

depends on (2)

Lean names referenced from this declaration's body.

DefectBudget in IndisputableMonolith.NumberTheory.WeakZeroFreeRegion decl_use
ZeroFreeRegion in IndisputableMonolith.NumberTheory.WeakZeroFreeRegion decl_use