zeroDeviation

formal source

  35
  36/-- The real deviation of `ρ` from the critical line, expressed in the
  37log-coordinate scale compatible with the RS defect functional. -/
  38def zeroDeviation (ρ : ℂ) : ℝ :=
  39  2 * (ρ.re - 1 / 2)
  40
  41/-- The RS defect attached to the zero-location deviation of `ρ`. -/
  42def zeroDefect (ρ : ℂ) : ℝ :=
  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 (ρ : ℂ) :