SignedFiniteExceptions.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.SignedZeroOrbits
6 import Mathlib.Analysis.Analytic.IsolatedZeros
7 
8 namespace Komorebi.PaperIV
9 noncomputable section
10 open Filter Metric Set
11 
12 @[simp] theorem canonicalSignedDenominator_zero {N : ℕ} (hN : 0 < N) :
13     canonicalSignedDenominator N 0 = 1 := by
14   rw [canonicalSignedDenominator, entireSigned_zero_eq_average]
15   simp [Nat.ne_of_gt hN]
16 
17 /-- Compact sets contain only finitely many zeros of the actual entire denominator. -/
18 theorem canonicalSignedDenominator_finite_zeros_on_compact {N : ℕ} (hN : 0 < N)
19     {K : Set ℂ} (hK : IsCompact K) :
20     {z ∈ K | canonicalSignedDenominator N z = 0}.Finite := by
21   have ha : AnalyticOnNhd ℂ (canonicalSignedDenominator N) univ :=
22     fun z _ => analyticAt_entireSigned N 0 _ _ z
23   have hn : ¬ EqOn (canonicalSignedDenominator N) 0 univ := by
24     intro h
25     have hh := h (mem_univ (0 : ℂ))
26     simp [canonicalSignedDenominator_zero hN] at hh
27   have he := (ha.eqOn_zero_or_eventually_ne_zero_of_preconnected isPreconnected_univ).resolve_left hn
28   have hk := (codiscreteWithin_mono (subset_univ K)) he
29   exact (hK.finite_sdiff_of_mem_codiscreteWithin hk).subset fun _ hz => ⟨hz.1, fun hn => hn hz.2⟩
30 
31 /-- A point belongs to one of the `N` positive root-of-unity rays. -/
32 def onSignedZeroRay (N : ℕ) (z : ℂ) : Prop :=
33   ∃ k < N, ∃ t : ℝ, 0 < t ∧ z = canonicalPrimitiveRoot N ^ k * (t : ℂ)
34 
35 theorem canonicalSignedDenominator_eventually_simple_on_rays {N : ℕ} (hN : 2 ≤ N) :
36     ∃ R : ℝ, 0 < R ∧ ∀ z : ℂ, R ≤ ‖z‖ → canonicalSignedDenominator N z = 0 →
37       analyticOrderAt (canonicalSignedDenominator N) z = 1 ∧ onSignedZeroRay N z := by
38   let : NeZero N := ⟨by omega⟩
39   have homega := canonicalPrimitiveRoot_isPrimitive (by omega : 0 < N)
40   rcases eq_or_lt_of_le hN with htwo | hthree
41   · subst N
42     refine ⟨1, by norm_num, ?_⟩
43     intro z _ hz
44     have hrho := canonicalSignedRoot_pow (by norm_num : 0 < 2)
45     refine ⟨entireSigned_two_zero_order_one homega hrho hz, ?_⟩
46     obtain ⟨m, hm | hm⟩ := (entireSigned_two_zero_iff_nat homega hrho).mp hz
47     · refine ⟨0, by omega, ((m : ℝ) + 1 / 2) * Real.pi, by positivity, ?_⟩
48       simpa using hm
49     · refine ⟨1, by omega, ((m : ℝ) + 1 / 2) * Real.pi, by positivity, ?_⟩
50       rw [pow_one, IsPrimitiveRoot.eq_neg_one_of_two_right homega]
51       simpa using hm
52   · obtain ⟨R, hR, hex⟩ := canonicalSignedDenominator_large_zero_orbits (by omega : 3 ≤ N) 0
53     refine ⟨R, hR, ?_⟩
54     intro z hz hz0
55     obtain ⟨k, _, m, _, _, hi, hp, hs⟩ := hex z hz hz0
56     have hu : (canonicalPrimitiveRoot N ^ k) ^ N = 1 := by
57       rw [← pow_mul, Nat.mul_comm, pow_mul, homega.pow_eq_one, one_pow]
58     have hui : ((canonicalPrimitiveRoot N ^ k)⁻¹) ^ N = 1 := by rw [inv_pow, hu, inv_one]
59     obtain ⟨j, hj, he⟩ := homega.eq_pow_of_pow_eq_one hui
60     have hu0 : canonicalPrimitiveRoot N ^ k ≠ 0 := by
61       intro h; simp [h, Nat.ne_of_gt (show 0 < N by omega)] at hu
62     refine ⟨hs, j, hj, (canonicalPrimitiveRoot N ^ k * z).re, hp, ?_⟩
63     have hzreal : ((canonicalPrimitiveRoot N ^ k * z).re : ℂ) = canonicalPrimitiveRoot N ^ k * z := by
64       apply Complex.ext <;> simp [hi]
65     rw [hzreal, he, ← mul_assoc, inv_mul_cancel₀ hu0, one_mul]
66 
67 /-- Corollary 11.11: the exceptional zeros form a finite set. -/
68 theorem canonicalSignedDenominator_finite_exceptional_zeros {N : ℕ} (hN : 2 ≤ N) :
69     {z : ℂ | canonicalSignedDenominator N z = 0 ∧
70       (analyticOrderAt (canonicalSignedDenominator N) z ≠ 1 ∨ ¬ onSignedZeroRay N z)}.Finite := by
71   obtain ⟨R, _, hex⟩ := canonicalSignedDenominator_eventually_simple_on_rays hN
72   apply (canonicalSignedDenominator_finite_zeros_on_compact (by omega : 0 < N)
73     (isCompact_closedBall (0 : ℂ) R)).subset
74   intro z hz
75   refine ⟨?_, hz.1⟩
76   rw [mem_closedBall, dist_zero_right]
77   by_contra h
78   have hh := hex z (le_of_lt (lt_of_not_ge h)) hz.1
79   exact hz.2.elim (fun h => h hh.1) (fun h => h hh.2)
80 
81 end
82 end Komorebi.PaperIV

Back to source controls