ReducedZeros.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.ReducedEntire
6 
7 namespace Komorebi.PaperIV
8 noncomputable section
9 open Metric Set
10 
11 theorem exists_complex_nth_root {N : ℕ} (hN : 0 < N) (w : ℂ) :
12     ∃ z : ℂ, z ^ N = w := by
13   by_cases hw : w = 0
14   · exact ⟨0, by simp [hw, hN.ne']⟩
15   refine ⟨Complex.exp (Complex.log w / N), ?_⟩
16   rw [← Complex.exp_nat_mul, mul_div_cancel₀ _ (Nat.cast_ne_zero.mpr hN.ne'), Complex.exp_log hw]
17 
18 theorem entireReducedDenominator_zero_ne_zero {N : ℕ} {w : ℂ}
19     (hw : entireReducedDenominator N w = 0) : w ≠ 0 := by
20   intro h; simp [h] at hw
21 
22 theorem entireReducedDenominator_finite_zeros_on_compact {N : ℕ} (hN : 0 < N)
23     {K : Set ℂ} (hK : IsCompact K) :
24     {w ∈ K | entireReducedDenominator N w = 0}.Finite := by
25   have ha : AnalyticOnNhd ℂ (entireReducedDenominator N) univ :=
26     fun w _ => analyticAt_entireReducedDenominator hN w
27   have hn : ¬ EqOn (entireReducedDenominator N) 0 univ := by
28     intro h
29     have hh := h (mem_univ (0 : ℂ))
30     simp at hh
31   have he := (ha.eqOn_zero_or_eventually_ne_zero_of_preconnected isPreconnected_univ).resolve_left hn
32   have hk := (Filter.codiscreteWithin_mono (subset_univ K)) he
33   exact (hK.finite_sdiff_of_mem_codiscreteWithin hk).subset fun _ hz => ⟨hz.1, fun hn => hn hz.2⟩
34 
35 theorem onSignedZeroRay_power_positive {N : ℕ} (hN : 0 < N) {z : ℂ}
36     (hz : onSignedZeroRay N z) : (z ^ N).im = 0 ∧ 0 < (z ^ N).re := by
37   obtain ⟨k, _, t, ht, rfl⟩ := hz
38   have hu : (canonicalPrimitiveRoot N ^ k) ^ N = 1 := by
39     rw [← pow_mul, Nat.mul_comm, pow_mul, (canonicalPrimitiveRoot_isPrimitive hN).pow_eq_one, one_pow]
40   rw [mul_pow, hu, one_mul, ← Complex.ofReal_pow]
41   exact ⟨rfl, pow_pos ht N⟩
42 
43 /-- The exceptional reduced zeros are a finite image of exceptional denominator zeros. -/
44 theorem entireReducedDenominator_finite_exceptional_zeros {N : ℕ} (hN : 2 ≤ N) :
45     {w : ℂ | entireReducedDenominator N w = 0 ∧
46       (analyticOrderAt (entireReducedDenominator N) w ≠ 1 ∨ w.im ≠ 0 ∨ w.re ≤ 0)}.Finite := by
47   apply ((canonicalSignedDenominator_finite_exceptional_zeros hN).image (fun z : ℂ => z ^ N)).subset
48   intro w hw
49   obtain ⟨z, hz⟩ := exists_complex_nth_root (by omega : 0 < N) w
50   have hz0 : z ≠ 0 := by
51     intro h; apply entireReducedDenominator_zero_ne_zero hw.1
52     rw [← hz, h, zero_pow (by omega : N ≠ 0)]
53   have hd : canonicalSignedDenominator N z = 0 := by
54     rw [canonicalSignedDenominator_eq_reduced_power (by omega), hz]; exact hw.1
55   refine ⟨z, ⟨hd, ?_⟩, hz⟩
56   by_contra h
57   push Not at h
58   have ho := canonicalSignedDenominator_order_eq_reduced (by omega : 0 < N) hz0
59   rw [hz] at ho
60   have hp := onSignedZeroRay_power_positive (by omega : 0 < N) h.2
61   rw [hz] at hp
62   rcases hw.2 with he | hi | hr
63   · exact he (ho.symm.trans h.1)
64   · exact hi hp.1
65   · exact not_le_of_gt hp.2 hr
66 
67 /-- Pointwise exhaustion and multiplicity for all sufficiently large reduced zeros. -/
68 theorem entireReducedDenominator_eventually_positive_simple {N : ℕ} (hN : 2 ≤ N) :
69     ∃ R : ℝ, 0 < R ∧ ∀ w : ℂ, R ≤ ‖w‖ → entireReducedDenominator N w = 0 →
70       analyticOrderAt (entireReducedDenominator N) w = 1 ∧ w.im = 0 ∧ 0 < w.re := by
71   obtain ⟨R, hR, hex⟩ := canonicalSignedDenominator_eventually_simple_on_rays hN
72   refine ⟨R ^ N, pow_pos hR N, ?_⟩
73   intro w hw hw0
74   obtain ⟨z, hz⟩ := exists_complex_nth_root (by omega : 0 < N) w
75   have hz0 : z ≠ 0 := by
76     intro h; apply entireReducedDenominator_zero_ne_zero hw0
77     rw [← hz, h, zero_pow (by omega : N ≠ 0)]
78   have hr : R ≤ ‖z‖ := by
79     by_contra h
80     have hp := pow_lt_pow_left₀ (lt_of_not_ge h) (norm_nonneg z) (by omega : N ≠ 0)
81     have hn : ‖z‖ ^ N = ‖w‖ := by rw [← norm_pow, hz]
82     linarith
83   have hd : canonicalSignedDenominator N z = 0 := by
84     rw [canonicalSignedDenominator_eq_reduced_power (by omega), hz]; exact hw0
85   obtain ⟨ho, hp⟩ := hex z hr hd
86   have hh := canonicalSignedDenominator_order_eq_reduced (by omega : 0 < N) hz0
87   rw [hz] at hh
88   refine ⟨hh.symm.trans ho, ?_⟩
89   simpa [hz] using onSignedZeroRay_power_positive (by omega : 0 < N) hp
90 
91 /-- The order-two reduced zeros are exactly the positive half-integer squares. -/
92 theorem entireReducedDenominator_two_zero_iff {w : ℂ} :
93     entireReducedDenominator 2 w = 0 ↔
94       ∃ m : ℕ, w = ((((m : ℂ) + 1 / 2) * Real.pi) ^ 2) := by
95   have homega := canonicalPrimitiveRoot_isPrimitive (by norm_num : 0 < 2)
96   have hrho := canonicalSignedRoot_pow (by norm_num : 0 < 2)
97   constructor
98   · intro hw
99     obtain ⟨z, hz⟩ := exists_complex_nth_root (by norm_num : 0 < 2) w
100     have hd : canonicalSignedDenominator 2 z = 0 := by
101       rw [canonicalSignedDenominator_eq_reduced_power (by norm_num), hz]; exact hw
102     obtain ⟨m, hm | hm⟩ := (entireSigned_two_zero_iff_nat homega hrho).mp hd
103     · exact ⟨m, by rw [← hz, hm]⟩
104     · exact ⟨m, by rw [← hz, hm, neg_sq]⟩
105   · rintro ⟨m, rfl⟩
106     rw [← canonicalSignedDenominator_eq_reduced_power (by norm_num)]
107     exact (entireSigned_two_zero_iff_nat homega hrho).mpr ⟨m, Or.inl rfl⟩
108 
109 theorem entireReducedDenominator_two_zero_order_one {w : ℂ}
110     (hw : entireReducedDenominator 2 w = 0) :
111     analyticOrderAt (entireReducedDenominator 2) w = 1 := by
112   obtain ⟨z, hz⟩ := exists_complex_nth_root (by norm_num : 0 < 2) w
113   have hz0 : z ≠ 0 := by
114     intro h; apply entireReducedDenominator_zero_ne_zero hw; rw [← hz, h, zero_pow two_ne_zero]
115   rw [← hz, ← canonicalSignedDenominator_order_eq_reduced (by norm_num) hz0]
116   apply entireSigned_two_zero_order_one (canonicalPrimitiveRoot_isPrimitive (by norm_num))
117     (canonicalSignedRoot_pow (by norm_num))
118   change canonicalSignedDenominator 2 z = 0
119   rw [canonicalSignedDenominator_eq_reduced_power (by norm_num), hz]; exact hw
120 
121 end
122 end Komorebi.PaperIV

Back to source controls