AlignedExponentialRadii.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.IndicatorGeometry
6 import Mathlib.Topology.Order.LiminfLimsup
7 
8 namespace Komorebi.PaperIV
9 noncomputable section
10 open Set Filter
11 open scoped Topology
12 
13 /-- Radii at which the two conjugate leading phases are both one. -/
14 def alignedRadii (b : ℝ) (n : ℕ) : ℝ :=
15   if b = 0 then (n : ℝ) else (2 * Real.pi / |b|) * n
16 
17 theorem alignedRadii_tendsto (b : ℝ) : Tendsto (alignedRadii b) atTop atTop := by
18   change Tendsto (fun n : ℕ => if b = 0 then (n : ℝ) else (2 * Real.pi / |b|) * n) atTop atTop
19   by_cases hb : b = 0
20   · simp only [hb, ite_true]
21     exact tendsto_natCast_atTop_atTop
22   · simp only [hb, ite_false]
23     have hC : 0 < 2 * Real.pi / |b| := div_pos (mul_pos (by norm_num) Real.pi_pos) (abs_pos.mpr hb)
24     exact (tendsto_natCast_atTop_atTop (R := ℝ)).const_mul_atTop hC
25 
26 theorem alignedRadii_phase (b : ℝ) (n : ℕ) :
27     Complex.exp (((b * alignedRadii b n : ℝ) : ℂ) * Complex.I) = 1 := by
28   by_cases hb : b = 0
29   · simp [alignedRadii, hb]
30   · by_cases hp : 0 < b
31     · have he : (((b * alignedRadii b n : ℝ) : ℂ) * Complex.I) =
32           (n : ℤ) * (2 * (Real.pi : ℂ) * Complex.I) := by
33         simp only [alignedRadii, ite_eq_right hb, abs_of_pos hp]
34         push_cast
35         field_simp [show (b : ℂ) ≠ 0 by exact_mod_cast hb]
36       rw [he, Complex.exp_int_mul_two_pi_mul_I]
37     · have hn : b < 0 := lt_of_le_of_ne (le_of_not_gt hp) hb
38       have he : (((b * alignedRadii b n : ℝ) : ℂ) * Complex.I) =
39           (-(n : ℤ)) * (2 * (Real.pi : ℂ) * Complex.I) := by
40         simp only [alignedRadii, ite_eq_right hb, abs_of_neg hn]
41         push_cast
42         field_simp [show (b : ℂ) ≠ 0 by exact_mod_cast hb]
43       rw [he]
44       simpa only [Int.cast_neg] using Complex.exp_int_mul_two_pi_mul_I (-(n : ℤ))
45 
46 /-- Equal maximal real parts on the unit circle have synchronized phases. -/
47 theorem alignedRadii_equal_projection {a b : ℂ} (ha : ‖a‖ = 1) (hb : ‖b‖ = 1)
48     (he : b.re = a.re) (n : ℕ) :
49     Complex.exp ((b - (a.re : ℂ)) * (alignedRadii a.im n : ℂ)) = 1 := by
50   have hphase : Complex.exp (((a.im * alignedRadii a.im n : ℝ) : ℂ) * Complex.I) = 1 :=
51     alignedRadii_phase a.im n
52   rcases unit_complex_same_real hb ha he with h | h
53   · rw [h]
54     have hx : (a - (a.re : ℂ)) * (alignedRadii a.im n : ℂ) =
55         (((a.im * alignedRadii a.im n : ℝ) : ℂ) * Complex.I) := by
56       apply Complex.ext <;> simp
57     rwa [hx]
58   · rw [h]
59     have hx : (star a - (a.re : ℂ)) * (alignedRadii a.im n : ℂ) =
60         -(((a.im * alignedRadii a.im n : ℝ) : ℂ) * Complex.I) := by
61       apply Complex.ext <;> simp
62     rw [hx, Complex.exp_neg, hphase, inv_one]
63 
64 /-- Every term below the maximal real part decays along the aligned radii. -/
65 theorem alignedRadii_lower_projection {a b : ℂ} (he : b.re < a.re) :
66     Tendsto (fun n => Complex.exp ((b - (a.re : ℂ)) * (alignedRadii a.im n : ℂ))) atTop (𝓝 0) := by
67   apply tendsto_zero_iff_norm_tendsto_zero.mpr
68   have ht := Real.tendsto_exp_neg_atTop_nhds_zero.comp
69     ((alignedRadii_tendsto a.im).const_mul_atTop (sub_pos.mpr he))
70   convert! ht using 1
71   funext n
72   rw [Complex.norm_exp]
73   congr 1
74   simp only [Complex.mul_re, Complex.sub_re, Complex.ofReal_re, Complex.sub_im, Complex.ofReal_im, mul_zero, sub_zero]
75   ring
76 
77 /-- For a finite sum with unit exponents, a positive number of aligned leading
78 terms survive. This proves a lower indicator sequence even on tie directions. -/
79 theorem finite_unit_exponential_aligned_limit {s : Finset ℕ} {a : ℕ → ℂ}
80     {k : ℕ} (hk : k ∈ s) (ha : ∀ i ∈ s, ‖a i‖ = 1)
81     (hmax : ∀ i ∈ s, (a i).re ≤ (a k).re) :
82     Tendsto (fun n => ∑ i ∈ s, Complex.exp ((a i - ((a k).re : ℂ)) * (alignedRadii (a k).im n : ℂ)))
83       atTop (𝓝 (((s.filter (fun i => (a i).re = (a k).re)).card : ℕ) : ℂ)) := by
84   have ht : ∀ i ∈ s, Tendsto
85       (fun n => Complex.exp ((a i - ((a k).re : ℂ)) * (alignedRadii (a k).im n : ℂ)))
86       atTop (𝓝 (if (a i).re = (a k).re then (1 : ℂ) else 0)) := by
87     intro i hi
88     by_cases he : (a i).re = (a k).re
89     · simp only [ite_eq_left he]
90       have hfn : (fun n => Complex.exp ((a i - ((a k).re : ℂ)) * (alignedRadii (a k).im n : ℂ))) = fun _ => 1 :=
91         funext (alignedRadii_equal_projection (ha k hk) (ha i hi) he)
92       rw [hfn]
93       exact tendsto_const_nhds
94     · simp only [ite_eq_right he]
95       exact alignedRadii_lower_projection (lt_of_le_of_ne (hmax i hi) he)
96   simpa only [← Finset.sum_filter, Finset.sum_const, nsmul_eq_mul, mul_one] using tendsto_finsetSum s ht
97 
98 /-- A nonzero exponential normalization identifies the logarithmic slope. -/
99 theorem log_norm_slope_of_normalized_limit {r : ℕ → ℝ} {F : ℕ → ℂ} {h : ℝ} {c : ℂ}
100     (hr : Tendsto r atTop atTop) (hc : c ≠ 0)
101     (hf : Tendsto (fun n => Complex.exp (-((h * r n : ℝ) : ℂ)) * F n) atTop (𝓝 c)) :
102     Tendsto (fun n => Real.log ‖F n‖ / r n) atTop (𝓝 h) := by
103   have ht : Tendsto (fun n => Real.log ‖Complex.exp (-((h * r n : ℝ) : ℂ)) * F n‖) atTop (𝓝 (Real.log ‖c‖)) := by
104     exact (Real.continuousAt_log (norm_ne_zero_iff.mpr hc)).tendsto.comp hf.norm
105   have hlim : Tendsto (fun n => h + Real.log ‖Complex.exp (-((h * r n : ℝ) : ℂ)) * F n‖ / r n) atTop (𝓝 h) := by
106     simpa using tendsto_const_nhds.add (ht.div_atTop hr)
107   apply hlim.congr'
108   filter_upwards [hr.eventually (eventually_gt_atTop (0 : ℝ)), hf.eventually_ne hc] with n hn hne
109   have hFn : F n ≠ 0 := (mul_ne_zero_iff.mp hne).2
110   rw [norm_mul, Complex.norm_exp, Complex.neg_re, Complex.ofReal_re,
111     Real.log_mul (Real.exp_ne_zero _) (norm_ne_zero_iff.mpr hFn), Real.log_exp]
112   field_simp
113   ring
114 
115 end
116 end Komorebi.PaperIV

Back to source controls