FullZeroCounting.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.ZeroEnumeration
6 
7 namespace Komorebi.PaperIV
8 noncomputable section
9 open Set Metric
10 
11 def SignedZeroEnumeration.orbitDisk {N : ℕ} (e : SignedZeroEnumeration N) (R : ℝ) : Set ℂ :=
12   e.orbit '' (univ ×ˢ {m | e.root m ≤ R})
13 
14 def SignedZeroEnumeration.exceptions {N : ℕ} (e : SignedZeroEnumeration N) : Set ℂ :=
15   zeroDisk (canonicalSignedDenominator N) e.radius \ range e.orbit
16 
17 theorem SignedZeroEnumeration.exceptions_finite {N : ℕ} (hN : 0 < N) (e : SignedZeroEnumeration N) :
18     e.exceptions.Finite := (canonicalSignedDenominator_zeroDisk_finite hN e.radius).sdiff
19 
20 theorem SignedZeroEnumeration.orbitDisk_finite_card {N : ℕ} (hN : 2 ≤ N)
21     (e : SignedZeroEnumeration N) {R : ℝ} (hR : 0 ≤ R) :
22     (e.orbitDisk R).Finite ∧ (e.orbitDisk R).ncard = N * sequenceCounting e.root R := by
23   have hf := (lattice_window_counting (div_pos Real.pi_pos (signed_sine_pos hN)) e.shift e.root e.windows hR).1
24   refine ⟨(finite_univ.prod hf).image e.orbit, ?_⟩
25   rw [SignedZeroEnumeration.orbitDisk, ncard_image_of_injective _ (e.orbit_injective (by omega)), ncard_prod]
26   simp [sequenceCounting]
27 
28 theorem SignedZeroEnumeration.orbitDisk_subset {N : ℕ} (hN : 0 < N)
29     (e : SignedZeroEnumeration N) (R : ℝ) :
30     e.orbitDisk R ⊆ zeroDisk (canonicalSignedDenominator N) R := by
31   rintro z ⟨p, hp, rfl⟩
32   exact ⟨(e.orbit_norm hN p).trans_le hp.2, (e.orbit_zero_simple hN p).1⟩
33 
34 theorem SignedZeroEnumeration.zeroDisk_subset_union {N : ℕ} (hN : 0 < N)
35     (e : SignedZeroEnumeration N) (R : ℝ) :
36     zeroDisk (canonicalSignedDenominator N) R ⊆ e.orbitDisk R ∪ e.exceptions := by
37   classical
38   intro z hz
39   by_cases hr : z ∈ range e.orbit
40   · obtain ⟨p, rfl⟩ := hr
41     apply Or.inl
42     exact ⟨p, ⟨mem_univ _, by change e.root p.2 ≤ R; rw [← e.orbit_norm hN p]; exact hz.1⟩, rfl⟩
43   · apply Or.inr
44     refine ⟨⟨?_, hz.2⟩, hr⟩
45     by_contra hb
46     obtain ⟨k, m, he⟩ := e.exhaustive z (le_of_lt (lt_of_not_ge hb)) hz.2
47     exact hr ⟨(k, m), he.symm⟩
48 
49 theorem SignedZeroEnumeration.weighted_count_bounds {N : ℕ} (hN : 2 ≤ N)
50     (e : SignedZeroEnumeration N) {R : ℝ} (hR : 0 ≤ R) :
51     N * sequenceCounting e.root R ≤ analyticZeroCount (canonicalSignedDenominator N) R ∧
52       analyticZeroCount (canonicalSignedDenominator N) R ≤ N * sequenceCounting e.root R +
53         finiteWeight (analyticOrderNatAt (canonicalSignedDenominator N)) e.exceptions := by
54   obtain ⟨hT, hc⟩ := e.orbitDisk_finite_card hN hR
55   have hw : ∀ z ∈ e.orbitDisk R, analyticOrderNatAt (canonicalSignedDenominator N) z = 1 := by
56     rintro _ ⟨p, _, rfl⟩
57     exact (e.orbit_zero_simple (by omega) p).2
58   have h := finiteWeight_between_tail_and_exceptions (analyticOrderNatAt (canonicalSignedDenominator N))
59     (canonicalSignedDenominator_zeroDisk_finite (by omega) R) hT (e.exceptions_finite (by omega))
60     (e.orbitDisk_subset (by omega) R) (e.zeroDisk_subset_union (by omega) R) hw
61   rwa [hc] at h
62 
63 /-- The full denominator disk count, including every exceptional multiplicity. -/
64 theorem canonicalSignedDenominator_zero_counting {N : ℕ} (hN : 2 ≤ N) :
65     ∃ K : ℝ, 0 < K ∧ ∀ R : ℝ, 0 ≤ R →
66       |(analyticZeroCount (canonicalSignedDenominator N) R : ℝ) -
67         ((N : ℝ) * Real.sin (Real.pi / N) / Real.pi) * R| ≤ K := by
68   let e := canonicalZeroEnumeration hN
69   let W := finiteWeight (analyticOrderNatAt (canonicalSignedDenominator N)) e.exceptions
70   refine ⟨(W : ℝ) + N * ((e.shift : ℝ) + 2) + 1, by positivity, ?_⟩
71   intro R hR
72   have hw := e.weighted_count_bounds hN hR
73   have hl : (N : ℝ) * sequenceCounting e.root R ≤ analyticZeroCount (canonicalSignedDenominator N) R := by
74     exact_mod_cast hw.1
75   have hu : (analyticZeroCount (canonicalSignedDenominator N) R : ℝ) ≤
76       N * sequenceCounting e.root R + W := by exact_mod_cast hw.2
77   have hc := (lattice_window_counting (div_pos Real.pi_pos (signed_sine_pos hN))
78     e.shift e.root e.windows hR).2
79   rw [abs_le] at hc ⊢
80   have he : ((N : ℝ) * Real.sin (Real.pi / N) / Real.pi) * R =
81       N * (R / (Real.pi / Real.sin (Real.pi / N))) := by field_simp
82   rw [he]
83   have hn := Nat.cast_nonneg (α := ℝ) N
84   constructor <;> nlinarith
85 
86 end
87 end Komorebi.PaperIV

Back to source controls