  50    (Foundation.DiscretenessForcing.J_log_eq_J_exp (zeroDeviation ρ)).symm
  51
  52/-- Expanded closed form for the zero-location defect. -/
  53theorem zeroDefect_eq_cosh_sub_one (ρ : ℂ) :
  54    zeroDefect ρ = Real.cosh (zeroDeviation ρ) - 1 := by
  55  simpa [Foundation.DiscretenessForcing.J_log] using zeroDefect_eq_J_log ρ
  56
  57/-- A point lies on the critical line exactly when its zero deviation is zero. -/
  58theorem zeroDeviation_eq_zero_iff_on_critical_line (ρ : ℂ) :
  59    zeroDeviation ρ = 0 ↔ OnCriticalLine ρ := by
  60  unfold zeroDeviation OnCriticalLine
  61  constructor
  62  · intro h
  63    linarith
  64  · intro h
  65    linarith
  66
  67/-- The zero-location defect vanishes exactly on the critical line. -/
  68theorem zeroDefect_zero_iff_on_critical_line (ρ : ℂ) :
  69    zeroDefect ρ = 0 ↔ OnCriticalLine ρ := by
  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. -/
  83theorem zeroDefect_pos_iff_off_critical_line (ρ : ℂ) :

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.