zeroDefect_zero_iff_on_critical_line

formal source

  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 (ρ : ℂ) :
  84    0 < zeroDefect ρ ↔ ¬ OnCriticalLine ρ := by
  85  rw [zeroDefect_eq_J_log]
  86  constructor
  87  · intro h hline
  88    have hzero :
  89        Foundation.DiscretenessForcing.J_log (zeroDeviation ρ) = 0 :=
  90      (Foundation.DiscretenessForcing.J_log_eq_zero_iff).mpr
  91        ((zeroDeviation_eq_zero_iff_on_critical_line ρ).mpr hline)
  92    linarith
  93  · intro hline
  94    have hneq : zeroDeviation ρ ≠ 0 := by
  95      intro hz
  96      exact hline ((zeroDeviation_eq_zero_iff_on_critical_line ρ).mp hz)
  97    exact Foundation.DiscretenessForcing.J_log_pos hneq
  98