CanonicalProductQuotient.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.CanonicalProductMultiplicity
6 import Mathlib.Analysis.Meromorphic.NormalForm
7 
8 namespace Komorebi.PaperIV
9 noncomputable section
10 open Set Filter
11 
12 def canonicalProductQuotient (f : ℂ → ℂ) : ℂ → ℂ :=
13   toMeromorphicNFOn (f / fullCanonicalProduct f) univ
14 
15 theorem rawCanonicalProductQuotient_meromorphic {f : ℂ → ℂ} (hf : Differentiable ℂ f)
16     (hs : ZeroPowerSummable f 1) : MeromorphicOn (f / fullCanonicalProduct f) univ := by
17   intro z _
18   exact (hf.analyticAt z).meromorphicAt.div ((fullCanonicalProduct_entire hs).analyticAt z).meromorphicAt
19 
20 theorem rawCanonicalProductQuotient_order_zero {f : ℂ → ℂ} (hf : Differentiable ℂ f)
21     (hs : ZeroPowerSummable f 1) (hf0 : f 0 ≠ 0) (z : ℂ) :
22     meromorphicOrderAt (f / fullCanonicalProduct f) z = 0 := by
23   rw [meromorphicOrderAt_div (hf.analyticAt z).meromorphicAt
24     ((fullCanonicalProduct_entire hs).analyticAt z).meromorphicAt,
25     (hf.analyticAt z).meromorphicOrderAt_eq, ((fullCanonicalProduct_entire hs).analyticAt z).meromorphicOrderAt_eq,
26     fullCanonicalProduct_same_orders hf hs hf0,
27     ← Nat.cast_analyticOrderNatAt (entire_analyticOrderAt_ne_top (fun w => hf.analyticAt w) hf0 z),
28     ENat.map_natCast]
29   norm_cast
30   simp
31 
32 theorem canonicalProductQuotient_entire {f : ℂ → ℂ} (hf : Differentiable ℂ f)
33     (hs : ZeroPowerSummable f 1) (hf0 : f 0 ≠ 0) : Differentiable ℂ (canonicalProductQuotient f) := by
34   intro z
35   have hn := meromorphicNFOn_toMeromorphicNFOn (f / fullCanonicalProduct f) univ (mem_univ z)
36   apply (hn.meromorphicOrderAt_nonneg_iff_analyticAt.mp ?_).differentiableAt
37   rw [meromorphicOrderAt_toMeromorphicNFOn (rawCanonicalProductQuotient_meromorphic hf hs) (mem_univ z),
38     rawCanonicalProductQuotient_order_zero hf hs hf0]
39 
40 theorem canonicalProductQuotient_ne_zero {f : ℂ → ℂ} (hf : Differentiable ℂ f)
41     (hs : ZeroPowerSummable f 1) (hf0 : f 0 ≠ 0) (z : ℂ) : canonicalProductQuotient f z ≠ 0 := by
42   have hn := meromorphicNFOn_toMeromorphicNFOn (f / fullCanonicalProduct f) univ (mem_univ z)
43   apply hn.meromorphicOrderAt_eq_zero_iff.mp
44   rw [meromorphicOrderAt_toMeromorphicNFOn (rawCanonicalProductQuotient_meromorphic hf hs) (mem_univ z),
45     rawCanonicalProductQuotient_order_zero hf hs hf0]
46 
47 theorem canonicalProductQuotient_eq_div {f : ℂ → ℂ} (hf : Differentiable ℂ f)
48     (hs : ZeroPowerSummable f 1) {z : ℂ} (hz : fullCanonicalProduct f z ≠ 0) :
49     canonicalProductQuotient f z = f z / fullCanonicalProduct f z := by
50   unfold canonicalProductQuotient
51   rw [toMeromorphicNFOn_eq_toMeromorphicNFAt (rawCanonicalProductQuotient_meromorphic hf hs) (mem_univ z)]
52   rw [toMeromorphicNFAt_eq_self.mpr
53     (((hf.analyticAt z).div ((fullCanonicalProduct_entire hs).analyticAt z) hz).meromorphicNFAt)]
54   rfl
55 
56 /-- Equality up to an explicitly constructed, entire, nowhere-zero factor.
57 Constancy of this factor remains the growth-theoretic Hadamard step. -/
58 theorem fullCanonicalProduct_times_quotient {f : ℂ → ℂ} (hf : Differentiable ℂ f)
59     (hs : ZeroPowerSummable f 1) (hf0 : f 0 ≠ 0) (z : ℂ) :
60     fullCanonicalProduct f z * canonicalProductQuotient f z = f z := by
61   by_cases hz : fullCanonicalProduct f z = 0
62   · rw [hz, zero_mul, (fullCanonicalProduct_zero_iff hf hs hf0 z).mp hz]
63   · rw [canonicalProductQuotient_eq_div hf hs hz]
64     field_simp
65 
66 theorem canonicalProductQuotient_zero {f : ℂ → ℂ} (hf : Differentiable ℂ f)
67     (hs : ZeroPowerSummable f 1) : canonicalProductQuotient f 0 = f 0 := by
68   rw [canonicalProductQuotient_eq_div hf hs (by rw [fullCanonicalProduct_zero]; exact one_ne_zero),
69     fullCanonicalProduct_zero, div_one]
70 
71 theorem entireReducedDenominator_product_quotient {N : ℕ} (hN : 2 ≤ N) :
72     Differentiable ℂ (canonicalProductQuotient (entireReducedDenominator N)) ∧
73     (∀ z, canonicalProductQuotient (entireReducedDenominator N) z ≠ 0) ∧
74     canonicalProductQuotient (entireReducedDenominator N) 0 = 1 ∧
75     (∀ z, fullCanonicalProduct (entireReducedDenominator N) z *
76       canonicalProductQuotient (entireReducedDenominator N) z = entireReducedDenominator N z) := by
77   have hf : Differentiable ℂ (entireReducedDenominator N) :=
78     fun z => (analyticAt_entireReducedDenominator (by omega) z).differentiableAt
79   have hs := entireReducedDenominator_reciprocal_zeros_summable hN
80   have h0 : entireReducedDenominator N 0 ≠ 0 := by rw [entireReducedDenominator_zero]; exact one_ne_zero
81   refine ⟨canonicalProductQuotient_entire hf hs h0, canonicalProductQuotient_ne_zero hf hs h0, ?_,
82     fullCanonicalProduct_times_quotient hf hs h0⟩
83   rw [canonicalProductQuotient_zero hf hs, entireReducedDenominator_zero]
84 
85 end
86 end Komorebi.PaperIV

Back to source controls