zeroDefect_nonneg

formal source

  97    exact Foundation.DiscretenessForcing.J_log_pos hneq
  98
  99/-- The zero-location defect is nonnegative everywhere. -/
 100theorem zeroDefect_nonneg (ρ : ℂ) : 0 ≤ zeroDefect ρ := by
 101  rw [zeroDefect_eq_J_log]
 102  exact Foundation.DiscretenessForcing.J_log_nonneg (zeroDeviation ρ)
 103
 104@[simp] theorem functionalReflection_re (ρ : ℂ) :
 105    (functionalReflection ρ).re = 1 - ρ.re := by
 106  simp [functionalReflection]
 107
 108@[simp] theorem criticalReflection_re (ρ : ℂ) :
 109    (criticalReflection ρ).re = 1 - ρ.re := by
 110  simp [criticalReflection]
 111
 112@[simp] theorem zeroDeviation_functionalReflection (ρ : ℂ) :
 113    zeroDeviation (functionalReflection ρ) = -zeroDeviation ρ := by
 114  unfold zeroDeviation functionalReflection
 115  simp
 116  linarith
 117
 118@[simp] theorem zeroDeviation_conj (ρ : ℂ) :
 119    zeroDeviation (conj ρ) = zeroDeviation ρ := by
 120  simp [zeroDeviation]
 121
 122@[simp] theorem zeroDeviation_criticalReflection (ρ : ℂ) :
 123    zeroDeviation (criticalReflection ρ) = -zeroDeviation ρ := by
 124  unfold zeroDeviation criticalReflection
 125  simp
 126  linarith
 127
 128/-- Reflection across `Re(s) = 1/2` preserves the zero-location defect. -/
 129theorem zeroDefect_invariant_under_functional_reflection (ρ : ℂ) :
 130    zeroDefect (functionalReflection ρ) = zeroDefect ρ := by