FullZeroSummability.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.ReducedZeroCounting
6 import Mathlib.Topology.Algebra.InfiniteSum.Real
7 
8 namespace Komorebi.PaperIV
9 noncomputable section
10 open Set Filter Asymptotics
11 
12 /-- Reciprocal-power convergence over all distinct zeros, weighted by their
13 actual analytic multiplicity. -/
14 def ZeroPowerSummable (f : ℂ → ℂ) (s : ℝ) : Prop :=
15   Summable (fun z : {z : ℂ // f z = 0} =>
16     (analyticOrderNatAt f z : ℝ) / ‖(z : ℂ)‖ ^ s)
17 
18 theorem summable_iff_comp_of_finite_complement {α β : Type*} (i : α → β)
19     (hi : Function.Injective i) (hc : (range i)ᶜ.Finite) (f : β → ℝ) :
20     Summable f ↔ Summable (f ∘ i) := by
21   have h : Summable (fun x : range i => f x) ↔ Summable f := by
22     have h := hc.summable_compl_iff (f := f)
23     rw [compl_compl] at h
24     exact h
25   rw [← h]
26   exact exists_congr (fun _ => hi.hasSum_range_iff)
27 
28 theorem SignedZeroEnumeration.root_equivalent_lattice {N : ℕ} (hN : 2 ≤ N)
29     (e : SignedZeroEnumeration N) :
30     e.root ~[atTop] (fun m : ℕ => (Real.pi / Real.sin (Real.pi / N)) * m) := by
31   let A := Real.pi / Real.sin (Real.pi / N)
32   have hA : 0 < A := div_pos Real.pi_pos (signed_sine_pos hN)
33   have hb : (fun m : ℕ => e.root m - A * m) =O[atTop] (fun _ => (1 : ℝ)) := by
34     apply isBigO_iff.mpr
35     refine ⟨A * e.shift, ?_⟩
36     filter_upwards [] with m
37     have hw := e.windows m
38     rw [norm_one, mul_one, Real.norm_eq_abs, abs_le]
39     dsimp [A] at *
40     constructor <;> nlinarith
41   have ht : Tendsto (fun m : ℕ => ‖A * (m : ℝ)‖) atTop atTop := by
42     simpa only [Real.norm_eq_abs, abs_of_nonneg (mul_nonneg hA.le (Nat.cast_nonneg _))] using
43       (tendsto_natCast_atTop_atTop (R := ℝ)).const_mul_atTop hA
44   exact hb.trans_isLittleO (isLittleO_const_left.mpr (Or.inr ht))
45 
46 theorem SignedZeroEnumeration.root_reciprocal_rpow_summable_iff {N : ℕ} (hN : 2 ≤ N)
47     (e : SignedZeroEnumeration N) (s : ℝ) :
48     Summable (fun m => 1 / e.root m ^ s) ↔ 1 < s := by
49   let A := Real.pi / Real.sin (Real.pi / N)
50   have hA : 0 < A := div_pos Real.pi_pos (signed_sine_pos hN)
51   have hp : 0 ≤ (fun m : ℕ => A * m) := fun m => mul_nonneg hA.le (Nat.cast_nonneg m)
52   have he := (IsEquivalent.rpow hp (e.root_equivalent_lattice hN) (r := s)).inv
53   have heq : (fun m => 1 / e.root m ^ s) ~[atTop]
54       (fun m : ℕ => 1 / (A * m) ^ s) := by simpa only [one_div] using! he
55   rw [heq.summable_iff_nat]
56   have hf : (fun m : ℕ => 1 / (A * m) ^ s) =
57       (fun m : ℕ => (1 / A ^ s) * (1 / (m : ℝ) ^ s)) := by
58     funext m
59     rw [Real.mul_rpow hA.le (Nat.cast_nonneg m)]
60     ring
61   rw [hf, summable_mul_left_iff (one_div_ne_zero (ne_of_gt (Real.rpow_pos_of_pos hA s)))]
62   exact Real.summable_one_div_nat_rpow
63 
64 theorem SignedZeroEnumeration.reducedRoot_reciprocal_rpow_summable_iff {N : ℕ} (hN : 2 ≤ N)
65     (e : SignedZeroEnumeration N) (s : ℝ) :
66     Summable (fun m => 1 / ‖e.reducedRoot m‖ ^ s) ↔ 1 < (N : ℝ) * s := by
67   have he : (fun m => 1 / ‖e.reducedRoot m‖ ^ s) =
68       (fun m => 1 / e.root m ^ ((N : ℝ) * s)) := by
69     funext m
70     rw [e.reducedRoot_norm, ← Real.rpow_natCast_mul (e.positive m).le]
71   rw [he]
72   exact e.root_reciprocal_rpow_summable_iff hN _
73 
74 def SignedZeroEnumeration.orbitZero {N : ℕ} (hN : 0 < N) (e : SignedZeroEnumeration N)
75     (p : Fin N × ℕ) : {z : ℂ // canonicalSignedDenominator N z = 0} :=
76   ⟨e.orbit p, (e.orbit_zero_simple hN p).1⟩
77 
78 theorem SignedZeroEnumeration.orbitZero_injective {N : ℕ} (hN : 0 < N)
79     (e : SignedZeroEnumeration N) : Function.Injective (e.orbitZero hN) := by
80   intro p q h
81   exact e.orbit_injective hN (congrArg Subtype.val h)
82 
83 theorem SignedZeroEnumeration.orbitZero_finite_complement {N : ℕ} (hN : 0 < N)
84     (e : SignedZeroEnumeration N) : (range (e.orbitZero hN))ᶜ.Finite := by
85   have hf : (Subtype.val ⁻¹' e.exceptions : Set {z : ℂ // canonicalSignedDenominator N z = 0}).Finite :=
86     (e.exceptions_finite hN).preimage Subtype.val_injective.injOn
87   apply hf.subset
88   intro z hz
89   have hd : (z : ℂ) ∈ zeroDisk (canonicalSignedDenominator N) ‖(z : ℂ)‖ := ⟨le_rfl, z.property⟩
90   rcases e.zeroDisk_subset_union hN _ hd with ht | he
91   · obtain ⟨p, _, hp⟩ := ht
92     exact False.elim (hz ⟨p, Subtype.ext hp⟩)
93   · exact he
94 
95 def SignedZeroEnumeration.reducedZero {N : ℕ} (hN : 0 < N) (e : SignedZeroEnumeration N)
96     (m : ℕ) : {z : ℂ // entireReducedDenominator N z = 0} :=
97   ⟨e.reducedRoot m, (e.reducedRoot_zero_simple hN m).1⟩
98 
99 theorem SignedZeroEnumeration.reducedZero_injective {N : ℕ} (hN : 0 < N)
100     (e : SignedZeroEnumeration N) : Function.Injective (e.reducedZero hN) := by
101   intro m n h
102   exact e.reducedRoot_injective hN (congrArg Subtype.val h)
103 
104 theorem SignedZeroEnumeration.reducedZero_finite_complement {N : ℕ} (hN : 0 < N)
105     (e : SignedZeroEnumeration N) : (range (e.reducedZero hN))ᶜ.Finite := by
106   have hf : (Subtype.val ⁻¹' e.reducedExceptions : Set {z : ℂ // entireReducedDenominator N z = 0}).Finite :=
107     (e.reducedExceptions_finite hN).preimage Subtype.val_injective.injOn
108   apply hf.subset
109   intro z hz
110   let r := ‖(z : ℂ)‖ ^ (1 / (N : ℝ))
111   have hr : 0 ≤ r := Real.rpow_nonneg (norm_nonneg (z : ℂ)) _
112   have hp : r ^ N = ‖(z : ℂ)‖ := by
113     simpa only [r, one_div] using Real.rpow_inv_natCast_pow (norm_nonneg (z : ℂ)) hN.ne'
114   have hd : (z : ℂ) ∈ zeroDisk (entireReducedDenominator N) (r ^ N) :=
115     ⟨hp.ge, z.property⟩
116   rcases e.reducedZeroDisk_subset_union hN hr hd with ht | he
117   · obtain ⟨m, _, hm⟩ := ht
118     exact False.elim (hz ⟨m, Subtype.ext hm⟩)
119   · exact he
120 
121 /-- The convergence exponent of the full denominator zero multiset is exactly one. -/
122 theorem canonicalSignedDenominator_zero_power_summable_iff {N : ℕ} (hN : 2 ≤ N) (s : ℝ) :
123     ZeroPowerSummable (canonicalSignedDenominator N) s ↔ 1 < s := by
124   let e := canonicalZeroEnumeration hN
125   have hn : 0 < N := by omega
126   unfold ZeroPowerSummable
127   rw [summable_iff_comp_of_finite_complement (e.orbitZero hn) (e.orbitZero_injective hn)
128     (e.orbitZero_finite_complement hn)]
129   have he : ((fun z : {z : ℂ // canonicalSignedDenominator N z = 0} =>
130       (analyticOrderNatAt (canonicalSignedDenominator N) z : ℝ) / ‖(z : ℂ)‖ ^ s) ∘ e.orbitZero hn) =
131       (fun p : Fin N × ℕ => 1 / e.root p.2 ^ s) := by
132     funext p
133     simp only [Function.comp_apply, SignedZeroEnumeration.orbitZero,
134       (e.orbit_zero_simple hn p).2, Nat.cast_one, e.orbit_norm hn]
135   rw [he]
136   have hp : Summable (fun p : Fin N × ℕ => 1 / e.root p.2 ^ s) ↔
137       Summable (fun m => 1 / e.root m ^ s) := by
138     constructor
139     · intro h
140       exact h.prod_factor ⟨0, hn⟩
141     · intro h
142       exact (summable_prod_of_nonneg (f := fun p : Fin N × ℕ => 1 / e.root p.2 ^ s) (fun p => (one_div_pos.mpr (Real.rpow_pos_of_pos (e.positive p.2) s)).le)).mpr
143         ⟨fun _ => h, (hasSum_fintype _).summable⟩
144   rw [hp]
145   exact e.root_reciprocal_rpow_summable_iff hN s
146 
147 /-- The convergence exponent of the full reduced zero multiset is exactly 1/N. -/
148 theorem entireReducedDenominator_zero_power_summable_iff {N : ℕ} (hN : 2 ≤ N) (s : ℝ) :
149     ZeroPowerSummable (entireReducedDenominator N) s ↔ 1 / (N : ℝ) < s := by
150   let e := canonicalZeroEnumeration hN
151   have hn : 0 < N := by omega
152   unfold ZeroPowerSummable
153   rw [summable_iff_comp_of_finite_complement (e.reducedZero hn) (e.reducedZero_injective hn)
154     (e.reducedZero_finite_complement hn)]
155   have he : ((fun z : {z : ℂ // entireReducedDenominator N z = 0} =>
156       (analyticOrderNatAt (entireReducedDenominator N) z : ℝ) / ‖(z : ℂ)‖ ^ s) ∘ e.reducedZero hn) =
157       (fun m => 1 / ‖e.reducedRoot m‖ ^ s) := by
158     funext m
159     simp only [Function.comp_apply, SignedZeroEnumeration.reducedZero,
160       (e.reducedRoot_zero_simple hn m).2, Nat.cast_one]
161   rw [he, e.reducedRoot_reciprocal_rpow_summable_iff hN]
162   rw [div_lt_iff₀ (by exact_mod_cast hn : (0 : ℝ) < N), mul_comm s]
163 
164 theorem entireReducedDenominator_reciprocal_zeros_summable {N : ℕ} (hN : 2 ≤ N) :
165     ZeroPowerSummable (entireReducedDenominator N) 1 := by
166   apply (entireReducedDenominator_zero_power_summable_iff hN 1).mpr
167   rw [div_lt_one (by exact_mod_cast (show 0 < N by omega) : (0 : ℝ) < N)]
168   exact_mod_cast (show 1 < N by omega)
169 
170 end
171 end Komorebi.PaperIV

Back to source controls