Skip to content

Commit f471d1f

Browse files
justus-springerjustus-springer
committed
partial derivatives of MvPowerSeries
1 parent 1563983 commit f471d1f

7 files changed

Lines changed: 384 additions & 139 deletions

File tree

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6682,6 +6682,7 @@ public import Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
66826682
public import Mathlib.RingTheory.MvPolynomial.Tower
66836683
public import Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
66846684
public import Mathlib.RingTheory.MvPowerSeries.Basic
6685+
public import Mathlib.RingTheory.MvPowerSeries.Derivative
66856686
public import Mathlib.RingTheory.MvPowerSeries.Equiv
66866687
public import Mathlib.RingTheory.MvPowerSeries.Evaluation
66876688
public import Mathlib.RingTheory.MvPowerSeries.Expand

‎Mathlib/Algebra/MvPolynomial/Basic.lean‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -593,6 +593,14 @@ theorem coeff_C [DecidableEq σ] (m) (a) :
593593
coeff m (C a : MvPolynomial σ R) = if 0 = m then a else 0 :=
594594
Finsupp.single_apply
595595

596+
theorem coeff_ne_zero_C {m : σ →₀ ℕ} (h : m ≠ 0) {a : R} : coeff m (C a) = 0 := by
597+
classical rw [coeff_C, if_neg h.symm]
598+
599+
@[simp]
600+
theorem coeff_add_single_C {m : σ →₀ ℕ} {a : R} {i : σ} :
601+
coeff (m + Finsupp.single i 1) (C a) = 0 :=
602+
coeff_ne_zero_C <| fun H ↦ by simpa using congr($(H) i)
603+
596604
lemma eq_C_of_isEmpty [IsEmpty σ] (p : MvPolynomial σ R) :
597605
p = C (p.coeff 0) := by
598606
obtain ⟨x, rfl⟩ := C_surjective σ p

‎Mathlib/Algebra/MvPolynomial/PDeriv.lean‎

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -118,6 +118,21 @@ theorem pderiv_pow {i : σ} {f : MvPolynomial σ R} {n : ℕ} :
118118
theorem pderiv_C_mul {f : MvPolynomial σ R} {i : σ} : pderiv i (C a * f) = C a * pderiv i f := by
119119
rw [C_mul', Derivation.map_smul, C_mul']
120120

121+
theorem coeff_pderiv {i : σ} (p : MvPolynomial σ R) (m : σ →₀ ℕ) :
122+
coeff m (pderiv i p) = coeff (m + single i 1) p * (m i + 1) := by
123+
classical
124+
induction p using MvPolynomial.induction_on' with
125+
| add p q hp hq => simp [hp, hq, add_mul]
126+
| monomial n a =>
127+
rw [pderiv_monomial, coeff_monomial, coeff_monomial]
128+
by_cases h : n = m + single i 1
129+
· simp [h]
130+
simp only [h, ↓reduceIte, zero_mul]
131+
by_cases hn : n i = 0
132+
· simp [hn]
133+
apply if_neg
134+
rwa [tsub_eq_iff_eq_add_of_le (fun _ ↦ by grind)]
135+
121136
theorem pderiv_map {S} [CommSemiring S] {φ : R →+* S} {f : MvPolynomial σ R} {i : σ} :
122137
pderiv i (map φ f) = map φ (pderiv i f) := by
123138
apply induction_on f (fun r ↦ by simp) (fun p q hp hq ↦ by simp [hp, hq]) fun p j eq ↦ ?_

‎Mathlib/RingTheory/MvPowerSeries/Basic.lean‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -351,6 +351,14 @@ theorem coeff_C [DecidableEq σ] (n : σ →₀ ℕ) (a : R) :
351351
theorem coeff_zero_C (a : R) : coeff (0 : σ →₀ ℕ) (C a) = a :=
352352
coeff_monomial_same 0 a
353353

354+
theorem coeff_ne_zero_C {n : σ →₀ ℕ} (h : n ≠ 0) {a : R} : coeff n (C a) = 0 := by
355+
classical rw [coeff_C, if_neg h]
356+
357+
@[simp]
358+
theorem coeff_add_single_C {n : σ →₀ ℕ} {a : R} {i : σ} :
359+
coeff (n + single i 1) (C a) = 0 :=
360+
coeff_ne_zero_C <| fun H ↦ by simpa using congr($(H) i)
361+
354362
@[grind inj]
355363
theorem C_injective : Function.Injective (C : R → MvPowerSeries σ R) := by
356364
intro a b h

‎Mathlib/RingTheory/MvPowerSeries/Derivative.lean‎

Lines changed: 203 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,203 @@
1+
/-
2+
Copyright (c) 2026 Justus Springer. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Justus Springer
5+
-/
6+
module
7+
8+
public import Mathlib.Algebra.MvPolynomial.PDeriv
9+
public import Mathlib.RingTheory.MvPowerSeries.Inverse
10+
public import Mathlib.RingTheory.MvPowerSeries.Trunc
11+
12+
/-!
13+
# Formal partial derivatives of multivariate power series
14+
15+
This file defines `MvPowerSeries.pderiv R i`, the formal partial derivative of a multivariate
16+
power series with respect to variable `i`, as a
17+
`Derivation R (MvPowerSeries σ R) (MvPowerSeries σ R)`.
18+
19+
See also `PowerSeries.derivative` for the univariate setting.
20+
21+
## Main definitions
22+
23+
- `MvPowerSeries.pderiv R i`: the formal partial derivative with respect to `i`, as a derivation.
24+
25+
## Main results
26+
27+
- `MvPowerSeries.coeff_pderiv`: coefficient formula
28+
`coeff n (pderiv R i f) = coeff (n + single i 1) f * (n i + 1)`.
29+
- `MvPowerSeries.pderiv_coe`: compatibility with `MvPolynomial.pderiv`.
30+
- `MvPowerSeries.trunc_pderiv`: truncation commutes with partial differentiation.
31+
- `MvPowerSeries.pderiv.ext`: a power series is determined by its constant term and its partial
32+
derivatives.
33+
- `MvPowerSeries.pderiv_pow`: power rule.
34+
- `MvPowerSeries.pderiv_inv`, `MvPowerSeries.pderiv_inv'`: derivative of an inverse.
35+
36+
-/
37+
38+
@[expose] public section
39+
40+
namespace MvPowerSeries
41+
42+
open MvPolynomial Finsupp
43+
44+
variable {σ R : Type*}
45+
46+
section CommutativeSemiring
47+
48+
variable [CommSemiring R]
49+
50+
/-- The underlying function of the formal partial derivative with respect to variable `i`.
51+
This is packaged as a derivation in `MvPowerSeries.pderiv`. -/
52+
noncomputable def pderivFun (i : σ) (f : MvPowerSeries σ R) : MvPowerSeries σ R :=
53+
fun d ↦ coeff (d + single i 1) f * (d i + 1)
54+
55+
theorem coeff_pderivFun {i : σ} (f : MvPowerSeries σ R) (d : σ →₀ ℕ) :
56+
coeff d (f.pderivFun i) = coeff (d + single i 1) f * (d i + 1) := by
57+
rfl
58+
59+
theorem pderivFun_coe {i : σ} (f : MvPolynomial σ R) :
60+
(f : MvPowerSeries σ R).pderivFun i = f.pderiv i := by
61+
ext
62+
rw [coeff_pderivFun, coeff_coe, coeff_coe, coeff_pderiv]
63+
64+
theorem pderivFun_add {i : σ} (f g : MvPowerSeries σ R) :
65+
pderivFun i (f + g) = pderivFun i f + pderivFun i g := by
66+
ext
67+
rw [coeff_pderivFun, map_add, map_add, coeff_pderivFun, coeff_pderivFun, add_mul]
68+
69+
theorem pderivFun_C {i : σ} (r : R) : pderivFun i (C r) = 0 := by
70+
ext n
71+
rw [coeff_pderivFun, coeff_add_single_C, zero_mul, (coeff n).map_zero]
72+
73+
theorem trunc_pderivFun [DecidableEq σ] {i : σ} (f : MvPowerSeries σ R) (n : σ →₀ ℕ) :
74+
trunc R n (pderivFun i f) = pderiv i (trunc R (n + single i 1) f) := by
75+
ext
76+
rw [coeff_trunc]
77+
split_ifs with h
78+
· rw [coeff_pderivFun, coeff_pderiv, coeff_trunc, if_pos (add_lt_add_left h _)]
79+
· rw [coeff_pderiv, coeff_trunc, if_neg ((add_lt_add_iff_right _).not.mpr h), zero_mul]
80+
81+
-- A special case of `pderivFun_mul`, used in its proof.
82+
private theorem pderivFun_coe_mul_coe {i : σ} (f g : MvPolynomial σ R) :
83+
pderivFun i (f * g : MvPowerSeries σ R) = f * pderiv i g + g * pderiv i f := by
84+
rw [← coe_mul, pderivFun_coe, pderiv_mul, add_comm, mul_comm _ g, ← coe_mul,
85+
← coe_mul, MvPolynomial.coe_add]
86+
87+
theorem pderivFun_mul {i : σ} (f g : MvPowerSeries σ R) :
88+
pderivFun i (f * g) = f • g.pderivFun i + g • f.pderivFun i := by
89+
classical
90+
ext n
91+
have h₁ : n < n + single i 1 := lt_def.mpr ⟨self_le_add_right _ _, i, by simp⟩
92+
have h₂ : n + single i 1 < n + single i 1 + single i 1 :=
93+
lt_def.mpr ⟨self_le_add_right _ _, i, by simp⟩
94+
have h₃ : n < n + single i 1 + single i 1 := lt_trans h₁ h₂
95+
rw [coeff_pderivFun, map_add, ← coeff_trunc_mul_trunc_eq_coeff_mul _ _ _ h₂,
96+
smul_eq_mul, smul_eq_mul, ← coeff_trunc_mul_trunc_eq_coeff_mul₂ _ _ g (f.pderivFun i) h₃ h₁,
97+
← coeff_trunc_mul_trunc_eq_coeff_mul₂ _ _ f (g.pderivFun i) h₃ h₁, trunc_pderivFun,
98+
trunc_pderivFun, ← coeff_coe, ← coeff_coe, ← coeff_coe, ← map_add, coe_mul, coe_mul, coe_mul,
99+
← pderivFun_coe_mul_coe, coeff_pderivFun]
100+
101+
theorem pderivFun_one {i : σ} : pderivFun i (1 : MvPowerSeries σ R) = 0 := by
102+
rw [← map_one C, pderivFun_C (1 : R)]
103+
104+
theorem pderivFun_smul {i : σ} (r : R) (f : MvPowerSeries σ R) :
105+
pderivFun i (r • f) = r • pderivFun i f := by
106+
rw [smul_eq_C_mul, smul_eq_C_mul, pderivFun_mul, pderivFun_C, smul_zero, add_zero, smul_eq_mul]
107+
108+
variable (R) in
109+
/-- The formal partial derivative of a multivariate formal power series with respect to
110+
variable `i`, as an `R`-derivation on `MvPowerSeries σ R`. -/
111+
noncomputable def pderiv (i : σ) : Derivation R (MvPowerSeries σ R) (MvPowerSeries σ R) where
112+
toFun := pderivFun i
113+
map_add' := pderivFun_add
114+
map_smul' := pderivFun_smul
115+
map_one_eq_zero' := pderivFun_one
116+
leibniz' := pderivFun_mul
117+
118+
@[simp] theorem pderiv_C {i : σ} {r : R} : pderiv R i (C r) = 0 := pderivFun_C r
119+
120+
@[simp] theorem pderiv_one {i : σ} : pderiv R i 1 = 0 := pderiv_C
121+
122+
theorem coeff_pderiv {i : σ} (f : MvPowerSeries σ R) (n : σ →₀ ℕ) :
123+
coeff n (pderiv R i f) = coeff (n + single i 1) f * (n i + 1) :=
124+
coeff_pderivFun f n
125+
126+
theorem pderiv_coe {i : σ} (f : MvPolynomial σ R) :
127+
pderiv R i f = MvPolynomial.pderiv i f := pderivFun_coe f
128+
129+
@[simp]
130+
theorem pderiv_X_self {i : σ} : pderiv R i (X i) = 1 := by
131+
classical
132+
ext n
133+
simp only [coeff_pderiv, coeff_X, boole_mul, add_eq_right, coeff_one]
134+
split_ifs <;> simp_all
135+
136+
@[simp]
137+
theorem pderiv_X_of_ne {i j : σ} (h : j ≠ i) : pderiv R i (X j) = 0 := by
138+
classical
139+
ext n
140+
simpa only [coeff_pderiv, coeff_X, boole_mul, coeff_zero] using
141+
if_neg (ne_iff.mpr ⟨i, by grind [add_apply]⟩)
142+
143+
theorem pderiv_X [DecidableEq σ] {i j : σ} :
144+
pderiv R i (X j) = Pi.single (M := fun _ => _) i 1 j := by
145+
by_cases h : i = j
146+
· subst h; simp only [pderiv_X_self, Pi.single_eq_same]
147+
· grind [pderiv_X_of_ne]
148+
149+
theorem trunc_pderiv [DecidableEq σ] {i : σ} (f : MvPowerSeries σ R) (n : σ →₀ ℕ) :
150+
trunc R n (pderiv R i f) = MvPolynomial.pderiv i (trunc R (n + single i 1) f) :=
151+
trunc_pderivFun ..
152+
153+
/-- The partial derivative of `g^n` equals `n * g^(n-1) * g'`. -/
154+
theorem pderiv_pow {i : σ} (g : MvPowerSeries σ R) (n : ℕ) :
155+
pderiv R i (g ^ n) = n * g ^ (n - 1) * pderiv R i g := by
156+
rw [Derivation.leibniz_pow, smul_eq_mul, nsmul_eq_mul, mul_assoc]
157+
158+
end CommutativeSemiring
159+
160+
/-- If `f` and `g` have the same constant term and all partial derivatives, then they are equal.
161+
162+
The `CommRing` assumption is needed because the proof uses `smul_right_inj`, which requires
163+
cancellation of addition in `R`; `IsAddTorsionFree` alone does not suffice. -/
164+
theorem pderiv.ext [CommRing R] [IsAddTorsionFree R] {f g : MvPowerSeries σ R}
165+
(hD : ∀ i, pderiv R i f = pderiv R i g) (hc : constantCoeff f = constantCoeff g) : f = g := by
166+
ext n
167+
by_cases h : n = 0
168+
· rw [h, coeff_zero_eq_constantCoeff, hc]
169+
obtain ⟨i, hi : n i ≠ 0⟩ := ne_iff.mp h
170+
have : single i 1 ≤ n := fun j ↦ by
171+
by_cases hj : j = i <;> grind [single_eq_same, single_eq_of_ne]
172+
have e := congr(coeff (n - single i 1) $(hD i))
173+
rwa [coeff_pderiv, coeff_pderiv, tsub_add_cancel_of_le this, coe_tsub, Pi.sub_apply,
174+
single_eq_same, Nat.cast_sub (Nat.one_le_iff_ne_zero.mpr hi), Nat.cast_one, sub_add_cancel,
175+
mul_comm, ← nsmul_eq_mul, mul_comm, ← nsmul_eq_mul, smul_right_inj hi] at e
176+
177+
@[simp]
178+
theorem pderiv_inv {i : σ} [CommRing R] (f : (MvPowerSeries σ R)ˣ) :
179+
pderiv R i ↑f⁻¹ = -(↑f⁻¹ : MvPowerSeries σ R) ^ 2 * pderiv R i f := by
180+
apply Derivation.leibniz_of_mul_eq_one
181+
simp
182+
183+
@[simp]
184+
theorem pderiv_invOf {i : σ} [CommRing R] (f : MvPowerSeries σ R) [Invertible f] :
185+
pderiv R i ⅟f = -⅟f ^ 2 * pderiv R i f := by
186+
rw [Derivation.leibniz_invOf, smul_eq_mul]
187+
188+
/-
189+
The following theorem is stated only in the case that `R` is a field. This is because
190+
there is currently no instance of `Inv (MvPowerSeries σ R)` for more general base rings `R`.
191+
-/
192+
193+
@[simp]
194+
theorem pderiv_inv' {i : σ} [Field R] (f : MvPowerSeries σ R) :
195+
pderiv R i f⁻¹ = -f⁻¹ ^ 2 * pderiv R i f := by
196+
by_cases h : constantCoeff f = 0
197+
· suffices f⁻¹ = 0 by
198+
rw [this, pow_two, zero_mul, neg_zero, zero_mul, map_zero]
199+
rwa [MvPowerSeries.inv_eq_zero]
200+
apply Derivation.leibniz_of_mul_eq_one
201+
exact MvPowerSeries.inv_mul_cancel (h := h)
202+
203+
end MvPowerSeries

‎Mathlib/RingTheory/MvPowerSeries/Trunc.lean‎

Lines changed: 39 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -125,16 +125,24 @@ theorem truncFinset_map [CommSemiring S] (f : R →+* S) (p : MvPowerSeries σ R
125125
ext x
126126
by_cases x ∈ s <;> grind [coeff_map, MvPolynomial.coeff_map]
127127

128-
theorem coeff_truncFinset_mul_truncFinset_eq_coeff_mul (hs : IsLowerSet (s : Set (σ →₀ ℕ)))
129-
{x : σ →₀ ℕ} (f g : MvPowerSeries σ R) (hx : x ∈ s) :
130-
(truncFinset R s f * truncFinset R s g).coeff x = coeff x (f * g) := by
128+
/-- A coefficient of a product of finset-truncated power series equals the coefficient of the
129+
untruncated product, with the two truncation finsets `s` and `t` allowed to differ. -/
130+
theorem coeff_truncFinset_mul_truncFinset_eq_coeff_mul₂ {t : Finset (σ →₀ ℕ)}
131+
(hs : IsLowerSet (s : Set (σ →₀ ℕ))) (ht : IsLowerSet (t : Set (σ →₀ ℕ)))
132+
{x : σ →₀ ℕ} (f g : MvPowerSeries σ R) (hxs : x ∈ s) (hxt : x ∈ t) :
133+
(truncFinset R s f * truncFinset R t g).coeff x = coeff x (f * g) := by
131134
classical
132135
simp only [MvPowerSeries.coeff_mul, MvPolynomial.coeff_mul]
133136
apply sum_congr rfl
134137
rintro ⟨i, j⟩ hij
135138
simp only [mem_antidiagonal] at hij
136-
rw [coeff_truncFinset_of_mem _ (hs (show i ≤ x by simp [← hij]) hx),
137-
coeff_truncFinset_of_mem _ (hs (show j ≤ x by simp [← hij]) hx)]
139+
rw [coeff_truncFinset_of_mem _ (hs (show i ≤ x by simp [← hij]) hxs),
140+
coeff_truncFinset_of_mem _ (ht (show j ≤ x by simp [← hij]) hxt)]
141+
142+
theorem coeff_truncFinset_mul_truncFinset_eq_coeff_mul (hs : IsLowerSet (s : Set (σ →₀ ℕ)))
143+
{x : σ →₀ ℕ} (f g : MvPowerSeries σ R) (hx : x ∈ s) :
144+
(truncFinset R s f * truncFinset R s g).coeff x = coeff x (f * g) :=
145+
coeff_truncFinset_mul_truncFinset_eq_coeff_mul₂ hs hs f g hx hx
138146

139147
theorem truncFinset_truncFinset_pow (hs : IsLowerSet (s : Set (σ →₀ ℕ))) {k : ℕ} (hk : 1 ≤ k)
140148
(p : MvPowerSeries σ R) : truncFinset R s ((truncFinset R s p) ^ k) =
@@ -190,6 +198,21 @@ theorem trunc_one (n : σ →₀ ℕ) (hnn : n ≠ 0) : trunc R n 1 = 1 :=
190198
theorem trunc_C (n : σ →₀ ℕ) (hnn : n ≠ 0) (a : R) : trunc R n (C a) = MvPolynomial.C a :=
191199
truncFinset_C (by simpa using pos_of_ne_zero hnn) a
192200

201+
/-- A coefficient of a product of truncated power series equals the coefficient of the untruncated
202+
product, with the two truncation levels `n₁` and `n₂` allowed to differ. -/
203+
theorem coeff_trunc_mul_trunc_eq_coeff_mul₂ (n₁ n₂ : σ →₀ ℕ)
204+
(f g : MvPowerSeries σ R) {m : σ →₀ ℕ} (h₁ : m < n₁) (h₂ : m < n₂) :
205+
(trunc R n₁ f * trunc R n₂ g).coeff m = coeff m (f * g) :=
206+
coeff_truncFinset_mul_truncFinset_eq_coeff_mul₂ (by intro; grind) (by intro; grind) f g
207+
(by simpa) (by simpa)
208+
209+
/-- A coefficient of a product of truncated power series equals the coefficient of the untruncated
210+
product. Both factors are truncated at the same level `n`. -/
211+
theorem coeff_trunc_mul_trunc_eq_coeff_mul (n : σ →₀ ℕ)
212+
(f g : MvPowerSeries σ R) {m : σ →₀ ℕ} (h : m < n) :
213+
(trunc R n f * trunc R n g).coeff m = coeff m (f * g) :=
214+
coeff_trunc_mul_trunc_eq_coeff_mul₂ n n f g h h
215+
193216
@[simp]
194217
theorem trunc_C_mul (n : σ →₀ ℕ) (a : R) (p : MvPowerSeries σ R) :
195218
trunc R n (C a * p) = MvPolynomial.C a * trunc R n p := by
@@ -231,11 +254,20 @@ theorem trunc'_one (n : σ →₀ ℕ) : trunc' R n 1 = 1 := truncFinset_one (by
231254
theorem trunc'_C (n : σ →₀ ℕ) (a : R) : trunc' R n (C a) = MvPolynomial.C a :=
232255
truncFinset_C (by simp) a
233256

234-
/-- Coefficients of the truncation of a product of two multivariate power series -/
257+
/-- A coefficient of a product of truncated power series equals the coefficient of the untruncated
258+
product, with the two truncation levels `n₁` and `n₂` allowed to differ. -/
259+
theorem coeff_trunc'_mul_trunc'_eq_coeff_mul₂ (n₁ n₂ : σ →₀ ℕ)
260+
(f g : MvPowerSeries σ R) {m : σ →₀ ℕ} (h₁ : m ≤ n₁) (h₂ : m ≤ n₂) :
261+
(trunc' R n₁ f * trunc' R n₂ g).coeff m = coeff m (f * g) :=
262+
coeff_truncFinset_mul_truncFinset_eq_coeff_mul₂ (by intro; grind) (by intro; grind) f g
263+
(by simpa) (by simpa)
264+
265+
/-- A coefficient of a product of truncated power series equals the coefficient of the untruncated
266+
product. Both factors are truncated at the same level `n`. -/
235267
theorem coeff_trunc'_mul_trunc'_eq_coeff_mul (n : σ →₀ ℕ)
236268
(f g : MvPowerSeries σ R) {m : σ →₀ ℕ} (h : m ≤ n) :
237269
(trunc' R n f * trunc' R n g).coeff m = coeff m (f * g) :=
238-
coeff_truncFinset_mul_truncFinset_eq_coeff_mul (by intro; grind) f g (by simpa)
270+
coeff_trunc'_mul_trunc'_eq_coeff_mul₂ n n f g h h
239271

240272
@[deprecated coeff_trunc'_mul_trunc'_eq_coeff_mul (since := "2026-02-20")]
241273
theorem coeff_mul_eq_coeff_trunc'_mul_trunc' (n : σ →₀ ℕ) (f g : MvPowerSeries σ R) {m : σ →₀ ℕ}

0 commit comments

Comments
 (0)