OrbitPoleReduction.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.LeadingPoleBounds
6 
7 namespace Komorebi.PaperIV
8 noncomputable section
9 open Set Filter
10 open scoped Topology Classical
11 
12 def leadingZeroWeight (N r m : ℕ) (ρ : ℂ) : ℂ :=
13   ((-ρ * deriv (canonicalSignedDenominator N) ρ) ^ r)⁻¹ * ρ⁻¹ ^ m
14 
15 theorem leadingZeroWeight_rotation {N : ℕ} (hN : 0 < N) {u : ℂ} (hu : u ^ N = 1)
16     (r n : ℕ) (ρ : ℂ) : leadingZeroWeight N r (N*n) (u*ρ) = leadingZeroWeight N r (N*n) ρ := by
17   have hd := canonicalSignedDenominator_derivative_rotation hN hu ρ
18   have he : -(u*ρ) * deriv (canonicalSignedDenominator N) (u*ρ) =
19       -ρ * deriv (canonicalSignedDenominator N) ρ := by
20     calc
21       _ = -ρ * (deriv (canonicalSignedDenominator N) (u*ρ) * u) := by ring
22       _ = _ := by rw [hd]
23   have hp : u ^ (N*n) = 1 := by rw [pow_mul, hu, one_pow]
24   unfold leadingZeroWeight
25   rw [he, inv_pow, mul_pow u ρ, hp, one_mul, ← inv_pow ρ]
26 
27 theorem leadingPoleCoefficient_eq_zero_weights (S : Finset ℂ) (N r m : ℕ) :
28     leadingPoleCoefficient S (canonicalPoleCoefficient (canonicalSignedDenominator N) r) r m =
29       ((m+r-1).choose (r-1) : ℂ) * ∑ ρ ∈ S, leadingZeroWeight N r m ρ := by
30   simp only [leadingPoleCoefficient, canonicalPoleCoefficient_leading, leadingZeroWeight]
31 
32 /-- An equivalence records exactly the chosen representatives and all N
33 distinct rotations of each representative. -/
34 theorem leading_zero_sum_orbit_reduction {N : ℕ} (hN : 0 < N) {ω : ℂ}
35     (hω : IsPrimitiveRoot ω N) (S T : Finset ℂ) (e : (T × Fin N) ≃ S)
36     (he : ∀ p : T × Fin N, (e p).val = ω ^ p.2.val * p.1.val) (r n : ℕ) :
37     (∑ ρ ∈ S, leadingZeroWeight N r (N*n) ρ) =
38       (N : ℂ) * ∑ τ ∈ T, leadingZeroWeight N r (N*n) τ := by
39   calc
40     _ = ∑ ρ : S, leadingZeroWeight N r (N*n) ρ.val := (Finset.sum_coe_sort S _).symm
41     _ = ∑ p : T × Fin N, leadingZeroWeight N r (N*n) (e p).val := (Equiv.sum_comp e _).symm
42     _ = ∑ p : T × Fin N, leadingZeroWeight N r (N*n) p.1.val := by
43       apply Finset.sum_congr rfl
44       intro p _
45       rw [he]
46       apply leadingZeroWeight_rotation hN
47       rw [← pow_mul, Nat.mul_comm p.2.val N, pow_mul, hω.pow_eq_one, one_pow]
48     _ = (N : ℂ) * ∑ τ : T, leadingZeroWeight N r (N*n) τ.val := by
49       rw [Fintype.sum_prod_type]
50       simp [Finset.mul_sum, nsmul_eq_mul]
51     _ = _ := by rw [Finset.sum_coe_sort]
52 
53 /-- Corollary 13.3: the orbit-reduced main term has exactly N times the
54 representative sum; both proved error bounds are unchanged. -/
55 theorem reciprocalCoeff_orbit_leading_bound {N : ℕ} (hN : 0 < N) {ω : ℂ}
56     (hω : IsPrimitiveRoot ω N) (S T : Finset ℂ) (e : (T × Fin N) ≃ S)
57     (he : ∀ p : T × Fin N, (e p).val = ω ^ p.2.val * p.1.val)
58     {R Rstar R₂ : ℝ} (hR : 0 < R) (hRR : R < Rstar) (hR₂ : Rstar < R₂)
59     (hS : ∀ ρ ∈ S, ‖ρ‖ = R) (hroot : ∀ ρ ∈ S, canonicalSignedDenominator N ρ = 0)
60     (hsimple : ∀ ρ ∈ S, deriv (canonicalSignedDenominator N) ρ ≠ 0)
61     (hzeros : ∀ z : ℂ, ‖z‖ < R₂ → canonicalSignedDenominator N z = 0 → z ∈ S)
62     {r : ℕ} (hr : 0 < r) :
63     ∃ C : ℝ, ∀ n : ℕ, 1 ≤ n →
64       ‖reciprocalCoeff N n (r : ℂ) - (N : ℂ) * ((N*n).factorial : ℂ) *
65         ((N*n+r-1).choose (r-1) : ℂ) * ∑ τ ∈ T, leadingZeroWeight N r (N*n) τ‖ ≤
66       lowerPrincipalConstant S (canonicalPoleCoefficient (canonicalSignedDenominator N) r) r *
67         ((N*n).factorial : ℝ) * (N*n : ℝ) ^ (r-2) * R⁻¹ ^ (N*n) +
68       C * ((N*n).factorial : ℝ) * Rstar⁻¹ ^ (N*n) := by
69   obtain ⟨C, hC⟩ := reciprocalCoeff_leading_bound hN hR hRR hR₂ hS hroot hsimple hzeros hr
70   refine ⟨C, fun n hn => ?_⟩
71   have h := hC n hn
72   rw [leadingPoleCoefficient_eq_zero_weights, leading_zero_sum_orbit_reduction hN hω S T e he] at h
73   simpa only [mul_assoc, mul_comm, mul_left_comm] using h
74 
75 end
76 end Komorebi.PaperIV

Back to source controls