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

zeroDefect_zero_iff_on_critical_line

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)

  68theorem zeroDefect_zero_iff_on_critical_line (ρ : ℂ) :
  69    zeroDefect ρ = 0 ↔ OnCriticalLine ρ := by

proof body

Term-mode proof.

  70  rw [zeroDefect_eq_J_log]
  71  constructor
  72  · intro h
  73    have hz :
  74        zeroDeviation ρ = 0 :=
  75      (Foundation.DiscretenessForcing.J_log_eq_zero_iff).mp h
  76    exact (zeroDeviation_eq_zero_iff_on_critical_line ρ).mp hz
  77  · intro h
  78    have hz : zeroDeviation ρ = 0 :=
  79      (zeroDeviation_eq_zero_iff_on_critical_line ρ).mpr h
  80    exact (Foundation.DiscretenessForcing.J_log_eq_zero_iff).mpr hz
  81
  82/-- Off the critical line, the zero-location defect is strictly positive. -/

used by (2)

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

depends on (11)

Lean names referenced from this declaration's body.