WeightedZeroCounts.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.ZeroSequenceCounting
6 
7 namespace Komorebi.PaperIV
8 noncomputable section
9 open Set Metric
10 
11 /-- Sum of natural weights over a finite set. The infinite-set fallback is never
12 used for the zero disks considered below. -/
13 def finiteWeight {α : Type*} (w : α → ℕ) (s : Set α) : ℕ := by
14   classical
15   exact if hs : s.Finite then ∑ x ∈ hs.toFinset, w x else 0
16 
17 theorem finiteWeight_of_finite {α : Type*} (w : α → ℕ) {s : Set α} (hs : s.Finite) :
18     finiteWeight w s = ∑ x ∈ hs.toFinset, w x := by
19   classical
20   unfold finiteWeight
21   rw [dite_eq_left hs]
22 
23 theorem finiteWeight_mono {α : Type*} (w : α → ℕ) {s t : Set α}
24     (hs : s.Finite) (ht : t.Finite) (hst : s ⊆ t) : finiteWeight w s ≤ finiteWeight w t := by
25   classical
26   rw [finiteWeight_of_finite w hs, finiteWeight_of_finite w ht]
27   exact Finset.sum_le_sum_of_subset_of_nonneg (hs.toFinset_mono hst) (fun _ _ _ => Nat.zero_le _)
28 
29 theorem finiteWeight_union_le {α : Type*} (w : α → ℕ) {s t : Set α}
30     (hs : s.Finite) (ht : t.Finite) :
31     finiteWeight w (s ∪ t) ≤ finiteWeight w s + finiteWeight w t := by
32   classical
33   rw [finiteWeight_of_finite w (hs.union ht), finiteWeight_of_finite w hs,
34     finiteWeight_of_finite w ht, Set.Finite.toFinset_union hs ht (hs.union ht)]
35   have h := Finset.sum_union_inter (s₁ := hs.toFinset) (s₂ := ht.toFinset) (f := w)
36   omega
37 
38 theorem finiteWeight_eq_ncard {α : Type*} {w : α → ℕ} {s : Set α}
39     (hs : s.Finite) (hw : ∀ x ∈ s, w x = 1) : finiteWeight w s = s.ncard := by
40   rw [finiteWeight_of_finite w hs, ncard_eq_toFinset_card s hs]
41   calc
42     _ = ∑ x ∈ hs.toFinset, (1 : ℕ) := Finset.sum_congr rfl (fun x hx => hw x (hs.mem_toFinset.mp hx))
43     _ = _ := by simp
44 
45 
46 /-- A finite exceptional set contributes at most its total multiplicity. -/
47 theorem finiteWeight_between_tail_and_exceptions {α : Type*} (w : α → ℕ)
48     {S T E : Set α} (hS : S.Finite) (hT : T.Finite) (hE : E.Finite)
49     (hTS : T ⊆ S) (hSTE : S ⊆ T ∪ E) (hw : ∀ x ∈ T, w x = 1) :
50     T.ncard ≤ finiteWeight w S ∧ finiteWeight w S ≤ T.ncard + finiteWeight w E := by
51   have ht := finiteWeight_eq_ncard hT hw
52   constructor
53   · rw [← ht]; exact finiteWeight_mono w hT hS hTS
54   · calc
55       _ ≤ finiteWeight w (T ∪ E) := finiteWeight_mono w hS (hT.union hE) hSTE
56       _ ≤ finiteWeight w T + finiteWeight w E := finiteWeight_union_le w hT hE
57       _ = _ := by rw [ht]
58 
59 /-- The actual zeros in a closed disk. -/
60 def zeroDisk (f : ℂ → ℂ) (R : ℝ) : Set ℂ := {z | ‖z‖ ≤ R ∧ f z = 0}
61 
62 /-- The manuscript's disk count, including analytic multiplicity. -/
63 def analyticZeroCount (f : ℂ → ℂ) (R : ℝ) : ℕ :=
64   finiteWeight (analyticOrderNatAt f) (zeroDisk f R)
65 
66 /-- Nonzero entire functions have finite analytic order at every point. -/
67 theorem entire_analyticOrderAt_ne_top {f : ℂ → ℂ} (hf : ∀ z, AnalyticAt ℂ f z)
68     {a : ℂ} (ha : f a ≠ 0) (z : ℂ) : analyticOrderAt f z ≠ ⊤ := by
69   intro h
70   have hall : AnalyticOnNhd ℂ f univ := fun w _ => hf w
71   have he := hall.eq_of_eventuallyEq (show AnalyticOnNhd ℂ (0 : ℂ → ℂ) univ from
72     fun _ _ => analyticAt_const) (analyticOrderAt_eq_top.mp h)
73   exact ha (congrFun he a)
74 
75 theorem canonicalSignedDenominator_order_ne_top {N : ℕ} (hN : 0 < N) (z : ℂ) :
76     analyticOrderAt (canonicalSignedDenominator N) z ≠ ⊤ :=
77   entire_analyticOrderAt_ne_top (f := canonicalSignedDenominator N) (a := 0) (fun w => analyticAt_entireSigned N 0 _ _ w)
78     (by rw [canonicalSignedDenominator_zero hN]; exact one_ne_zero) z
79 
80 theorem entireReducedDenominator_order_ne_top {N : ℕ} (hN : 0 < N) (z : ℂ) :
81     analyticOrderAt (entireReducedDenominator N) z ≠ ⊤ :=
82   entire_analyticOrderAt_ne_top (a := 0) (analyticAt_entireReducedDenominator hN)
83     (by rw [entireReducedDenominator_zero]; exact one_ne_zero) z
84 
85 theorem canonicalSignedDenominator_zeroDisk_finite {N : ℕ} (hN : 0 < N) (R : ℝ) :
86     (zeroDisk (canonicalSignedDenominator N) R).Finite := by
87   simpa only [zeroDisk, mem_closedBall, dist_zero_right] using
88     canonicalSignedDenominator_finite_zeros_on_compact hN (isCompact_closedBall (0 : ℂ) R)
89 
90 theorem entireReducedDenominator_zeroDisk_finite {N : ℕ} (hN : 0 < N) (R : ℝ) :
91     (zeroDisk (entireReducedDenominator N) R).Finite := by
92   simpa only [zeroDisk, mem_closedBall, dist_zero_right] using
93     entireReducedDenominator_finite_zeros_on_compact hN (isCompact_closedBall (0 : ℂ) R)
94 
95 end
96 end Komorebi.PaperIV

Back to source controls