pith. machine review for the scientific record. sign in
def definition def or abbrev

classical_zfr

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)

  48def classical_zfr (c : ℝ) (hc : 0 < c) : ZeroFreeRegion where
  49  width := fun t => c / Real.log t

proof body

Definition body.

  50  width_pos := by
  51    intro t ht
  52    exact div_pos hc (Real.log_pos ht)
  53  width_decreasing := by
  54    intro t₁ t₂ ht₁ ht₁₂
  55    apply div_le_div_of_nonneg_left (le_of_lt hc) (Real.log_pos ht₁)
  56    exact Real.log_le_log (by linarith) (le_of_lt ht₁₂)
  57
  58/-! ## Defect Budget Bound
  59
  60The RS defect-budget bridge constrains the total defect in the ledger.
  61This translates to a constraint on zeta zeros via the explicit formula. -/
  62

used by (2)

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

depends on (10)

Lean names referenced from this declaration's body.