ExponentialBounds.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.CompanionCompletion
6 
7 /-! # Canonical roots and analytic growth bounds -/
8 
9 namespace Komorebi.PaperIV
10 noncomputable section
11 
12 def canonicalPrimitiveRoot (N : ℕ) : ℂ :=
13   Complex.exp (2 * (Real.pi : ℂ) * Complex.I / N)
14 
15 def canonicalSignedRoot (N : ℕ) : ℂ :=
16   Complex.exp ((Real.pi : ℂ) * Complex.I / N)
17 
18 theorem canonicalPrimitiveRoot_isPrimitive {N : ℕ} (hN : 0 < N) :
19     IsPrimitiveRoot (canonicalPrimitiveRoot N) N :=
20   Complex.isPrimitiveRoot_exp N hN.ne'
21 
22 theorem canonicalSignedRoot_pow {N : ℕ} (hN : 0 < N) :
23     canonicalSignedRoot N ^ N = -1 := by
24   unfold canonicalSignedRoot
25   rw [← Complex.exp_nat_mul]
26   have hn : (N : ℂ) ≠ 0 := by exact_mod_cast hN.ne'
27   have he : (N : ℂ) * ((Real.pi : ℂ) * Complex.I / N) = (Real.pi : ℂ) * Complex.I := by
28     field_simp
29   rw [he, Complex.exp_pi_mul_I]
30 
31 /-- The determinant statement requires no root witnesses from the caller. -/
32 theorem signedFundamentalMatrix_det_one {N : ℕ} (hN : 1 < N) (z : ℂ) :
33     (signedFundamentalMatrix N z).det = 1 :=
34   signedFundamentalMatrix_det hN (canonicalPrimitiveRoot_isPrimitive (by omega))
35     (canonicalSignedRoot_pow (by omega)) z
36 
37 /-- Every root of minus one is on the unit circle. -/
38 theorem norm_signedRoot {N : ℕ} (hN : 0 < N) {rho : ℂ} (hrho : rho ^ N = -1) :
39     ‖rho‖ = 1 := by
40   apply Complex.norm_eq_one_of_pow_eq_one (n := N * 2)
41   · rw [pow_mul, hrho]
42     norm_num
43   · omega
44 
45 /-- The explicit global exponential-type upper bound from Proposition 11.2. -/
46 theorem norm_entireSigned_zero_le {N : ℕ} (hN : 0 < N)
47     {omega rho : ℂ} (homega : IsPrimitiveRoot omega N) (hrho : rho ^ N = -1)
48     (z : ℂ) :
49     ‖entireSigned N 0 omega rho z‖ ≤ Real.exp ‖z‖ := by
50   rw [entireSigned_zero_eq_average, norm_mul, norm_inv, Complex.norm_natCast]
51   have homegaNorm : ‖omega‖ = 1 :=
52     Complex.norm_eq_one_of_pow_eq_one homega.pow_eq_one hN.ne'
53   have ht (l : ℕ) : ‖Complex.exp ((rho * omega ^ l) * z)‖ ≤ Real.exp ‖z‖ := by
54     rw [Complex.norm_exp]
55     apply Real.exp_le_exp.mpr
56     calc
57       _ ≤ ‖(rho * omega ^ l) * z‖ := Complex.re_le_norm _
58       _ = ‖z‖ := by simp [norm_pow, norm_signedRoot hN hrho, homegaNorm]
59   calc
60     _ ≤ (N : ℝ)⁻¹ * ∑ l ∈ Finset.range N, ‖Complex.exp ((rho * omega ^ l) * z)‖ :=
61       mul_le_mul_of_nonneg_left (norm_sum_le _ _) (by positivity)
62     _ ≤ (N : ℝ)⁻¹ * ∑ _l ∈ Finset.range N, Real.exp ‖z‖ :=
63       mul_le_mul_of_nonneg_left (Finset.sum_le_sum (fun l _ => ht l)) (by positivity)
64     _ = Real.exp ‖z‖ := by simp [hN.ne']
65 
66 end
67 end Komorebi.PaperIV

Back to source controls