NormalizedEntire.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.SharpGrowth
6 import KomorebiPaperIV.AlgebraicCompletion
7 
8 namespace Komorebi.PaperIV
9 noncomputable section
10 open FormalMultilinearSeries Set Filter Metric
11 open scoped Topology
12 
13 def entireNormalizedSection (N j : ℕ) : ℂ → ℂ :=
14   ofScalarsSum (fun n => PowerSeries.coeff n (normalizedResidueSection (K := ℂ) N j))
15 
16 theorem normalizedSection_coeff_norm (N j n : ℕ) :
17     ‖PowerSeries.coeff n (normalizedResidueSection (K := ℂ) N j)‖ =
18       (j.factorial : ℝ) / ((N * n + j).factorial : ℝ) := by
19   rw [coeff_normalizedResidueSection, norm_div]
20   simp
21 
22 theorem normalizedSection_entire_radius {N : ℕ} (hN : 0 < N) (j : ℕ) :
23     (ofScalars ℂ (fun n => PowerSeries.coeff n (normalizedResidueSection (K := ℂ) N j))).radius = ⊤ := by
24   apply radius_eq_top_of_summable_norm
25   intro r
26   apply Summable.of_nonneg_of_le (fun n => mul_nonneg (norm_nonneg _) (pow_nonneg r.2 _))
27     (fun n => ?_) ((Real.summable_pow_div_factorial (r : ℝ)).mul_left (j.factorial : ℝ))
28   rw [ofScalars_norm, normalizedSection_coeff_norm]
29   calc
30     _ = (j.factorial : ℝ) * ((r : ℝ) ^ n / ((N * n + j).factorial : ℝ)) := by
31       change ((j.factorial : ℝ) / ((N * n + j).factorial : ℝ)) * (r : ℝ) ^ n = _
32       ring
33     _ ≤ (j.factorial : ℝ) * ((r : ℝ) ^ n / (n.factorial : ℝ)) := by
34       apply mul_le_mul_of_nonneg_left _ (by positivity)
35       apply div_le_div_of_nonneg_left (pow_nonneg r.2 n) (by positivity)
36       exact_mod_cast Nat.factorial_le ((Nat.le_mul_of_pos_left n hN).trans (Nat.le_add_right _ j))
37 
38 theorem analyticAt_entireNormalizedSection {N : ℕ} (hN : 0 < N) (j : ℕ) (w : ℂ) :
39     AnalyticAt ℂ (entireNormalizedSection N j) w := by
40   apply (ofScalars ℂ (fun n => PowerSeries.coeff n (normalizedResidueSection (K := ℂ) N j))).analyticOnNhd
41   rw [normalizedSection_entire_radius hN]; simp
42 
43 theorem hasSum_entireNormalizedSection {N : ℕ} (hN : 0 < N) (j : ℕ) (w : ℂ) :
44     HasSum (fun n => (j.factorial : ℂ) / ((N * n + j).factorial : ℂ) * w ^ n)
45       (entireNormalizedSection N j w) := by
46   have h := (ofScalars ℂ (fun n => PowerSeries.coeff n (normalizedResidueSection (K := ℂ) N j))).hasSum
47     (x := w) (by rw [normalizedSection_entire_radius hN]; simp)
48   simpa only [entireNormalizedSection, ofScalarsSum, ofScalars_apply_eq', smul_eq_mul,
49     coeff_normalizedResidueSection] using h
50 
51 @[simp] theorem entireNormalizedSection_zero (N j : ℕ) : entireNormalizedSection N j 0 = 1 := by
52   simp [entireNormalizedSection, Nat.factorial_ne_zero]
53 
54 theorem entireNormalizedSection_iteratedDeriv_zero {N : ℕ} (hN : 0 < N) (j n : ℕ) :
55     iteratedDeriv n (entireNormalizedSection N j) 0 =
56       (n.factorial : ℂ) * (j.factorial : ℂ) / ((N * n + j).factorial : ℂ) := by
57   let p := ofScalars ℂ (fun n => PowerSeries.coeff n (normalizedResidueSection (K := ℂ) N j))
58   have hp : HasFPowerSeriesAt (entireNormalizedSection N j) p 0 :=
59     (p.hasFPowerSeriesOnBall (by dsimp [p]; rw [normalizedSection_entire_radius hN]; simp)).hasFPowerSeriesAt
60   have he := hp.eq_formalMultilinearSeries (analyticAt_entireNormalizedSection hN j 0).hasFPowerSeriesAt
61   have hc := congrArg (fun q : FormalMultilinearSeries ℂ ℂ ℂ => q.coeff n) he
62   simp only [p, coeff_ofScalars] at hc
63   have hn : (n.factorial : ℂ) ≠ 0 := by exact_mod_cast n.factorial_ne_zero
64   have hh := ((div_eq_iff hn).mp hc.symm).trans (mul_comm _ _)
65   simpa only [coeff_normalizedResidueSection, mul_div_assoc] using hh
66 
67 theorem entireNormalizedSection_transfer {N j : ℕ} (hN : 0 < N) (hj : j < N)
68     {ω : ℂ} (hω : IsPrimitiveRoot ω N) (z : ℂ) :
69     entireNormalizedSection N j (z ^ N) * z ^ j =
70       (j.factorial : ℂ) * entireTransfer N j ω 1 z := by
71   have hi : Function.Injective (fun n : ℕ => N * n + j) := by
72     intro a b h; exact Nat.mul_left_cancel hN (Nat.add_right_cancel h)
73   have hz : ∀ n ∉ Set.range (fun m : ℕ => N * m + j),
74       PowerSeries.coeff n (transferSection N j (1 : ℂ)) * z ^ n = 0 := by
75     intro n hn
76     have hres : n % N ≠ j := by
77       intro he
78       apply hn
79       refine ⟨n / N, ?_⟩
80       change N * (n / N) + j = n
81       rw [← he, Nat.div_add_mod]
82     simp [coeff_transferSection, transferSectionCoeff, hres]
83   have ht := (hi.hasSum_iff hz).mpr (hasSum_entireTransfer hN hj hω (1 : ℂ) z)
84   apply ((hasSum_entireNormalizedSection hN j (z ^ N)).mul_right (z ^ j)).unique
85   convert ht.mul_left (j.factorial : ℂ) using 1
86   funext n
87   simp only [Function.comp_apply, coeff_transferSection, transferSectionCoeff, Nat.add_mod,
88     Nat.mul_mod_right, zero_add, Nat.mod_eq_of_lt hj, ↓reduceIte, one_pow, one_mul]
89   simp only [map_div₀, map_one, map_natCast]
90   rw [← pow_mul, pow_add]
91   ring
92 
93 theorem entireTransfer_unit_norm_le {N : ℕ} (hN : 0 < N) (j : ℕ)
94     {ω : ℂ} (hω : IsPrimitiveRoot ω N) (z : ℂ) :
95     ‖entireTransfer N j ω 1 z‖ ≤ Real.exp ‖z‖ := by
96   have hn : ‖ω‖ = 1 := Complex.norm_eq_one_of_pow_eq_one hω.pow_eq_one hN.ne'
97   have ht (k : ℕ) : ‖((ω ^ j)⁻¹) ^ k * Complex.exp ((1 * ω ^ k) * z)‖ ≤ Real.exp ‖z‖ := by
98     simp only [norm_mul, norm_pow, norm_inv, hn, one_pow, inv_one, one_mul]
99     rw [Complex.norm_exp]
100     apply Real.exp_le_exp.mpr
101     calc
102       _ ≤ ‖ω ^ k * z‖ := Complex.re_le_norm _
103       _ = ‖z‖ := by simp [norm_pow, hn]
104   rw [entireTransfer, norm_mul, norm_inv, Complex.norm_natCast]
105   calc
106     _ ≤ (N : ℝ)⁻¹ * ∑ k ∈ Finset.range N, ‖((ω ^ j)⁻¹) ^ k * Complex.exp ((1 * ω ^ k) * z)‖ :=
107       mul_le_mul_of_nonneg_left (norm_sum_le _ _) (by positivity)
108     _ ≤ (N : ℝ)⁻¹ * ∑ _k ∈ Finset.range N, Real.exp ‖z‖ :=
109       mul_le_mul_of_nonneg_left (Finset.sum_le_sum (fun k _ => ht k)) (by positivity)
110     _ = Real.exp ‖z‖ := by simp [hN.ne']
111 
112 end
113 end Komorebi.PaperIV

Back to source controls