ZeroZetaDecomposition.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.ZeroLatticeComparison
6 
7 namespace Komorebi.PaperIV
8 noncomputable section
9 open Set Filter
10 open scoped Topology
11 
12 theorem tsum_injection_add_complement {α β : Type*} (i : α → β)
13     (hi : Function.Injective i) {f : β → ℂ} (hf : Summable f) :
14     (∑' a, f (i a)) + (∑' b : ↥((range i)ᶜ), f b) = ∑' b, f b := by
15   rw [← tsum_range f hi]
16   exact (hf.subtype (range i)).tsum_add_tsum_compl (hf.subtype (range i)ᶜ)
17 
18 theorem finite_subtype_tsum_entire {α : Type*} {S : Set α} (hS : S.Finite)
19     (f : α → ℂ → ℂ) (hf : ∀ a, Differentiable ℂ (f a)) :
20     Differentiable ℂ (fun s => ∑' a : S, f a s) := by
21   classical
22   let := hS.fintype
23   simp only [tsum_fintype]
24   exact Differentiable.fun_sum (fun a _ => hf a)
25 
26 def SignedZeroEnumeration.reducedExceptionZeta {N : ℕ} (hn : 0 < N)
27     (e : SignedZeroEnumeration N) (s : ℂ) : ℂ :=
28   ∑' z : ↥((range (e.reducedZero hn))ᶜ), absoluteZeroZetaTerm (entireReducedDenominator N) z.val s
29 
30 def SignedZeroEnumeration.absoluteExceptionZeta {N : ℕ} (hn : 0 < N)
31     (e : SignedZeroEnumeration N) (s : ℂ) : ℂ :=
32   ∑' z : ↥((range (e.orbitZero hn))ᶜ), absoluteZeroZetaTerm (canonicalSignedDenominator N) z.val s
33 
34 theorem absoluteZeroZetaTerm_entire (f : ℂ → ℂ) (z : {z : ℂ // f z = 0}) :
35     Differentiable ℂ (absoluteZeroZetaTerm f z) := by
36   unfold absoluteZeroZetaTerm
37   exact weightedDirichletTerm_differentiable _ _ z
38 
39 theorem SignedZeroEnumeration.reducedExceptionZeta_entire {N : ℕ} (hn : 0 < N)
40     (e : SignedZeroEnumeration N) : Differentiable ℂ (e.reducedExceptionZeta hn) :=
41   finite_subtype_tsum_entire (e.reducedZero_finite_complement hn) _
42     (absoluteZeroZetaTerm_entire _)
43 
44 theorem SignedZeroEnumeration.absoluteExceptionZeta_entire {N : ℕ} (hn : 0 < N)
45     (e : SignedZeroEnumeration N) : Differentiable ℂ (e.absoluteExceptionZeta hn) :=
46   finite_subtype_tsum_entire (e.orbitZero_finite_complement hn) _
47     (absoluteZeroZetaTerm_entire _)
48 
49 theorem SignedZeroEnumeration.reducedZetaTerm {N : ℕ} (hn : 0 < N)
50     (e : SignedZeroEnumeration N) (m : ℕ) (s : ℂ) :
51     absoluteZeroZetaTerm (entireReducedDenominator N) (e.reducedZero hn m) s =
52       positiveZetaTerm (e.root m) ((N : ℂ) * s) := by
53   simp only [absoluteZeroZetaTerm, weightedDirichletTerm, SignedZeroEnumeration.reducedZero,
54     (e.reducedRoot_zero_simple hn m).2, Nat.cast_one, one_mul, e.reducedRoot_norm,
55     Real.log_pow, positiveZetaTerm]
56   push_cast
57   congr 1
58   ring
59 
60 theorem SignedZeroEnumeration.orbitZetaTerm {N : ℕ} (hn : 0 < N)
61     (e : SignedZeroEnumeration N) (p : Fin N × ℕ) (s : ℂ) :
62     absoluteZeroZetaTerm (canonicalSignedDenominator N) (e.orbitZero hn p) s =
63       positiveZetaTerm (e.root p.2) s := by
64   simp only [absoluteZeroZetaTerm, weightedDirichletTerm, SignedZeroEnumeration.orbitZero,
65     (e.orbit_zero_simple hn p).2, Nat.cast_one, one_mul, e.orbit_norm hn, positiveZetaTerm]
66 
67 theorem SignedZeroEnumeration.reducedZeta_decomposition {N : ℕ} (hN : 2 ≤ N)
68     (e : SignedZeroEnumeration N) {s : ℂ} (hs : 1 / (N : ℝ) < s.re) :
69     absoluteZeroZeta (entireReducedDenominator N) s =
70       (∑' m, positiveZetaTerm (e.root m) ((N : ℂ) * s)) +
71         e.reducedExceptionZeta (by omega) s := by
72   have hsum := ((entireReducedDenominator_zeta_absolute_convergence hN s).mpr hs).of_norm
73   have h := tsum_injection_add_complement (e.reducedZero (by omega))
74     (e.reducedZero_injective (by omega)) hsum
75   simpa only [e.reducedZetaTerm, absoluteZeroZeta, SignedZeroEnumeration.reducedExceptionZeta] using h.symm
76 
77 theorem SignedZeroEnumeration.absoluteZeta_decomposition {N : ℕ} (hN : 2 ≤ N)
78     (e : SignedZeroEnumeration N) {s : ℂ} (hs : 1 < s.re) :
79     absoluteZeroZeta (canonicalSignedDenominator N) s =
80       (N : ℂ) * (∑' m, positiveZetaTerm (e.root m) s) +
81         e.absoluteExceptionZeta (by omega) s := by
82   have hsum := ((canonicalSignedDenominator_zeta_absolute_convergence hN s).mpr hs).of_norm
83   have h := tsum_injection_add_complement (e.orbitZero (by omega))
84     (e.orbitZero_injective (by omega)) hsum
85   have hp := hsum.comp_injective (e.orbitZero_injective (by omega))
86   have hprod := hp.tsum_prod
87   simp only [Function.comp_apply] at hprod
88   erw [hprod] at h
89   simpa only [Function.comp_apply, e.orbitZetaTerm, tsum_fintype, Finset.sum_const,
90     Finset.card_univ, Fintype.card_fin, nsmul_eq_mul, absoluteZeroZeta,
91     SignedZeroEnumeration.absoluteExceptionZeta] using h.symm
92 
93 end
94 end Komorebi.PaperIV

Back to source controls