[Merged by Bors] - feat(RingTheory/MvPowerSeries): partial derivatives of `MvPowerSeries` by justus-springer · Pull Request #39626 · leanprover-community/mathlib4

justus-springer · 2026-05-20T17:01:31Z

Previously, we had formal derivatives for PowerSeries and Polynomial and formal partial derivatives for MvPolynomial, but no formal partial derivatives for MvPowerSeries. This PR adds them. Furthermore, PowerSeries.derivative is refactored to be defined in terms of MvPowerSeries.pderiv, which reduces code duplication (In particular, there is no need to define the bare function PowerSeries.derivativeFun anymore).

Most proofs are direct generalizations from the univariate case. I only had to add a few missing API lemmas, which I am PR'ing separately below:

github-actions · 2026-05-20T17:03:00Z

PR summary 9ea5caf3a2

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.RingTheory.PowerSeries.Derivative	1790	1563	-227 (-12.68%)
Mathlib.RingTheory.PowerSeries.Exp	1793	1797	+4 (+0.22%)

Import changes for all files

Files	Import difference
`Mathlib.RingTheory.PowerSeries.Derivative`	-227
14 files `Mathlib.NumberTheory.LSeries.HurwitzZetaValues` `Mathlib.NumberTheory.ModularForms.CuspFormSubmodule` `Mathlib.NumberTheory.ModularForms.DedekindEta` `Mathlib.NumberTheory.ModularForms.Delta` `Mathlib.NumberTheory.ModularForms.Derivative` `Mathlib.NumberTheory.ModularForms.DimensionFormulas.LevelOne` `Mathlib.NumberTheory.ModularForms.Discriminant` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.MDifferentiable` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion` `Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula` `Mathlib.NumberTheory.ModularForms.LevelOne.GradedRing` `Mathlib.NumberTheory.ZetaValues`	1
4 files `Mathlib.NumberTheory.BernoulliPolynomials` `Mathlib.NumberTheory.Bernoulli` `Mathlib.RingTheory.PowerSeries.Exp` `Mathlib.RingTheory.PowerSeries.Log`	4
`Mathlib.RingTheory.MvPowerSeries.Derivative` (new file)	1257

Declarations diff (regex)

+ coeff_pderiv
+ coeff_pderivFun
+ derivative_one
+ pderiv
+ pderiv.ext
+ pderivFun
+ pderivFun_C
+ pderivFun_add
+ pderivFun_coe
+ pderivFun_coe_mul_coe
+ pderivFun_mul
+ pderivFun_one
+ pderivFun_smul
+ pderiv_C
+ pderiv_X
+ pderiv_X_of_ne
+ pderiv_X_self
+ pderiv_coe
+ pderiv_inv
+ pderiv_inv'
+ pderiv_invOf
+ pderiv_one
+ pderiv_pow
+ trunc_pderiv
+ trunc_pderivFun
- derivativeFun_coe_mul_coe

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 9ea5caf).

+20 new declarations
−0 removed declarations

+MvPowerSeries.coeff_pderiv
+MvPowerSeries.coeff_pderivFun
+MvPowerSeries.pderiv
+MvPowerSeries.pderiv.ext
+MvPowerSeries.pderivFun
+MvPowerSeries.pderivFun_C
+MvPowerSeries.pderivFun_add
+MvPowerSeries.pderivFun_one
+MvPowerSeries.pderiv_C
+MvPowerSeries.pderiv_X
+MvPowerSeries.pderiv_X_of_ne
+MvPowerSeries.pderiv_X_self
+MvPowerSeries.pderiv_coe
+MvPowerSeries.pderiv_inv
+MvPowerSeries.pderiv_inv'
+MvPowerSeries.pderiv_invOf
+MvPowerSeries.pderiv_one
+MvPowerSeries.pderiv_pow
+MvPowerSeries.trunc_pderiv
+PowerSeries.derivative_one

No changes to strong technical debt.

Increase in weak tech debt: (relative, absolute) = (1.00, 0.00)

Current number	Change	Type (weak)
5011	1	exposed public sections

Current commit 9ea5caf3a2
Reference commit cd580e54f1

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

…_single_C` (#39623) These lemmas are multivariate analogs to `Polynomial.coeff_C_of_ne_zero`, `Polynomial.coeff_C_succ` and `PowerSeries.coeff_C_of_ne_zero` and `PowerSeries.coeff_succ_C`. They are useful for defining partial derivatives for multivariate power series, see PR #39626. - [x] depends on: #39632

mathlib-merge-conflicts · 2026-06-25T01:23:48Z

This pull request has conflicts, please merge master and resolve them.

…#39624) This formula is useful for defining partial derivatives of multivariate power series, see PR #39626.

…39625) Generalize `coeff_trunc_mul_trunc_eq_coeff_mul` (and its analogs for `truncFinset` and `trunc'`) to allow for different truncation levels for the two arguments. This matches the API for univariate power series, where we already have `PowerSeries.coeff_mul_eq_coeff_trunc_mul_trunc₂`. This is useful for defining partial derivatives of multivariate power series, see PR #39626. Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>

mathlib-dependent-issues · 2026-06-26T13:02:16Z

This PR/issue depends on:

~~[Merged by Bors] - feat(Algebra/MvPolynomial/Basic): coeff_C_of_ne_zero and coeff_add_single_C #39623~~
~~[Merged by Bors] - feat(Algebra/MvPolynomial/PDeriv): a coefficient formula for pderiv #39624~~
~~[Merged by Bors] - feat(RingTheory/MvPowerSeries/Trunc): generalize truncation lemmas #39625~~
By Dependent Issues (🤖). Happy coding!

riccardobrasca · 2026-07-15T15:41:47Z

+    ← coe_mul, MvPolynomial.coe_add]
+
+theorem pderivFun_mul {i : σ} (f g : MvPowerSeries σ R) :
+    pderivFun i (f * g) = f • g.pderivFun i + g • f.pderivFun i := by


Why smul instead of *?

Ah, it's to define the derivation as a Deriv?

Yes, although actually we can also use * and it still works in the definition of pderiv because of defeqs.

I've changed it to * for now.

I see that leibniz' uses smul, so I think your previous version was better, sorry for the noise.

riccardobrasca · 2026-07-16T01:52:55Z

Thanks!

bors d+

mathlib-bors · 2026-07-16T01:52:58Z

✌️ justus-springer can now approve this pull request until 2026-07-30 01:52 UTC (in 2 weeks). To approve and merge, reply with bors r+. More detailed instructions are available here.

⚠️ This delegation only covers changes within Archive/**, Counterexamples/**, docs/**, DownstreamTest/**, Mathlib/**, MathlibTest/**, widget/**, Archive.lean, Counterexamples.lean, docs.lean, Mathlib.lean; an author commit touching anything else will revoke it. Bors also revokes it if a later push changes too many files for it to check the full list — even if it stays within scope.

justus-springer · 2026-07-16T12:38:48Z

bors r+

#39626) Previously, we had formal derivatives for `PowerSeries` and `Polynomial` and formal partial derivatives for `MvPolynomial`, but no formal partial derivatives for `MvPowerSeries`. This PR adds them. Furthermore, `PowerSeries.derivative` is refactored to be defined in terms of `MvPowerSeries.pderiv`, which reduces code duplication (In particular, there is no need to define the bare function `PowerSeries.derivativeFun` anymore). Most proofs are direct generalizations from the univariate case. I only had to add a few missing API lemmas, which I am PR'ing separately below: - [x] depends on: #39623 - [x] depends on: #39624 - [x] depends on: #39625

mathlib-bors · 2026-07-16T13:10:52Z

Pull request successfully merged into master.

Build succeeded:

partial derivatives of MvPowerSeries

f471d1f

github-actions Bot added the t-ring-theory Ring theory label May 20, 2026

mathlib-dependent-issues Bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label May 20, 2026

fix

d24920b

mathlib-merge-conflicts Bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jun 25, 2026

mathlib-bors Bot pushed a commit that referenced this pull request Jun 26, 2026

feat(Algebra/MvPolynomial/PDeriv): a coefficient formula for pderiv (…

d7d52d2

…#39624) This formula is useful for defining partial derivatives of multivariate power series, see PR #39626.

mathlib-dependent-issues Bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jun 26, 2026

Merge branch 'master' into justus/MvPowerSeries_pderiv

686ff66

github-actions Bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jun 26, 2026

justus-springer added 3 commits June 26, 2026 14:05

update deprecation date

ed8cf60

fix

f9955f7

Merge branch 'master' into justus/MvPowerSeries_pderiv

a380513

justus-springer added the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Jun 27, 2026

lint

dd15f82

github-actions Bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Jun 27, 2026

riccardobrasca self-assigned this Jul 15, 2026

riccardobrasca reviewed Jul 15, 2026

View reviewed changes

b-mehta added the awaiting-author A reviewer has asked the author a question or requested changes. label Jul 15, 2026

justus-springer added 2 commits July 15, 2026 17:44

apply suggestions

7ebc454

add semiring section

a18d8da

justus-springer added awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Jul 15, 2026

Merge branch 'master' into justus/MvPowerSeries_pderiv

0786b41

github-actions Bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Jul 15, 2026

mathlib-bors Bot added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Jul 16, 2026

justus-springer added 2 commits July 16, 2026 12:27

mul -> smul

2c09b23

Merge branch 'master' into justus/MvPowerSeries_pderiv

9ea5caf

mathlib-bors Bot added the ready-to-merge This PR has been sent to bors. label Jul 16, 2026

mathlib-bors Bot added the bors-staging This PR is currently being built by bors on the staging branch. label Jul 16, 2026

mathlib-bors Bot changed the title ~~feat(RingTheory/MvPowerSeries): partial derivatives of MvPowerSeries~~ [Merged by Bors] - feat(RingTheory/MvPowerSeries): partial derivatives of MvPowerSeries Jul 16, 2026

mathlib-bors Bot closed this Jul 16, 2026

mathlib-bors Bot removed the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Jul 16, 2026

Uh oh!

Conversation

justus-springer commented May 20, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions Bot commented May 20, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 9ea5caf3a2

Import changes for modified files

Declarations diff (regex)

Declarations diff (Lean)

Uh oh!

mathlib-merge-conflicts Bot commented Jun 25, 2026

Uh oh!

mathlib-dependent-issues Bot commented Jun 26, 2026

Uh oh!

Uh oh!

Uh oh!

riccardobrasca Jul 15, 2026

Choose a reason for hiding this comment

Uh oh!

riccardobrasca Jul 15, 2026

Choose a reason for hiding this comment

Uh oh!

justus-springer Jul 15, 2026

Choose a reason for hiding this comment

Uh oh!

justus-springer Jul 15, 2026

Choose a reason for hiding this comment

Uh oh!

riccardobrasca Jul 16, 2026

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

riccardobrasca commented Jul 16, 2026

Uh oh!

mathlib-bors Bot commented Jul 16, 2026

Uh oh!

justus-springer commented Jul 16, 2026

Uh oh!

mathlib-bors Bot commented Jul 16, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

justus-springer commented May 20, 2026 •

edited

Loading

github-actions Bot commented May 20, 2026 •

edited

Loading