NilpotentSeries.lean

1 import Mathlib.RingTheory.PowerSeries.Log
2 import Mathlib.RingTheory.Nilpotent.Exp
3 
4 set_option autoImplicit false
5 
6 namespace PaperX.NilpotentSeries
7 
8 open scoped BigOperators
9 
10 variable {A : Type*} [CommRing A]
11 
12 theorem hasSubst_C {a : A} (ha : IsNilpotent a) :
13     PowerSeries.HasSubst (PowerSeries.C a) := by
14   change IsNilpotent (PowerSeries.constantCoeff (PowerSeries.C a))
15   simpa using ha
16 
17 /-- Evaluation of a formal series at a nilpotent element, using algebraic substitution. -/
18 noncomputable def eval (a : A) (f : PowerSeries A) : A :=
19   PowerSeries.constantCoeff (f.subst (PowerSeries.C a))
20 
21 theorem eval_eq_finsum {a : A} (ha : IsNilpotent a) (f : PowerSeries A) :
22     eval a f = ∑ᶠ n, PowerSeries.coeff n f * a ^ n := by
23   unfold eval
24   rw [PowerSeries.constantCoeff_eq, PowerSeries.constantCoeff_subst (hasSubst_C ha)]
25   simp only [map_pow, ← PowerSeries.constantCoeff_eq, PowerSeries.constantCoeff_C, smul_eq_mul]
26 
27 theorem eval_eq_sum {a : A} {k : ℕ} (hk : a ^ k = 0) (f : PowerSeries A) :
28     eval a f = ∑ n ∈ Finset.range k, PowerSeries.coeff n f * a ^ n := by
29   rw [eval_eq_finsum ⟨k, hk⟩]
30   apply finsum_eq_sum_of_support_subset
31   intro n hn
32   by_contra hnk
33   have hkn : k ≤ n := Nat.le_of_not_gt (by simpa using hnk)
34   exact hn (by simp [pow_eq_zero_of_le hkn hk])
35 
36 theorem subst_C_eq_C_eval {a : A} (ha : IsNilpotent a) (f : PowerSeries A) :
37     f.subst (PowerSeries.C a) = PowerSeries.C (eval a f) := by
38   apply PowerSeries.ext
39   intro n
40   by_cases hn : n = 0
41   · subst n
42     simp [eval]
43   · rw [PowerSeries.coeff_subst' (hasSubst_C ha)]
44     simp [← map_pow, PowerSeries.coeff_C, hn]
45 
46 variable [Algebra ℚ A]
47 
48 theorem eval_exp {a : A} (ha : IsNilpotent a) :
49     eval a (PowerSeries.exp A) = IsNilpotent.exp a := by
50   obtain ⟨k, hk⟩ := ha
51   rw [eval_eq_sum hk, IsNilpotent.exp_eq_sum hk]
52   apply Finset.sum_congr rfl
53   intro n _
54   simp [PowerSeries.coeff_exp, Algebra.smul_def]
55 
56 end PaperX.NilpotentSeries

Back to source controls