PrincipalPartCoefficients.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import Mathlib.RingTheory.PowerSeries.WellKnown
6 import Mathlib.Basic.Complex.Basic
7 import Mathlib.Data.Nat.Choose.Bounds
8 
9 namespace Komorebi.PaperIV
10 noncomputable section
11 
12 /-- Formal expansion of the normalized pole `(1-z/rho)^(-ell)`. -/
13 def principalPartSeries (ρ : ℂ) (ℓ : ℕ) : PowerSeries ℂ :=
14   PowerSeries.rescale ρ⁻¹ (PowerSeries.invOneSubPow ℂ ℓ).val
15 
16 theorem principalPartSeries_coefficient (ρ : ℂ) {ℓ : ℕ} (hℓ : 0 < ℓ) (m : ℕ) :
17     PowerSeries.coeff m (principalPartSeries ρ ℓ) =
18       ((m + ℓ - 1).choose (ℓ - 1) : ℂ) * ρ⁻¹ ^ m := by
19   rw [principalPartSeries, PowerSeries.coeff_rescale,
20     PowerSeries.invOneSubPow_val_eq_mk_sub_one_add_choose_of_pos ℂ ℓ hℓ,
21     PowerSeries.coeff_mk]
22   rw [show ℓ - 1 + m = m + ℓ - 1 by omega]
23   ring
24 
25 theorem principalPartSeries_inverse (ρ : ℂ) (ℓ : ℕ) :
26     principalPartSeries ρ ℓ * (1 - PowerSeries.C ρ⁻¹ * PowerSeries.X) ^ ℓ = 1 := by
27   have h0 := (PowerSeries.invOneSubPow ℂ ℓ).val_inv
28   rw [PowerSeries.invOneSubPow_inv_eq_one_sub_pow] at h0
29   have h := congrArg (PowerSeries.rescale ρ⁻¹) h0
30   simpa only [principalPartSeries, map_mul, map_pow, map_sub, map_one, PowerSeries.rescale_X] using h
31 
32 /-- Uniform polynomial bound for all lower principal-part orders. -/
33 theorem lower_principal_part_choose_bound {m ℓ r : ℕ}
34     (hm : 1 ≤ m) (hℓ : 1 ≤ ℓ) (hℓr : ℓ < r) :
35     (m + ℓ - 1).choose (ℓ - 1) ≤ ℓ ^ (ℓ - 1) * m ^ (r - 2) := by
36   calc
37     _ ≤ (m + ℓ - 1) ^ (ℓ - 1) := Nat.choose_le_pow _ _
38     _ ≤ (ℓ * m) ^ (ℓ - 1) := Nat.pow_le_pow_left (by
39       have h := Nat.mul_le_mul_left (ℓ - 1) hm
40       have hl : ℓ - 1 + 1 = ℓ := by omega
41       have he : (ℓ - 1) * m + m = ℓ * m := by
42         simpa only [Nat.add_mul, one_mul] using congrArg (fun x => x * m) hl
43       omega) _
44     _ = ℓ ^ (ℓ - 1) * m ^ (ℓ - 1) := Nat.mul_pow _ _ _
45     _ ≤ ℓ ^ (ℓ - 1) * m ^ (r - 2) := Nat.mul_le_mul_left _ (Nat.pow_le_pow_right hm (by omega))
46 
47 end
48 end Komorebi.PaperIV

Back to source controls