NormalizedOrder.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.NormalizedGrowth
6 
7 namespace Komorebi.PaperIV
8 noncomputable section
9 open Set Filter
10 open scoped Topology Classical
11 
12 /-- Every signed or unsigned residue weight leaves the dominant vertex term
13 unchanged on the positive real ray. -/
14 theorem entireTransfer_positive_ray {N : ℕ} (hN : 0 < N) (j : ℕ)
15     {ω : ℂ} (hω : IsPrimitiveRoot ω N) :
16     Tendsto (fun r : ℝ => (N : ℂ) * Complex.exp (-(r : ℂ)) * entireTransfer N j ω 1 r)
17       atTop (𝓝 1) := by
18   have hw : ‖ω‖ = 1 := Complex.norm_eq_one_of_pow_eq_one hω.pow_eq_one hN.ne'
19   have hk (k : ℕ) (hk : k ∈ (Finset.range N).erase 0) : (ω ^ k - 1).re < 0 := by
20     have hne : ω ^ k ≠ 1 := by
21       intro he
22       have := hω.pow_inj (Finset.mem_range.mp (Finset.mem_erase.mp hk).2) hN (he.trans (pow_zero ω).symm)
23       exact (Finset.mem_erase.mp hk).1 this
24     have := unit_complex_re_lt_one (by simp [norm_pow, hw]) hne
25     simpa using sub_neg.mpr this
26   have ht (k : ℕ) (hk' : k ∈ (Finset.range N).erase 0) :
27       Tendsto (fun r : ℝ => ((ω ^ j)⁻¹) ^ k * Complex.exp ((ω ^ k - 1) * (r : ℂ))) atTop (𝓝 0) := by
28     have he : Tendsto (fun r : ℝ => Complex.exp ((ω ^ k - 1) * (r : ℂ))) atTop (𝓝 0) := by
29       apply tendsto_zero_iff_norm_tendsto_zero.mpr
30       simp only [Complex.norm_exp, Complex.mul_re, Complex.ofReal_re, Complex.ofReal_im, mul_zero, sub_zero]
31       exact Real.tendsto_exp_atBot.comp (tendsto_id.const_mul_atTop_of_neg (hk k hk'))
32     simpa using he.const_mul (((ω ^ j)⁻¹) ^ k)
33   have htall := tendsto_finsetSum (s := (Finset.range N).erase 0) (fun k hk => ht k hk)
34   have htotal : Tendsto (fun r : ℝ =>
35       (∑ k ∈ (Finset.range N).erase 0, ((ω ^ j)⁻¹) ^ k * Complex.exp ((ω ^ k - 1) * (r : ℂ))) + 1)
36       atTop (𝓝 1) := by simpa using htall.add_const 1
37   apply htotal.congr
38   intro r
39   have hn : (N : ℂ) ≠ 0 := by exact_mod_cast hN.ne'
40   have he : (N : ℂ) * Complex.exp (-(r : ℂ)) * entireTransfer N j ω 1 r =
41       ∑ k ∈ Finset.range N, ((ω ^ j)⁻¹) ^ k * Complex.exp ((ω ^ k - 1) * (r : ℂ)) := by
42     calc
43       _ = Complex.exp (-(r : ℂ)) *
44           ∑ k ∈ Finset.range N, ((ω ^ j)⁻¹) ^ k * Complex.exp (ω ^ k * (r : ℂ)) := by
45         unfold entireTransfer
46         simp only [one_mul]
47         field_simp
48       _ = ∑ k ∈ Finset.range N, Complex.exp (-(r : ℂ)) *
49           (((ω ^ j)⁻¹) ^ k * Complex.exp (ω ^ k * (r : ℂ))) := Finset.mul_sum ..
50       _ = _ := by
51         apply Finset.sum_congr rfl
52         intro k _
53         rw [mul_left_comm, ← Complex.exp_add]
54         congr 2
55         ring
56   rw [he]
57   simpa using (Finset.sum_erase_add (Finset.range N) (fun k => ((ω ^ j)⁻¹) ^ k *
58     Complex.exp ((ω ^ k - 1) * (r : ℂ))) (Finset.mem_range.mpr hN))
59 
60 end
61 end Komorebi.PaperIV

Back to source controls