 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
 131  calc
 132    zeroDefect (functionalReflection ρ)
 133        =
 134          Foundation.DiscretenessForcing.J_log
 135            (zeroDeviation (functionalReflection ρ)) := zeroDefect_eq_J_log _
 136    _ = Foundation.DiscretenessForcing.J_log (-zeroDeviation ρ) := by
 137          rw [zeroDeviation_functionalReflection]
 138    _ = Foundation.DiscretenessForcing.J_log (zeroDeviation ρ) := by
 139          exact Foundation.DiscretenessForcing.J_log_symmetric (zeroDeviation ρ)
 140    _ = zeroDefect ρ := (zeroDefect_eq_J_log ρ).symm
 141
 142/-- Conjugation preserves the zero-location defect. -/
 143theorem zeroDefect_invariant_under_conjugation (ρ : ℂ) :
 144    zeroDefect (conj ρ) = zeroDefect ρ := by
 145  calc
 146    zeroDefect (conj ρ)
 147        =
 148          Foundation.DiscretenessForcing.J_log

papers checked against this theorem

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