IndicatorGeometry.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.DominantExponential
6 import Mathlib.Topology.Order.Lattice
7 
8 namespace Komorebi.PaperIV
9 noncomputable section
10 open Set Filter
11 open scoped Topology
12 
13 def rayDirection (θ : ℝ) : ℂ := Complex.exp ((θ : ℂ) * Complex.I)
14 
15 theorem norm_rayDirection (θ : ℝ) : ‖rayDirection θ‖ = 1 :=
16   Complex.norm_exp_ofReal_mul_I θ
17 
18 def signedProjection (N : ℕ) (θ : ℝ) (k : ℕ) : ℝ :=
19   (canonicalSignedVertex N k * rayDirection θ).re
20 
21 def signedIndicator (N : ℕ) (hN : 0 < N) (θ : ℝ) : ℝ :=
22   (Finset.range N).sup' ⟨0, Finset.mem_range.mpr hN⟩ (signedProjection N θ)
23 
24 theorem signedProjection_cos (N k : ℕ) (θ : ℝ) :
25     signedProjection N θ k = Real.cos (θ + (2 * k + 1) * (Real.pi / N)) := by
26   unfold signedProjection rayDirection
27   rw [canonicalSignedVertex_exp, ← Complex.exp_add]
28   have he : (((2 * (k : ℝ) + 1) * (Real.pi / N) : ℝ) : ℂ) * Complex.I + (θ : ℂ) * Complex.I =
29       ((θ + (2 * k + 1) * (Real.pi / N) : ℝ) : ℂ) * Complex.I := by push_cast; ring
30   rw [he, Complex.exp_ofReal_mul_I_re]
31 
32 theorem signedIndicator_cos (N : ℕ) (hN : 0 < N) (θ : ℝ) :
33     signedIndicator N hN θ = (Finset.range N).sup' ⟨0, Finset.mem_range.mpr hN⟩
34       (fun k => Real.cos (θ + (2 * k + 1) * (Real.pi / N))) := by
35   unfold signedIndicator
36   congr 1
37   funext k
38   exact signedProjection_cos N k θ
39 
40 theorem continuous_signedProjection (N k : ℕ) : Continuous (fun θ => signedProjection N θ k) := by
41   simp only [signedProjection_cos]
42   fun_prop
43 
44 theorem continuous_signedIndicator (N : ℕ) (hN : 0 < N) : Continuous (signedIndicator N hN) :=
45   Continuous.finset_sup'_apply _ (fun k _ => continuous_signedProjection N k)
46 
47 theorem signedProjection_le_indicator {N k : ℕ} (hN : 0 < N) (hk : k < N) (θ : ℝ) :
48     signedProjection N θ k ≤ signedIndicator N hN θ :=
49   (Finset.range N).le_sup' _ (Finset.mem_range.mpr hk)
50 
51 theorem canonicalSignedVertex_sum_zero {N : ℕ} (hN : 2 ≤ N) :
52     ∑ k ∈ Finset.range N, canonicalSignedVertex N k = 0 := by
53   simp only [canonicalSignedVertex, ← Finset.mul_sum,
54     (canonicalPrimitiveRoot_isPrimitive (show 0 < N by omega)).geom_sum_eq_zero (show 1 < N by omega), mul_zero]
55 
56 theorem signedIndicator_nonneg {N : ℕ} (hN : 2 ≤ N) (θ : ℝ) :
57     0 ≤ signedIndicator N (by omega) θ := by
58   have he : (∑ k ∈ Finset.range N, signedProjection N θ k) = 0 := by
59     simp only [signedProjection, ← Complex.re_sum, ← Finset.sum_mul, canonicalSignedVertex_sum_zero hN, zero_mul, Complex.zero_re]
60   have hb := Finset.sum_le_sum (fun k hk => signedProjection_le_indicator (show 0 < N by omega) (Finset.mem_range.mp hk) θ)
61   rw [he] at hb
62   simp only [Finset.sum_const, Finset.card_range, nsmul_eq_mul] at hb
63   exact nonneg_of_mul_nonneg_right hb (by exact_mod_cast (show 0 < N by omega))
64 
65 theorem canonicalSignedVertex_pow {N : ℕ} (hN : 0 < N) (k : ℕ) :
66     canonicalSignedVertex N k ^ N = -1 := by
67   simp only [canonicalSignedVertex, mul_pow, pow_right_comm (canonicalPrimitiveRoot N) k N,
68     canonicalSignedRoot_pow hN, (canonicalPrimitiveRoot_isPrimitive hN).pow_eq_one, one_pow, mul_one]
69 
70 theorem signed_root_in_vertices {N : ℕ} (hN : 0 < N) {a : ℂ} (ha : a ^ N = -1) :
71     ∃ k < N, canonicalSignedVertex N k = a := by
72   have : NeZero N := ⟨hN.ne'⟩
73   have hρ : canonicalSignedRoot N ≠ 0 := by
74     rw [← norm_ne_zero_iff, norm_signedRoot hN (canonicalSignedRoot_pow hN)]; exact one_ne_zero
75   have hp : (a / canonicalSignedRoot N) ^ N = 1 := by
76     rw [div_pow, ha, canonicalSignedRoot_pow hN]; norm_num
77   obtain ⟨k, hk, he⟩ := (canonicalPrimitiveRoot_isPrimitive hN).eq_pow_of_pow_eq_one hp
78   refine ⟨k, hk, ?_⟩
79   rw [canonicalSignedVertex, he]
80   field_simp
81 
82 /-- Two points on the unit circle with equal real parts are equal or conjugate. -/
83 theorem unit_complex_same_real {a b : ℂ} (ha : ‖a‖ = 1) (hb : ‖b‖ = 1)
84     (hr : a.re = b.re) : a = b ∨ a = star b := by
85   have hsa := Complex.sq_norm_sub_sq_re a
86   have hsb := Complex.sq_norm_sub_sq_re b
87   rw [ha, hr] at hsa
88   rw [hb] at hsb
89   have he : (a.im - b.im) * (a.im + b.im) = 0 := by nlinarith
90   rcases mul_eq_zero.mp he with hm | hp
91   · exact Or.inl (Complex.ext hr (sub_eq_zero.mp hm))
92   · exact Or.inr (Complex.ext (by simpa using hr) (by simp only [Complex.star_def, Complex.conj_im]; linarith))
93 
94 /-- A tie between maximal projections is possible only on an Nth-root ray. -/
95 theorem signed_maximizer_strict_of_not_tie {N k : ℕ} (hN : 0 < N) {u : ℂ}
96     (hu : ‖u‖ = 1) (hnt : u ^ N ≠ 1) (hk : k < N)
97     (hmax : ∀ j < N, (canonicalSignedVertex N j * u).re ≤ (canonicalSignedVertex N k * u).re)
98     {l : ℕ} (hl : l < N) (hlk : l ≠ k) :
99     (canonicalSignedVertex N l * u).re < (canonicalSignedVertex N k * u).re := by
100   have hun : u ≠ 0 := by rw [← norm_ne_zero_iff, hu]; exact one_ne_zero
101   have hneq : canonicalSignedVertex N l * u ≠ canonicalSignedVertex N k * u := by
102     intro he
103     exact hlk (canonicalSignedVertex_injective hN (Finset.mem_range.mpr hl) (Finset.mem_range.mpr hk) (mul_right_cancel₀ hun he))
104   apply lt_of_le_of_ne (hmax l hl)
105   intro he
106   have hconj := (unit_complex_same_real (by simp [norm_canonicalSignedVertex, hu])
107     (by simp [norm_canonicalSignedVertex, hu]) he).resolve_left hneq
108   have hab : (canonicalSignedVertex N l * u) * (canonicalSignedVertex N k * u) = 1 := by
109     rw [hconj, mul_comm, Complex.star_def, Complex.mul_conj, Complex.normSq_eq_norm_sq]
110     simp [norm_canonicalSignedVertex, hu]
111   have hp := congrArg (fun z : ℂ => z ^ N) hab
112   simp only [mul_pow, canonicalSignedVertex_pow hN, one_pow] at hp
113   have hsq : (u ^ N) ^ 2 = 1 := by linear_combination hp
114   have hminus : u ^ N = -1 := (sq_eq_one_iff.mp hsq).resolve_left hnt
115   obtain ⟨j, hj, hju⟩ := signed_root_in_vertices hN (a := u⁻¹) (by rw [inv_pow, hminus]; norm_num)
116   have hjone : canonicalSignedVertex N j * u = 1 := by rw [hju, inv_mul_cancel₀ hun]
117   have hkone : canonicalSignedVertex N k * u = 1 := by
118     by_contra hn
119     have ht := unit_complex_re_lt_one (by simp [norm_canonicalSignedVertex, hu]) hn
120     have hh := hmax j hj
121     rw [hjone] at hh
122     exact (not_lt_of_ge hh) ht
123   have hlone : canonicalSignedVertex N l * u = 1 := by
124     by_contra hn
125     have ht := unit_complex_re_lt_one (by simp [norm_canonicalSignedVertex, hu]) hn
126     rw [he, hkone] at ht
127     exact lt_irrefl _ ht
128   exact hneq (hlone.trans hkone.symm)
129 
130 /-- Tie directions, including all periods, in the manuscript's normalization. -/
131 def signedTieDirection (N : ℕ) (θ : ℝ) : Prop :=
132   ∃ k : ℤ, θ = 2 * Real.pi * k / N
133 
134 theorem signedTieDirection_iff {N : ℕ} (hN : 0 < N) (θ : ℝ) :
135     signedTieDirection N θ ↔ rayDirection θ ^ N = 1 := by
136   rw [rayDirection, ← Complex.exp_nat_mul, Complex.exp_eq_one_iff]
137   constructor
138   · rintro ⟨k, rfl⟩
139     refine ⟨k, ?_⟩
140     have hn : (N : ℂ) ≠ 0 := by exact_mod_cast hN.ne'
141     push_cast
142     field_simp
143   · rintro ⟨k, hk⟩
144     refine ⟨k, ?_⟩
145     have he := congrArg Complex.im hk
146     simp only [Complex.mul_im, Complex.mul_re, Complex.natCast_re, Complex.natCast_im,
147       Complex.intCast_re, Complex.intCast_im, Complex.ofReal_re, Complex.ofReal_im,
148       Complex.I_im, Complex.I_re] at he
149     have hn : (N : ℝ) ≠ 0 := by exact_mod_cast hN.ne'
150     apply (eq_div_iff hn).mpr
151     norm_num at he
152     linear_combination he
153 
154 end
155 end Komorebi.PaperIV

Back to source controls