ReducedEntire.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.SignedFiniteExceptions
6 import KomorebiPaperIV.ReciprocalCore
7 import Mathlib.Analysis.Analytic.OfScalars
8 
9 namespace Komorebi.PaperIV
10 noncomputable section
11 open FormalMultilinearSeries
12 
13 /-- The manuscript's reduced denominator as an actual complex power series. -/
14 def entireReducedDenominator (N : ℕ) : ℂ → ℂ :=
15   ofScalarsSum (fun n => PowerSeries.coeff n (reducedDenominator (R := ℂ) N))
16 
17 theorem reducedDenominator_coeff_complex (N n : ℕ) :
18     PowerSeries.coeff n (reducedDenominator (R := ℂ) N) =
19       (-1 : ℂ) ^ n / ((N * n).factorial : ℂ) := by
20   simp [coeff_reducedDenominator]
21 
22 theorem reducedDenominator_coeff_norm (N n : ℕ) :
23     ‖PowerSeries.coeff n (reducedDenominator (R := ℂ) N)‖ =
24       1 / ((N * n).factorial : ℝ) := by
25   rw [reducedDenominator_coeff_complex, norm_div, norm_pow]
26   simp
27 
28 theorem reducedDenominator_entire_radius {N : ℕ} (hN : 0 < N) :
29     (ofScalars ℂ (fun n => PowerSeries.coeff n (reducedDenominator (R := ℂ) N))).radius = ⊤ := by
30   apply radius_eq_top_of_summable_norm
31   intro r
32   apply Summable.of_nonneg_of_le (fun n => mul_nonneg (norm_nonneg _) (pow_nonneg r.2 _))
33     (fun n => ?_) (Real.summable_pow_div_factorial (r : ℝ))
34   rw [ofScalars_norm, reducedDenominator_coeff_norm, one_div_mul_eq_div]
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)
37 
38 theorem analyticAt_entireReducedDenominator {N : ℕ} (hN : 0 < N) (w : ℂ) :
39     AnalyticAt ℂ (entireReducedDenominator N) w := by
40   apply (ofScalars ℂ (fun n => PowerSeries.coeff n (reducedDenominator (R := ℂ) N))).analyticOnNhd
41   rw [reducedDenominator_entire_radius hN]; simp
42 
43 theorem hasSum_entireReducedDenominator {N : ℕ} (hN : 0 < N) (w : ℂ) :
44     HasSum (fun n => PowerSeries.coeff n (reducedDenominator (R := ℂ) N) * w ^ n)
45       (entireReducedDenominator N w) := by
46   have h := (ofScalars ℂ (fun n => PowerSeries.coeff n (reducedDenominator (R := ℂ) N))).hasSum
47     (x := w) (by rw [reducedDenominator_entire_radius hN]; simp)
48   simpa only [entireReducedDenominator, ofScalarsSum, ofScalars_apply_eq', smul_eq_mul] using h
49 
50 @[simp] theorem entireReducedDenominator_zero (N : ℕ) : entireReducedDenominator N 0 = 1 := by
51   simp [entireReducedDenominator]
52 
53 /-- Exact analytic substitution, proved by reindexing the convergent Taylor series. -/
54 theorem canonicalSignedDenominator_eq_reduced_power {N : ℕ} (hN : 0 < N) (z : ℂ) :
55     canonicalSignedDenominator N z = entireReducedDenominator N (z ^ N) := by
56   have hd := hasSum_entireSigned hN hN (canonicalPrimitiveRoot_isPrimitive hN)
57     (canonicalSignedRoot_pow hN) z
58   have hi : Function.Injective (fun n : ℕ => N * n) := fun _ _ h => Nat.mul_left_cancel hN h
59   have hz : ∀ n ∉ Set.range (fun m : ℕ => N * m),
60       PowerSeries.coeff n (signedSection (R := ℂ) N 0) * z ^ n = 0 := by
61     intro n hn
62     have hnd : ¬ N ∣ n := by rintro ⟨m, rfl⟩; exact hn ⟨m, rfl⟩
63     rw [signedSection_zero_eq_expand_reducedDenominator hN, PowerSeries.coeff_expand]
64     simp [hnd]
65   have hh := (hi.hasSum_iff hz).mpr hd
66   apply hh.unique
67   convert hasSum_entireReducedDenominator hN (z ^ N) using 1
68   ext n
69   dsimp only [Function.comp_def]
70   rw [signedSection_zero_eq_expand_reducedDenominator hN, PowerSeries.coeff_expand_mul, pow_mul]
71 
72 /-- Away from zero the power substitution preserves analytic multiplicity. -/
73 theorem canonicalSignedDenominator_order_eq_reduced {N : ℕ} (hN : 0 < N)
74     {z : ℂ} (hz : z ≠ 0) :
75     analyticOrderAt (canonicalSignedDenominator N) z =
76       analyticOrderAt (entireReducedDenominator N) (z ^ N) := by
77   have hd : deriv (fun w : ℂ => w ^ N) z = (N : ℂ) * z ^ (N - 1) := by
78     exact (hasDerivAt_pow N z).deriv
79   have hh := analyticOrderAt_comp_of_deriv_ne_zero (f := entireReducedDenominator N)
80     (show AnalyticAt ℂ (fun w : ℂ => w ^ N) z by fun_prop)
81     (by rw [hd]; exact mul_ne_zero (Nat.cast_ne_zero.mpr hN.ne') (pow_ne_zero _ hz))
82   have he : entireReducedDenominator N ∘ (fun w : ℂ => w ^ N) = canonicalSignedDenominator N :=
83     funext fun w => (canonicalSignedDenominator_eq_reduced_power hN w).symm
84   rwa [he] at hh
85 
86 end
87 end Komorebi.PaperIV

Back to source controls