zeroDeviation_functionalReflection

formal source

 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
 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. -/