feat(Analysis/Calculus/PartialDerivatives): Propose notation for partial derivatives.

[Paul-Lez]

This PR introduces a notation for partial derivatives, taken with respect to a canonical basis. The idea here is that this might be useful for e.g. writing down PDEs. The notation allows use to write things like

-- The canonical basis for `ℝ × ℝ` is indexed by `Fin 0` so `∂₀[ℝ]` corresponds to taking 
-- the first partial derivative
example : (∂₀[ℝ] fun (x : ℝ × ℝ) => x.1) 0 = 1 := by
  simp [Pi.zero_def, lineDeriv]

This has already been discussed on Zulip here.

I've opened this PR as a draft in order to get preliminary feedback on the contents (e.g. is this appropriate for Mathlib?); the file contains some demos of the notation in action.

Co-authored-by: Eric Wieser efw@google.com

---

• depends on: feat(LinearAlgebra/Basis/HasCanonicalBasis): propose HasCanonicalBasis class #25425

[github-actions]

PR summary 7ee2a85e61

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.LinearAlgebra.Basis.HasCanonicalBasis (new file)	1975
Mathlib.Analysis.Calculus.PartialDerivatives.Notation (new file)	2025

---

Declarations diff

+ EuclideanSpace.hasCanonicalBasis
+ HasCanonicalBasis
+ Pi.hasCanonicalBasis
+ basis_apply
+ instance : HasCanonicalBasis 𝕜 (𝕜 × 𝕜 × 𝕜) (Fin 3)
+ instance : HasCanonicalBasis 𝕜 (𝕜 × 𝕜) (Fin 2) (![(1, 0), (0, 1)])
+ instance : HasCanonicalBasis 𝕜 𝕜 (Fin 1) (fun _ ↦ 1)
+ instance [Ring 𝕜] (p : ENNReal) :
+ partialDeriv
+ prod
+ reindex

You can run this locally as follows

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

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/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).

[lecopivo]

I have similar notation in SciLean but I think they are trying to simplify different things.

• your PR defines what a canonical basis is and the notation makes it easier to write derivatives in the direction of the canonical basis
• in SciLean the derivative notation mainly makes it simpler to write mathematical $$\frac{\partial f(x)}{\partial x}|_{x=x_0}$$ i.e. differentiate expression w.r.t. some variable and then evaluate it at some point.

I would suggest merging these two notations together.

Also it might make sense to split this PR into two

• PR for HasCanonicalBasis such that you get feedback from people that do not care about partial derivatives
• PR just for the derivative notation which can add notation for normal and partial derivatives

[lecopivo]

I think this should be abbrev instead of partialDeriv otherwise you will have to duplicate whole API for lineDeriv or start every proof with unfold partialDeriv.

[ocfnash]

(or ideally not even an abbrev)

[lecopivo]

I have similar notation in SciLean but I think they are trying simplify different things.

• your PR defines what a canonical basis is and the notation makes it easier to write derivatives in the direction of the canonical basis
• in SciLean the derivative notation mainly makes it simpler to write mathematical $$\frac{\partial f(x)}{\partial x}|_{x=x_0}$$ i.e. differentiate expression w.r.t. some variable and then evaluate it at some point.

Suggestion to combine SciLean and your PR notations:

In SciLean you can write:
(a) ∂ f = fderiv ℝ f
(b) ∂ (x':=x), f x' = fderiv ℝ f x
(c) ∂ (x':=x;dx), f x' = fderiv ℝ f x dx
(d) ∂ (x':=x), f x' = deriv ℝ f x if domain of f is ℝ

I would propose extending you notation in similar fashion such that instead of writing

(∂₀[ℝ] fun (x : ℝ × ℝ) => x.1) 0

you write

(∂₀[ℝ] (x := (0 : ℝ × ℝ)), x.1)

i.e. ∂ works similarly to fun, ∑, ∏, ∀, dropping fun and =>. Personally find this more readable. For example the first term of Lagrange-Euler equation can be written as

∂ (t':=t), ∂ (x':=x t'), L t' x'

instead of as

∂ (fun t' => ∂ (fun x' => L t' x') (x t')) t

SciLean defines this notation here.

There is an elaborator for ∂ f that decides whether to use fderiv or deriv based on the domain of f and macro rules to expand ∂ (x':=x), f x' into `∂ (fun x' => f x') x' which is then consumed by the elaborator.

[Paul-Lez]

That sounds good! I'll have a go at combining the two

[lecopivo]

Use FinEnum to index basis vectors

You can index basis vectors with a type that implements FinEnum ι and define the notation as

∂ᵢ[ℝ] f = (partialDeriv 𝕜 f · (f (FinEnum.equiv.symm i))

This way the

noncomputable abbrev prod {V : Type v} {W : Type v'} {κ : Type w'}
    [AddCommGroup V] [AddCommGroup W] [Module 𝕜 V] [Module 𝕜 W]
    (f : ι → V) (g : κ → W) [HasCanonicalBasis 𝕜 V ι f] [HasCanonicalBasis 𝕜 W κ g] :
    HasCanonicalBasis 𝕜 (V × W) (ι ⊕ κ) (Sum.elim (LinearMap.inl 𝕜 _ _ ∘ f)
      (LinearMap.inr 𝕜 _ _ ∘ g)) := ...

can be instance and there is not need for having these specialized instances like

noncomputable instance : HasCanonicalBasis 𝕜 (𝕜 × 𝕜) (Fin 2)

In SciLean, I have class IndexType ι n which is effectively FinEnum ι with n = FinEnum.card. I found that exposing nin the type makes some things easier and some types cleaner looking. For example, 𝕜 × 𝕜 is equivalent to Fin (1+1) rather than to Fin (FinEnum.card + FinEnum.card) which helps unification a lot.

I would also change

noncomputable instance : HasCanonicalBasis 𝕜 𝕜 (Fin 1) (fun _ ↦ 1)

to

noncomputable instance : HasCanonicalBasis 𝕜 𝕜 Unit (fun _ ↦ 1)

[lecopivo]

By using FinEnum to index basis vectors this instance and the one bellow is not necessary.

[lecopivo]

Another suggestion for the notation is to remove the [𝕜] argument

In SciLean, the derivative notation does not state the base field explicitly. It is expected that you usually work with one base field and state that with set_default_scalar 𝕜 at the top of the file which just defines local notation defaultScalar% that expands to 𝕜 and the notation uses defaultScalar%

macro "set_default_scalar" r:term : command =>
  `(local macro_rules | `(defaultScalar%) => do pure (← `($r)).raw)

This is Kyle's solution discussed here https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/notation.20over.20field/with/419274309

Adding something like defaultScalar% should be done as separate PR and then we can add an option to omit 𝕜 in the notation.

[lecopivo]

I'm really unsure about f as an argument here. Why is it not a field of the class?

My general rule of thumb is that if f appears in some type in downstream code then it should be a parameter but if it does not appear in the type then it should be a field.

Having separate f field can still be useful for kernel reduction as basis = f might be only prepositionally equal but not defeq. However, I'm still a bit skeptical, why doesn't HasCanonicalBasis just pick canonical Basis? Do you really need good defeq here?

[ocfnash]

Are you sure that lineDeriv deserves to be the privileged concept which gets the special notation?

Admittedly I have a bias from my early training but it is the Fréchet derivative which is the well-behaved concept. If we cannot have notation for both, then I would favour giving the notation to Fréchet.

[lecopivo]

That is definitely something to consider, also fderiv has better API right now. However, there is a difference between the derivative as a function and the notion of differentiability.

If a function f is Differentiable (i.e. Frechet differentiable) then fderiv R f x dx = lineDeriv R f x dx.

Personally, I would get rid of fderiv and replace it with if h : DifferentiableAt f x then <lineDeriv R f, ...> else 0 where ... is a proof saying that Gateaux and Frechet derivative coincide for Frechet differentiable functions.

[ocfnash]

I don't think we should try to emphasise lineDeriv like this. The well-behaved Fréchet derivative is the definition about which we can prove most useful results. So if we tried to hide it away as you suggest, most lemmas will just have to begin with a little dance to break through to the useful concept.

[lecopivo]

I see, my point of view is more from 'tactic writing' point of view: stick to one notion of derivative and write theorems only for it with the weakest notion of differentiability possible.

Every derivative function will require very similar set of theorems which are effectively duplicates of each other. For example, deriv vs fderiv, lots of theorems about special functions are formulated only for deriv. So I see the possibility of turning everything into lineDeriv

Anyway, at the current state of Mathlib I agree that the special notation should go to fderiv rather than to lineDeriv.

[Paul-Lez]

Will change to fderiv!

[leanprover-community-bot-assistant]

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

[mathlib-dependent-issues]

This PR/issue depends on:

• feat(LinearAlgebra/Basis/HasCanonicalBasis): propose HasCanonicalBasis class #25425
  By Dependent Issues (🤖). Happy coding!