DominantExponential.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.SignedSectorConfinement
6 import Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
7 
8 namespace Komorebi.PaperIV
9 noncomputable section
10 open Set Filter
11 open scoped Topology
12 
13 /-- A finite collection of strictly positive gaps has a common positive bound. -/
14 theorem finite_positive_gap {s : Finset ℕ} {d : ℕ → ℝ}
15     (hd : ∀ i ∈ s, 0 < d i) : ∃ δ : ℝ, 0 < δ ∧ ∀ i ∈ s, δ ≤ d i := by
16   by_cases hs : s.Nonempty
17   · exact ⟨s.inf' hs d, (Finset.lt_inf'_iff hs).mpr hd, fun i hi => s.inf'_le d hi⟩
18   · exact ⟨1, by norm_num, by simp [Finset.not_nonempty_iff_eq_empty.mp hs]⟩
19 
20 /-- Quantitative one-term dominance of an actual finite exponential sum. -/
21 theorem finite_exponential_dominant_bound {s : Finset ℕ} {a : ℕ → ℂ}
22     {k : ℕ} (hk : k ∈ s) {u : ℂ} {δ r : ℝ} (hr : 0 ≤ r)
23     (hgap : ∀ i ∈ s.erase k, ((a i - a k) * u).re ≤ -δ) :
24     ‖Complex.exp (-(a k * ((r : ℂ) * u))) *
25       (∑ i ∈ s, Complex.exp (a i * ((r : ℂ) * u))) - 1‖ ≤
26       ((s.erase k).card : ℝ) * Real.exp (-δ * r) := by
27   rw [finite_one_term_normalization hk, add_sub_cancel_left]
28   calc
29     _ ≤ ∑ i ∈ s.erase k, ‖Complex.exp ((a i - a k) * ((r : ℂ) * u))‖ := norm_sum_le _ _
30     _ ≤ ∑ _i ∈ s.erase k, Real.exp (-δ * r) := by
31       apply Finset.sum_le_sum
32       intro i hi
33       rw [Complex.norm_exp]
34       apply Real.exp_le_exp.mpr
35       have he : ((a i - a k) * ((r : ℂ) * u)).re = ((a i - a k) * u).re * r := by
36         rw [show (a i - a k) * ((r : ℂ) * u) = ((a i - a k) * u) * (r : ℂ) by ring,
37           Complex.mul_re]
38         simp
39       rw [he]
40       exact mul_le_mul_of_nonneg_right (hgap i hi) hr
41     _ = _ := by simp
42 
43 theorem finite_exponential_dominant_tendsto {s : Finset ℕ} {a : ℕ → ℂ}
44     {k : ℕ} (hk : k ∈ s) {u : ℂ}
45     (hgap : ∀ i ∈ s.erase k, (a i * u).re < (a k * u).re) :
46     Tendsto (fun r : ℝ => Complex.exp (-(a k * ((r : ℂ) * u))) *
47       (∑ i ∈ s, Complex.exp (a i * ((r : ℂ) * u)))) atTop (𝓝 1) := by
48   obtain ⟨δ, hδ, hδgap⟩ := finite_positive_gap (fun i hi => sub_pos.mpr (hgap i hi))
49   have ht : Tendsto (fun r : ℝ => ((s.erase k).card : ℝ) * Real.exp (-δ * r)) atTop (𝓝 0) := by
50     simpa only [mul_zero, neg_mul, Function.comp_apply, id_eq] using
51       (Real.tendsto_exp_neg_atTop_nhds_zero.comp (tendsto_id.const_mul_atTop hδ)).const_mul ((s.erase k).card : ℝ)
52   apply tendsto_iff_norm_sub_tendsto_zero.mpr
53   apply squeeze_zero' (Eventually.of_forall (fun _ => norm_nonneg _)) _ ht
54   filter_upwards [eventually_ge_atTop (0 : ℝ)] with r hr
55   exact finite_exponential_dominant_bound hk hr (fun i hi => by
56     rw [sub_mul, Complex.sub_re]; linarith [hδgap i hi])
57 
58 /-- A unit complex number has real part strictly below one unless it is one. -/
59 theorem unit_complex_re_lt_one {a : ℂ} (ha : ‖a‖ = 1) (h : a ≠ 1) : a.re < 1 := by
60   have he := Complex.re_le_norm a
61   rw [ha] at he
62   apply lt_of_le_of_ne he
63   intro hr
64   have hi : a.im = 0 := by
65     have hs := Complex.sq_norm_sub_sq_re a
66     rw [ha, hr] at hs
67     nlinarith [sq_nonneg a.im]
68   apply h
69   exact Complex.ext hr (by simpa using hi)
70 
71 theorem canonicalSignedVertex_injective {N : ℕ} (hN : 0 < N) :
72     Set.InjOn (canonicalSignedVertex N) (↑(Finset.range N) : Set ℕ) := by
73   intro i hi j hj he
74   apply (canonicalPrimitiveRoot_isPrimitive hN).pow_inj
75     (Finset.mem_range.mp hi) (Finset.mem_range.mp hj)
76   exact mul_left_cancel₀ (by rw [← norm_ne_zero_iff, norm_signedRoot hN (canonicalSignedRoot_pow hN)]; exact one_ne_zero) he
77 
78 theorem canonicalSignedVertex_mul_star_self (N k : ℕ) :
79     canonicalSignedVertex N k * star (canonicalSignedVertex N k) = 1 := by
80   rw [Complex.star_def, Complex.mul_conj, Complex.normSq_eq_norm_sq, norm_canonicalSignedVertex]
81   norm_num
82 
83 /-- Looking straight toward any polygon vertex gives a strictly dominant term. -/
84 theorem canonicalSignedDenominator_dominant_ray {N : ℕ} (hN : 0 < N)
85     {k : ℕ} (hk : k < N) :
86     Tendsto (fun r : ℝ => (N : ℂ) * Complex.exp (-(r : ℂ)) *
87       canonicalSignedDenominator N ((r : ℂ) * star (canonicalSignedVertex N k))) atTop (𝓝 1) := by
88   have h := finite_exponential_dominant_tendsto (a := canonicalSignedVertex N)
89     (Finset.mem_range.mpr hk) (u := star (canonicalSignedVertex N k)) (fun i hi => ?_)
90   · convert! h using 1
91     funext r
92     rw [show canonicalSignedVertex N k * ((r : ℂ) * star (canonicalSignedVertex N k)) = (r : ℂ) by
93       rw [mul_left_comm, canonicalSignedVertex_mul_star_self, mul_one]]
94     unfold canonicalSignedDenominator
95     rw [entireSigned_zero_eq_average]
96     have hn : (N : ℂ) ≠ 0 := by exact_mod_cast hN.ne'
97     dsimp [canonicalSignedVertex]
98     field_simp
99     apply Finset.sum_congr rfl
100     intro i _
101     congr 1
102     ring
103   · rw [canonicalSignedVertex_mul_star_self]
104     apply unit_complex_re_lt_one (by simp [norm_canonicalSignedVertex])
105     intro he
106     have hij := mul_right_cancel₀
107       (show star (canonicalSignedVertex N k) ≠ 0 by rw [← norm_ne_zero_iff]; simp [norm_canonicalSignedVertex])
108       (he.trans (canonicalSignedVertex_mul_star_self N k).symm)
109     exact (Finset.mem_erase.mp hi).1 (canonicalSignedVertex_injective hN
110       (Finset.mem_erase.mp hi).2 (Finset.mem_range.mpr hk) hij)
111 
112 end
113 end Komorebi.PaperIV

Back to source controls