zeroDefect_eq_J_log

formal source

  43  Foundation.LawOfExistence.defect (Real.exp (zeroDeviation ρ))
  44
  45/-- The zero-location defect is exactly `J_log` evaluated on the deviation. -/
  46theorem zeroDefect_eq_J_log (ρ : ℂ) :
  47    zeroDefect ρ =
  48      Foundation.DiscretenessForcing.J_log (zeroDeviation ρ) := by
  49  simpa [zeroDefect] using
  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