def
definition
zeroDeviationSet
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.NumberTheory.CompletedXiSymmetry on GitHub at line 38.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
35 { s : ℂ | Ξ.xi s = 0 }
36
37/-- The set of zero deviations realized by zeros of a completed-ξ surface. -/
38def zeroDeviationSet (Ξ : CompletedXiSurface) : Set ℝ :=
39 { t : ℝ | ∃ s : ℂ, Ξ.xi s = 0 ∧ zeroDeviation s = t }
40
41/-- The set of zero defects realized by zeros of a completed-ξ surface. -/
42def zeroDefectSet (Ξ : CompletedXiSurface) : Set ℝ :=
43 { d : ℝ | ∃ s : ℂ, Ξ.xi s = 0 ∧ zeroDefect s = d }
44
45/-- Functional-equation invariance of the completed-ξ value. -/
46theorem xi_reflection_invariant (Ξ : CompletedXiSurface) (s : ℂ) :
47 Ξ.xi (functionalReflection s) = Ξ.xi s := by
48 simpa [functionalReflection] using Ξ.reflection s
49
50/-- Conjugation symmetry of the completed-ξ value. -/
51theorem xi_conjugation_invariant (Ξ : CompletedXiSurface) (s : ℂ) :
52 Ξ.xi (conj s) = conj (Ξ.xi s) :=
53 Ξ.conjugation s
54
55/-- Zeros come in reflection pairs under the functional equation. -/
56theorem zero_pairing_under_reflection (Ξ : CompletedXiSurface) {s : ℂ}
57 (hs : Ξ.xi s = 0) :
58 Ξ.xi (functionalReflection s) = 0 := by
59 simpa [functionalReflection, hs] using Ξ.reflection s
60
61/-- Zeros come in conjugate pairs under reality symmetry. -/
62theorem zero_pairing_under_conjugation (Ξ : CompletedXiSurface) {s : ℂ}
63 (hs : Ξ.xi s = 0) :
64 Ξ.xi (conj s) = 0 := by
65 rw [Ξ.conjugation, hs]
66 simp
67
68/-- Zeros are stable under reflection composed with conjugation. -/