`zeroDefect_invariant_under_functional_reflection`

proved

show as: view math explainer →

module: IndisputableMonolith.NumberTheory.ZeroLocationCost
domain: NumberTheory
line: 129 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.NumberTheory.ZeroLocationCost on GitHub at line 129.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

 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
 149            (zeroDeviation (conj ρ)) := zeroDefect_eq_J_log _
 150    _ = Foundation.DiscretenessForcing.J_log (zeroDeviation ρ) := by
 151          rw [zeroDeviation_conj]
 152    _ = zeroDefect ρ := (zeroDefect_eq_J_log ρ).symm
 153
 154/-- Reflection plus conjugation preserves the zero-location defect. -/
 155theorem zeroDefect_invariant_under_reflection (ρ : ℂ) :
 156    zeroDefect (criticalReflection ρ) = zeroDefect ρ := by
 157  calc
 158    zeroDefect (criticalReflection ρ)
 159        =

papers checked against this theorem

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