CompleteHomogeneous.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.ThetaZeroBell
6 
7 namespace Komorebi.PaperIV
8 noncomputable section
9 open scoped Classical
10 
11 def powerSumLog (q : ℕ → ℂ) : PowerSeries ℂ :=
12   PowerSeries.mk (fun n => if n = 0 then 0 else q n / (n : ℂ))
13 
14 @[simp] theorem powerSumLog_constantCoeff (q : ℕ → ℂ) : (powerSumLog q).constantCoeff = 0 := by
15   simp [powerSumLog]
16 
17 @[simp] theorem powerSumLog_derivative_coeff (q : ℕ → ℂ) (n : ℕ) :
18     PowerSeries.coeff n (PowerSeries.derivative ℂ (powerSumLog q)) = q (n + 1) := by
19   simp only [powerSumLog, PowerSeries.coeff_derivative, PowerSeries.coeff_mk, Nat.succ_ne_zero, ↓reduceIte, Nat.cast_add, Nat.cast_one]
20   exact div_mul_cancel₀ _ (by exact_mod_cast Nat.succ_ne_zero n)
21 
22 def homogeneousSeries (q : ℕ → ℂ) : PowerSeries ℂ := formalExpFamily (powerSumLog q) 1
23 
24 def homogeneousCoeff (q : ℕ → ℂ) (n : ℕ) : ℂ := PowerSeries.coeff n (homogeneousSeries q)
25 
26 @[simp] theorem homogeneousSeries_constantCoeff (q : ℕ → ℂ) : (homogeneousSeries q).constantCoeff = 1 := by
27   exact constantCoeff_formalExpFamily_of_zero (powerSumLog_constantCoeff q) 1
28 
29 theorem homogeneousSeries_derivative (q : ℕ → ℂ) :
30     PowerSeries.derivative ℂ (homogeneousSeries q) =
31       homogeneousSeries q * PowerSeries.derivative ℂ (powerSumLog q) := by
32   simpa [homogeneousSeries] using derivative_formalExpFamily (powerSumLog_constantCoeff q) (1 : ℂ)
33 
34 theorem homogeneousCoeff_recurrence (q : ℕ → ℂ) (n : ℕ) :
35     (n + 1 : ℂ) * homogeneousCoeff q (n + 1) =
36       ∑ k ∈ Finset.range (n + 1), homogeneousCoeff q k * q (n - k + 1) := by
37   have h := congrArg (PowerSeries.coeff n) (homogeneousSeries_derivative q)
38   rw [PowerSeries.coeff_derivative, PowerSeries.coeff_mul,
39     Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk] at h
40   simpa [homogeneousCoeff, mul_comm] using h
41 
42 def homogeneousGeometric (a : ℂ) : PowerSeries ℂ := PowerSeries.mk (fun n => a ^ n)
43 
44 @[simp] theorem homogeneousGeometric_coeff (a : ℂ) (n : ℕ) :
45     PowerSeries.coeff n (homogeneousGeometric a) = a ^ n := by simp [homogeneousGeometric]
46 
47 @[simp] theorem homogeneousGeometric_constantCoeff (a : ℂ) :
48     (homogeneousGeometric a).constantCoeff = 1 := by simp [homogeneousGeometric]
49 
50 theorem homogeneousGeometric_inverse (a : ℂ) :
51     homogeneousGeometric a * (1 - PowerSeries.C a * PowerSeries.X) = 1 := by
52   have h := congrArg (PowerSeries.rescale a) (PowerSeries.mk_one_mul_one_sub_eq_one ℂ)
53   simpa [PowerSeries.rescale_mk, homogeneousGeometric] using h
54 
55 theorem homogeneousGeometric_derivative (a : ℂ) :
56     PowerSeries.derivative ℂ (homogeneousGeometric a) =
57       homogeneousGeometric a * (PowerSeries.C a * homogeneousGeometric a) := by
58   have h := congrArg (PowerSeries.derivative ℂ) (homogeneousGeometric_inverse a)
59   simp [Derivation.leibniz, smul_eq_mul] at h
60   have he : PowerSeries.derivative ℂ (homogeneousGeometric a) *
61       (1 - PowerSeries.C a * PowerSeries.X) = homogeneousGeometric a * PowerSeries.C a := by
62     linear_combination h
63   calc
64     _ = PowerSeries.derivative ℂ (homogeneousGeometric a) *
65         ((1 - PowerSeries.C a * PowerSeries.X) * homogeneousGeometric a) := by
66       rw [mul_comm (1 - PowerSeries.C a * PowerSeries.X), homogeneousGeometric_inverse, mul_one]
67     _ = (PowerSeries.derivative ℂ (homogeneousGeometric a) *
68         (1 - PowerSeries.C a * PowerSeries.X)) * homogeneousGeometric a := by ring
69     _ = (homogeneousGeometric a * PowerSeries.C a) * homogeneousGeometric a := by rw [he]
70     _ = _ := by ring
71 
72 def finiteHomogeneousSeries {ι : Type*} (a : ι → ℂ) (S : Finset ι) : PowerSeries ℂ :=
73   ∏ i ∈ S, homogeneousGeometric (a i)
74 
75 @[simp] theorem finiteHomogeneousSeries_constantCoeff {ι : Type*} (a : ι → ℂ) (S : Finset ι) :
76     (finiteHomogeneousSeries a S).constantCoeff = 1 := by simp [finiteHomogeneousSeries]
77 
78 theorem finiteHomogeneousSeries_derivative {ι : Type*} (a : ι → ℂ) (S : Finset ι) :
79     PowerSeries.derivative ℂ (finiteHomogeneousSeries a S) =
80       finiteHomogeneousSeries a S * ∑ i ∈ S, PowerSeries.C (a i) * homogeneousGeometric (a i) := by
81   induction S using Finset.induction_on with
82   | empty => simp [finiteHomogeneousSeries]
83   | @insert i S hi ih =>
84       simp only [finiteHomogeneousSeries, Finset.prod_insert hi] at ih ⊢
85       rw [Derivation.leibniz, homogeneousGeometric_derivative, ih, Finset.sum_insert hi]
86       ring
87 
88 theorem finiteHomogeneousSeries_eq_homogeneous {ι : Type*} (a : ι → ℂ) (S : Finset ι) :
89     finiteHomogeneousSeries a S = homogeneousSeries (fun m => ∑ i ∈ S, a i ^ m) := by
90   have he : (∑ i ∈ S, PowerSeries.C (a i) * homogeneousGeometric (a i)) =
91       PowerSeries.derivative ℂ (powerSumLog (fun m => ∑ i ∈ S, a i ^ m)) := by
92     ext n
93     simp [pow_succ, mul_comm]
94   apply powerSeries_linear_ode_unique (H := PowerSeries.derivative ℂ (powerSumLog (fun m => ∑ i ∈ S, a i ^ m)))
95   · simp
96   · rw [finiteHomogeneousSeries_derivative, he]
97   · exact homogeneousSeries_derivative _
98 
99 /-- The finite coefficients are precisely the complete homogeneous monomial sums. -/
100 theorem finiteHomogeneousSeries_monomials {ι : Type*} (a : ι → ℂ) (S : Finset ι) (n : ℕ) :
101     PowerSeries.coeff n (finiteHomogeneousSeries a S) =
102       ∑ l ∈ S.finsuppAntidiag n, ∏ i ∈ S, a i ^ (l i) := by
103   simp [finiteHomogeneousSeries, PowerSeries.coeff_prod]
104 
105 end
106 end Komorebi.PaperIV

Back to source controls