BranchedDirichlet.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.ZeroZetaConvergence
6 
7 namespace Komorebi.PaperIV
8 noncomputable section
9 open Set Filter Metric
10 open scoped Topology
11 
12 def branchedDirichletTerm {ι : Type*} (c L : ι → ℂ) (i : ι) (s : ℂ) : ℂ :=
13   c i * Complex.exp (-s * L i)
14 
15 theorem branchedDirichletTerm_differentiable {ι : Type*} (c L : ι → ℂ) (i : ι) :
16     Differentiable ℂ (branchedDirichletTerm c L i) := by
17   unfold branchedDirichletTerm
18   fun_prop
19 
20 theorem branchedDirichletTerm_norm {ι : Type*} (c L : ι → ℂ) (r : ι → ℝ)
21     (hr : ∀ i, 0 < r i) (hL : ∀ i, (L i).re = Real.log (r i)) (i : ι) (s : ℂ) :
22     ‖branchedDirichletTerm c L i s‖ =
23       ‖c i‖ / r i ^ s.re * Real.exp (s.im * (L i).im) := by
24   rw [branchedDirichletTerm, norm_mul, Complex.norm_exp]
25   simp only [Complex.mul_re, Complex.neg_re, Complex.neg_im, hL]
26   rw [neg_mul s.im, sub_neg_eq_add, Real.exp_add, Real.rpow_def_of_pos (hr i),
27     div_eq_mul_inv, ← Real.exp_neg]
28   ring_nf
29 
30 theorem branchedDirichletTerm_strip_bound {ι : Type*} (c L : ι → ℂ) (r : ι → ℝ)
31     (hr : ∀ i, 0 < r i) (hL : ∀ i, (L i).re = Real.log (r i))
32     {B K a b : ℝ} (_hB : 0 ≤ B) (hK : 0 ≤ K) (harg : ∀ i, |(L i).im| ≤ B)
33     {s : ℂ} (ha : a ≤ s.re) (hb : s.re ≤ b) (hi : |s.im| ≤ K) (i : ι) :
34     ‖branchedDirichletTerm c L i s‖ ≤
35       Real.exp (K * B) * (‖c i‖ / r i ^ a + ‖c i‖ / r i ^ b) := by
36   rw [branchedDirichletTerm_norm c L r hr hL]
37   have hs : ‖c i‖ / r i ^ s.re ≤ ‖c i‖ / r i ^ a + ‖c i‖ / r i ^ b := by
38     have h := weightedDirichletTerm_strip_bound (fun _ : ι => 1) r hr ha hb i
39     rw [weightedDirichletTerm_norm _ _ hr] at h
40     norm_num only [Nat.cast_one] at h
41     have h' := mul_le_mul_of_nonneg_left h (norm_nonneg (c i))
42     simpa only [mul_add, mul_one_div] using h'
43   have he : Real.exp (s.im * (L i).im) ≤ Real.exp (K * B) := by
44     apply Real.exp_le_exp.mpr
45     calc _ ≤ |s.im * (L i).im| := le_abs_self _
46          _ = |s.im| * |(L i).im| := abs_mul _ _
47          _ ≤ K * B := mul_le_mul hi (harg i) (abs_nonneg _) hK
48   calc
49     _ ≤ (‖c i‖ / r i ^ a + ‖c i‖ / r i ^ b) * Real.exp (K * B) :=
50       mul_le_mul hs he (Real.exp_nonneg _) (add_nonneg (div_nonneg (norm_nonneg _) (Real.rpow_nonneg (hr i).le _))
51         (div_nonneg (norm_nonneg _) (Real.rpow_nonneg (hr i).le _)))
52     _ = _ := mul_comm _ _
53 
54 /-- Absolute convergence at an individual complex parameter. -/
55 theorem branchedDirichlet_summable_norm {ι : Type*} (c L : ι → ℂ) (r : ι → ℝ)
56     (hr : ∀ i, 0 < r i) (hL : ∀ i, (L i).re = Real.log (r i))
57     {B : ℝ} (hB : 0 ≤ B) (harg : ∀ i, |(L i).im| ≤ B) (s : ℂ)
58     (hs : Summable (fun i => ‖c i‖ / r i ^ s.re)) :
59     Summable (fun i => ‖branchedDirichletTerm c L i s‖) := by
60   apply ((hs.add hs).mul_left (Real.exp (|s.im| * B))).of_norm_bounded
61   intro i
62   rw [norm_norm]
63   exact branchedDirichletTerm_strip_bound c L r hr hL hB (abs_nonneg _) harg le_rfl le_rfl le_rfl i
64 
65 /-- A local Weierstrass theorem for bounded choices of logarithmic arguments.
66 It retains all finite exceptional terms and does not require a global branch. -/
67 theorem branchedDirichlet_locally_uniform {ι : Type*} (c L : ι → ℂ) (r : ι → ℝ)
68     (hr : ∀ i, 0 < r i) (hL : ∀ i, (L i).re = Real.log (r i))
69     {B : ℝ} (hB : 0 ≤ B) (harg : ∀ i, |(L i).im| ≤ B) (U : Set ℂ)
70     (hs : ∀ s ∈ U, ∃ a b : ℝ, a < s.re ∧ s.re < b ∧
71       Summable (fun i => ‖c i‖ / r i ^ a) ∧ Summable (fun i => ‖c i‖ / r i ^ b)) :
72     HasSumLocallyUniformlyOn (branchedDirichletTerm c L)
73       (fun s => ∑' i, branchedDirichletTerm c L i s) U := by
74   apply hasSumLocallyUniformlyOn_of_of_forall_exists_nhds
75   intro s hsU
76   obtain ⟨a, b, ha, hb, hsa, hsb⟩ := hs s hsU
77   let V := {z : ℂ | a < z.re ∧ z.re < b ∧ |z.im| < |s.im| + 1}
78   have hV : IsOpen V := (isOpen_lt continuous_const Complex.continuous_re).inter
79     ((isOpen_lt Complex.continuous_re continuous_const).inter
80       (isOpen_lt Complex.continuous_im.abs continuous_const))
81   have hsV : s ∈ V := ⟨ha, hb, by linarith⟩
82   refine ⟨V, mem_nhdsWithin_of_mem_nhds (hV.mem_nhds hsV), ?_⟩
83   apply hasSumUniformlyOn_iff_tendstoUniformlyOn.mpr
84   apply tendstoUniformlyOn_tsum ((hsa.add hsb).mul_left (Real.exp ((|s.im| + 1) * B)))
85   intro i z hz
86   exact branchedDirichletTerm_strip_bound c L r hr hL hB (by positivity) harg hz.1.le hz.2.1.le hz.2.2.le i
87 
88 theorem branchedDirichlet_entire {ι : Type*} (c L : ι → ℂ) (r : ι → ℝ)
89     (hr : ∀ i, 0 < r i) (hL : ∀ i, (L i).re = Real.log (r i))
90     {B : ℝ} (hB : 0 ≤ B) (harg : ∀ i, |(L i).im| ≤ B)
91     (hs : ∀ t : ℝ, Summable (fun i => ‖c i‖ / r i ^ t)) :
92     HasSumLocallyUniformlyOn (branchedDirichletTerm c L)
93       (fun s => ∑' i, branchedDirichletTerm c L i s) univ ∧
94     Differentiable ℂ (fun s => ∑' i, branchedDirichletTerm c L i s) := by
95   have h := branchedDirichlet_locally_uniform c L r hr hL hB harg univ
96     (fun s _ => ⟨s.re - 1, s.re + 1, by linarith, by linarith, hs _, hs _⟩)
97   refine ⟨h, differentiableOn_univ.mp ?_⟩
98   exact h.summableLocallyUniformlyOn.differentiableOn isOpen_univ
99     (fun i s _ => branchedDirichletTerm_differentiable c L i s)
100 
101 theorem branchedDirichlet_halfplane {ι : Type*} (c L : ι → ℂ) (r : ι → ℝ)
102     (hr : ∀ i, 0 < r i) (hL : ∀ i, (L i).re = Real.log (r i))
103     {B : ℝ} (hB : 0 ≤ B) (harg : ∀ i, |(L i).im| ≤ B) (σ : ℝ)
104     (hs : ∀ t : ℝ, σ < t → Summable (fun i => ‖c i‖ / r i ^ t)) :
105     HasSumLocallyUniformlyOn (branchedDirichletTerm c L)
106       (fun s => ∑' i, branchedDirichletTerm c L i s) {s : ℂ | σ < s.re} ∧
107     DifferentiableOn ℂ (fun s => ∑' i, branchedDirichletTerm c L i s) {s : ℂ | σ < s.re} := by
108   have h := branchedDirichlet_locally_uniform c L r hr hL hB harg {s : ℂ | σ < s.re}
109     (fun s hs0 => ⟨(σ + s.re) / 2, s.re + 1, by dsimp at hs0; linarith,
110       by linarith, hs _ (by dsimp at hs0; linarith), hs _ (by dsimp at hs0; linarith)⟩)
111   exact ⟨h, h.summableLocallyUniformlyOn.differentiableOn
112     (isOpen_lt continuous_const Complex.continuous_re)
113     (fun i s _ => branchedDirichletTerm_differentiable c L i s)⟩
114 
115 end
116 end Komorebi.PaperIV

Back to source controls