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

boundaryZeroFreeCert

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)

  46def boundaryZeroFreeCert : BoundaryZeroFreeCert where
  47  ge_one := fun _ hs => riemannZeta_ne_zero_re_ge_one hs

proof body

Definition body.

  48  gt_one := fun _ hs => riemannZeta_ne_zero_re_gt_one hs
  49
  50/-! ## 2. The true strip target -/
  51
  52/-- A logarithmic zero-free strip with constants `c` and `T`.
  53
  54For `|Im(s)| ≥ T`, the region
  55`Re(s) > 1 - c / log(|Im(s)|)` is zero-free. This is the classical
  56Hadamard-de la Vallée-Poussin shape, stated as the exact bridge needed by
  57the RS program. -/

used by (2)

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

depends on (15)

Lean names referenced from this declaration's body.