Partial derivatives

Stream: mathlib4

[Kiran Singh]

I'm currently in high school and very interested in math and formal logic. I'd like to contribute to mathlib4, specifically by adding partial derivatives to the library. I'm currently working through Vector Calculus, Linear Algebra and Differential Forms by Hubbard & Hubbard and have already written some proofs that I'd want to include, and I'm about to submit a pull request. After looking through the current derivatives section of the library, it would be good to get some guidance on whether the proofs should be written based on theorems from the Fréchet derivative, the two-dimensional derivative or both.  The proofs in each of their lean files seem to reference each other. I have read the Lean theorem prover guide (https://leanprover.github.io/theorem_proving_in_lean/) and also the contributing guide at https://leanprover-community.github.io/contribute/index.html, and if there is anything else that I should read before submitting the PR please let me know.

[Yury G. Kudryashov]

The main issue with partial derivatives is that we don't have a notion of a canonical basis. You can already use docs#lineDeriv with a direction given by k-th basis vector to deal with partial derivatives.

[Yury G. Kudryashov]

There are many ways to represent, e.g., $\mathbb R^3$ in Mathlib. At least,

• ℝ × ℝ × ℝ
• (ℝ × ℝ) × ℝ
• Fin 3 → ℝ
• ℝ × (Fin 2 → ℝ)
• ...
  with variations for docs#EuclideanSpace

[Yury G. Kudryashov]

Also, do you want to deal with Fréchet derivatives of f : (E × F) → G with respect to the first and second vector variables or not?

[Eric Wieser]

Yury G. Kudryashov said:

we don't have a notion of a canonical basis.

Should we have a Type-valued version of Module.Free for this? I guess we get in trouble with Fin 3 -> Real, since this would give a basis indexed by (_ : Fin 3) × Unit if we just let typeclass search pull part the pi type

[Yury G. Kudryashov]

Should we force Fin _ index type? FinEnum can help here

[Kevin Buzzard]

Rather than a type-valued version of Module.free (which is just Basis right?) we could just have a bundled "based vector space" type

[Johan Commelin]

Here is some ancient Lean 3 code that Reid and I wrote at some point

import data.equiv.basic
import data.fin
import for_mathlib.finvec
import for_mathlib.misc

open function set
open_locale finvec

-- R is the type in which coordinates take values,
-- which we can imagine as being the real numbers,
-- though we do not assume anything about R.
variables (R : Type*)

section coordinates

/--
A type X *has coordinates* valued in R
when it is equipped with an embedding into Rⁿ for some specific n.
Mathematically, we can identify X with a subset of Rⁿ,
but in Lean, the type X is not restricted to being of the form
`subtype s` for some `s : set (fin n → R)`.
Informally, we denote this situation by "X ⊆ Rⁿ".
-/
class has_coordinates (X : Type*) :=
(ambdim : ℕ)
(coords : X → finvec ambdim R)
(inj : injective coords)

def coords {X : Type*} [cX : has_coordinates R X] : X → finvec cX.ambdim R :=
cX.coords

/-- Magic causing `simps` to use `coords` on the left hand side of generated `simp` lemmas. -/
def has_coordinates.simps.coords := @coords R

/- TODO: `simps` generates over-applied lemmas like

  coords R x i = (...) i

rather than

  coords R x = ...

because the type of `coords R x` is itself a function type (`fin n → R`).
We work around this with `{ fully_applied := ff }`
but then the lemmas are under-applied instead:

  coords R = λ x, ...
-/

variables {R}

lemma injective_coords (X : Type*) [cX : has_coordinates R X] : injective (@coords R X cX) :=
cX.inj

-- TODO: generalize to `finvec n X` where `[has_coordinates R X]`;
-- but this will lose the definition as `id`.
/-- Rⁿ tautologically has coordinates given by the identity. -/
@[simps { fully_applied := ff }] instance has_coordinates.finvec (n : ℕ) : has_coordinates R (finvec n R) :=
{ ambdim := n,
  coords := λ x, x,
  inj := injective_id }

/-- R has coordinates given by the usual identification R ≃ R¹. -/
@[simps { fully_applied := ff }] instance has_coordinates.self : has_coordinates R R :=
{ ambdim := 1,
  coords := const (fin 1),
  inj := λ a b h, congr_fun h 0 }

/-- If X ⊆ Rⁿ and Y ⊆ Rᵐ then X × Y ⊆ Rⁿ⁺ᵐ. -/
@[simps { fully_applied := ff, simp_rhs := tt }] instance has_coordinates.prod
  {X Y : Type*} [cX : has_coordinates R X] [cY : has_coordinates R Y] :
  has_coordinates R (X × Y) :=
{ ambdim := cX.ambdim + cY.ambdim,
  coords := λ p, coords R p.1 ++ coords R p.2,
  inj := injective.comp (equiv.injective _) (injective.prod_map cX.inj cY.inj) }

/-- If X ⊆ Rⁿ and S is a subset of X then S ⊆ Rⁿ. -/
@[simps { fully_applied := ff }] instance has_coordinates.subtype {X : Type*} [cX : has_coordinates R X] (s : set X) :
  has_coordinates R s :=
{ ambdim := cX.ambdim,
  coords := λ a, coords R (subtype.val a),
  inj := injective.comp cX.inj subtype.val_injective }

/-- Any subsingleton may be regarded as having coordinates valued in R⁰. -/
@[simps { fully_applied := ff }] def has_coordinates.subsingleton {X : Type*} [subsingleton X] : has_coordinates R X :=
{ ambdim := 0,
  coords := λ x, fin_zero_elim,
  inj := subsingleton_injective _ }

@[simps { fully_applied := ff, rhs_md := semireducible }]
instance pempty.has_coordinates : has_coordinates R pempty := has_coordinates.subsingleton

@[simps { fully_applied := ff, rhs_md := semireducible }]
instance punit.has_coordinates : has_coordinates R punit := has_coordinates.subsingleton

variables (R)

/-- The subset of Rⁿ which is mapped onto by X. -/
def coordinate_image (X : Type*) [cX : has_coordinates R X] := range (@coords R X _)

variables {R}

lemma coordinate_image_prod {X Y : Type*} [cX : has_coordinates R X] [cY : has_coordinates R Y] :
  coordinate_image R (X × Y) = coordinate_image R X ⊠ coordinate_image R Y :=
begin
  apply set.ext,
  refine finvec.rec (λ v w, _),
  rw finvec.mem_prod_iff,
  simp [coordinate_image, finvec.append.inj_iff]
end

end coordinates

section reindexing

/--
If X and Y have coordinates valued in R,
then a function f : X → Y is a *reindexing*
if it fits into a diagram

  X ⊆ Rⁿ
f ↓   ↓ r^*
  Y ⊆ Rᵐ

where the map r^* is given by reindexing the coordinates
according to some map r : fin m → fin n, so that
r^*(x₁, ..., xₙ) = (xᵣ₍₁₎, ..., xᵣ₍ₘ₎).

For example, projections and subset inclusions are reindexings,
as are maps built from these by forming products.
A given map f may be a reindexing in more than one way (i.e., for several r),
for example if both X and Y are empty.
Here we don't care about the choice of r so we make `is_reindexing` a Prop.

A basic fact about definability is that
the preimage of a definable set under a map of the form r^* is definable.
This notion `is_reindexing` will let us reformulate this result
in the language of `has_coordinates`.
-/
inductive is_reindexing
  {X Y : Type*} [cX : has_coordinates R X] [cY : has_coordinates R Y]
  (f : X → Y) : Prop
| mk (σ : fin cY.ambdim → fin cX.ambdim)
     (h : ∀ x i, coords R x (σ i) = coords R (f x) i)
  : is_reindexing

variables {R}

lemma is_reindexing.id (X : Type*) [cX : has_coordinates R X] :
  is_reindexing R (id : X → X) :=
⟨id, λ x i, rfl⟩

lemma is_reindexing.comp
  {X Y Z : Type*} [cX : has_coordinates R X] [cY : has_coordinates R Y] [cZ : has_coordinates R Z]
  {g : Y → Z} (hg : is_reindexing R g) {f : X → Y} (hf : is_reindexing R f) :
  is_reindexing R (g ∘ f) :=
begin
  cases hf with fσ hf,
  cases hg with gσ hg,
  refine ⟨fσ ∘ gσ, λ x i, _⟩,
  simp [hf, hg]
end

lemma is_reindexing.fst
  {X Y : Type*} [cX : has_coordinates R X] [cY : has_coordinates R Y] :
  is_reindexing R (prod.fst : X × Y → X) :=
begin
  refine ⟨fin.cast_add _, λ p i, _⟩,
  change finvec.left (_ ++ _) i = _,
  simp
end

lemma is_reindexing.snd
  {X Y : Type*} [cX : has_coordinates R X] [cY : has_coordinates R Y] :
  is_reindexing R (prod.snd : X × Y → Y) :=
begin
  refine ⟨fin.nat_add _, λ p i, _⟩,
  change finvec.right (_ ++ _) i = _,
  simp
end

lemma is_reindexing.prod
  {X Y Z : Type*} [cX : has_coordinates R X] [cY : has_coordinates R Y] [cZ : has_coordinates R Z]
  {f : X → Y} (hf : is_reindexing R f) {g : X → Z} (hg : is_reindexing R g) :
  is_reindexing R (λ x, (f x, g x)) :=
begin
  cases hf with fσ hf,
  cases hg with gσ hg,
  let σ : fin cY.ambdim ⊕ fin cZ.ambdim → fin cX.ambdim := λ i, sum.cases_on i fσ gσ,
  refine ⟨σ ∘ sum_fin_sum_equiv.symm, λ x, _⟩,
  dsimp only [(∘)],
  -- TODO: lemma for `e : α ≃ β` that `(∀ a, p a (e a)) ↔ (∀ b, p (e.symm b) b)`?
  refine sum_fin_sum_equiv.forall_congr_left.mp _,
  rintro (i|i); rw equiv.symm_apply_apply,
  { refine (hf _ i).trans _,
    refine congr_fun _ i,
    exact finvec.left_append.symm },
  { refine (hg _ i).trans _,
    refine congr_fun _ i,
    exact finvec.right_append.symm }
end

lemma is_reindexing.coords {X : Type*} [cX : has_coordinates R X] :
  is_reindexing R (λ (x : X), coords R x) :=
⟨id, λ x j, rfl⟩

lemma is_reindexing.coord {X : Type*} [cX : has_coordinates R X] (i : fin cX.ambdim) :
  is_reindexing R (λ x, coords R x i) :=
⟨λ _, i, λ x j, rfl⟩

lemma is_reindexing.subtype.val {X : Type*} [cX : has_coordinates R X] {s : set X} :
  is_reindexing R (subtype.val : s → X) :=
⟨id, λ x j, rfl⟩

lemma is_reindexing.finvec.left {n m : ℕ} :
  is_reindexing R (finvec.left : (finvec (n+m) R) → (finvec n R)) :=
⟨fin.cast_add m, λ x j, rfl⟩

lemma is_reindexing.finvec.right {n m : ℕ} :
  is_reindexing R (finvec.right : (finvec (n+m) R) → (finvec m R)) :=
⟨fin.nat_add n, λ x j, rfl⟩

lemma is_reindexing.finvec.init {n : ℕ} :
  is_reindexing R (finvec.init : (finvec (n+1) R) → (finvec n R)) :=
⟨fin.cast_succ, λ x j, rfl⟩

lemma is_reindexing.finvec.snoc {n : ℕ} :
  is_reindexing R (λ (p : finvec n R × R), p.1.snoc p.2) :=
⟨id, by { intros x j, rw finvec.snoc_eq_append, refl }⟩

end reindexing

[Johan Commelin]

It depends on some for_mathlib stuff from a private repo. But I guess the ideas can be understood without access to those files.

[Eric Wieser]

Kevin Buzzard said:

which is just Basis right?

Right, but a canonical one like volume is a canonical measure

[Edward van de Meent]

so then a bundled class-version of Basis? possibly add on a type def WithBasis X b to infer a non-canonical instance?

[Edward van de Meent]

i wonder if there are some spaces with multiple "canonical" bases...

[Edward van de Meent]

i.e. with at least two bases, both of which are common, perhaps even so that swapping is a common technique?

[Kiran Singh]

Sorry for the late response, I've been busy with school for the past week.

I had initially started down the track of building off of ordinary and Frechet derivative theorems as a foundation for partial derivatives. An example of what I had been doing is below.

Your suggestions were helpful, though I'm still getting to grips with what some of the suggestions mean. Based on one of the suggestions, I'm realizing that the line derivative already in Mathlib would work as a partial derivative, when the vector that it's taken with respect to is part of the basis of the set the function is on. So, I think that instead of building off of the Frechet and ordinary derivative code, I'll instead focus on adding theorems specific to partial derivatives, based on the definition of line derivatives already in Mathlib. Some of the theorems that I plan to work on first are Taylor's Theorem and Clairaut's Theorem. Would it make sense to implement those based on the line derivative as I'm planning to do? Or would adding code for canonical bases and specific code for partial derivatives be more useful - and in that case, how would you suggest that a newcomer to Lean should start?

An example of the code (As the import for Linear Algebra hasn't been working for me, I haven't been able to check this code, though I think this was how I wrote it previously)

import Mathlib.LinearAlgebra.Basis.Defs
import Mathlib.Analysis.Calculus.FDeriv.Basic
import Mathlib.Analysis.Calculus.Deriv.Basic
import Mathlib.Analysis.NormedSpace.OperatorNorm.NormedSpace


universe u v w

noncomputable section

open scoped Topology ENNReal NNReal
open Filter Asymptotics Set

open ContinuousLinearMap (smulRight smulRight_one_eq_iff)

variable {𝕜 : Type u} [NontriviallyNormedField 𝕜]
variable {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F]
variable {E : Type w} [NormedAddCommGroup E] [NormedSpace 𝕜 E]

def PartialDerivWithin (f : 𝕜 × 𝕜 → F) (s : Set 𝕜 × 𝕜) (x : 𝕜) (b: basis ι R (𝕜 × 𝕜)) (v: b i):=
  fderivWithin 𝕜 × 𝕜 (f v c) s x

def PartialDeriv (f : 𝕜 × 𝕜 → F) (s : Set 𝕜 × 𝕜) (x : 𝕜) (b: basis ι R (𝕜 × 𝕜)) (v: b i):=
  fderiv 𝕜 × 𝕜 (f v c) x

[Patrick Massot]

We still need to understand why you want partial derivatives in Mathlib. What do you plan to do with them?

[Patrick Massot]

Also the code snippet you posted doesn’t make any sense. What are you trying to do?

[Patrick Massot]

Thinking back about this, I fear my comments may be a bit disheartening without any coding help. Here a version of our code that means something (but I am really unsure whether this is what you meant).

def PartialDerivWithin (f : 𝕜 × 𝕜 → F) (s : Set (𝕜 × 𝕜)) (x : 𝕜 × 𝕜) (b: Basis ι 𝕜 (𝕜 × 𝕜)) (i : ι) :=
  fderivWithin 𝕜 f s x (b i)

[Patrick Massot]

This says f is a function from 𝕜 × 𝕜 to F, s is a set in 𝕜 × 𝕜, x a point in 𝕜 × 𝕜 and b a basis of 𝕜 × 𝕜 as a 𝕜-vector space (not necessarily the standard basis). This basis is indexed by the type ι and i is an index. The body of the definition is the derivative of f at x within s evaluated on the basis vector b i if f is differentiable at x within s, and the zero vector otherwise.

[Yury G. Kudryashov]

Note: lineDerivWithin may be a better match (they are equal for Frechet differentiable functions).

[Kiran Singh]

Patrick Massot said:

We still need to understand why you want partial derivatives in Mathlib. What do you plan to do with them?

I'm aiming to add them for theorems such as Clairaut's, and it seems like the code already written for line derivatives could be used for the necessary partial derivative definitions much more easily than what I had originally been planning on. Does that make sense, or would you suggest a different way of approaching partial derivatives/a more urgent topic in multivariable calculus to add?

[Heather Macbeth]

By Clairaut's theorem do you mean the symmetry of second derivatives? This is in mathlib:
https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/Calculus/FDeriv/Symmetric.html

[Kiran Singh]

Yes. I would've thought it would be under a partial derivatives section.
So would partial derivatives still be useful to add, or would it mostly be what line and Fréchet derivatives can do already?

[Yury G. Kudryashov]

Line derivative is a more general version of a partial derivative.

[Yury G. Kudryashov]

OTOH, it makes sense to prove the symmetry of second derivatives without Frechet differentiability assumptions.

[Yury G. Kudryashov]

AFAIR, neither the version that we have, nor the version assuming existence of mixed partial derivatives (we should use lineDerivs or lineDerivWithins) imply the other.

[Patrick Massot]

What is the version not assuming twice differentiable?

[Patrick Massot]

Kiran, maybe we should explicitly say something. Partial derivatives are mostly a teaching trick. This trick has two related goals: avoiding requiring abstract linear algebra understanding in elementary multi-variate calculus, and reducing everything to function from ℝ to ℝ. When people mature partial derivatives mostly disappear.

[Robert Maxton]

:face_with_raised_eyebrow: I'm not even sure that's true in pure mathematics (functional analysis and operator algebras come to mind; taking a derivative with respect to an operator is at any rate much clearer conceptually as a partial derivative than as a line derivative on an continuous-valued basis), but it's definitely not true in mathematical physics, where graduate level stat mech and quantum algebra make heavy use of partial derivatives

[Ruben Van de Velde]

Maybe it would be interesting to show one or a few results from those fields that use partial derivatives, to see what that looks like in practice

[Yury G. Kudryashov]

Patrick Massot said:

What is the version not assuming twice differentiable?

You don't need to assume that $\frac{\partial^2 f}{\partial x^2}$ exists to show $\dfrac{\partial^2 f}{\partial x\partial y}=\dfrac{\partial^2 f}{\partial y\partial x}$, and sometimes it's important.

[Patrick Massot]

My question is: what do you need to assume?

[Yury G. Kudryashov]

One option is to assume that the mixed second derivatives exist and are continuous at the point.

[Yury G. Kudryashov]

It's similar to the situation with the divergence theorem: you can assume that the partial derivatives exist and are integrable (we don't have this version yet), or you can assume that the function is Fréchet differentiable.

[Kiran Singh]

Thanks everyone for the responses.  Since I'm a newcomer to Lean and a high school student, here's my understanding based on what you've said - and feel free to correct me if I've misunderstood anything.  It sounds like line derivatives cover most of what partial derivatives are used for, but there might be some applications (e.g. operator algebras and mathematical physics as Robert mentioned) where partial derivatives would be more useful to use than line derivatives, and it might be helpful to have that definition in Mathlib.

It also sounds like Clairaut's theorem is partially implemented for the case of k=2 (the second derivative) and the definition is for Fréchet differentiable functions, and there might be an opportunity to prove the more general case of Clairaut for arbitrary k and partially differentiable functions.

As you can probably tell, I am looking for first issues to contribute to Mathlib as part of my learning, and am happy to get your guidance on what would be helpful and also do-able as a first contribution. If one or both of these two areas (partial derivative definitions, or generalized Clairaut's theorem) seems like a useful contribution then I'd be happy to try; or if you have other suggestions I'd welcome those too.

Thanks again for all the help here.

[Yury G. Kudryashov]

About Clairaut's theorem: neither of two versions implies the other. In one case you assume Fréchet differentiability but you don't need to assume that the second derivative is continuous; in the other case, you assume that f has lineDeriv in the direction of u near x₀, the derivative has lineDeriv in direction of v near x₀, and the mixed 2nd derivative is continuous.

[Yury G. Kudryashov]

About generalization to higher derivatives: the right way to do it is to claim that iteratedFDeriv of a ContDiff function is a symmetric multilinear function. The proof goes by induction using the existing fact about 2nd derivatives.

[Yury G. Kudryashov]

I don't recommend working on partial derivatives as your first contribution to Mathlib, because the main difficulty is how to make it useful for different types.

[Kiran Singh]

Thank you - that is a helpful explanation of the two versions of Clairaut's theorem, and of how to generalize to higher derivatives. I am also starting to understand your point that the challenge with partial derivatives is how to apply it to different types.

I will keep thinking on and learning about this topic, but based on your feedback I'm thinking of switching my focus to another area. I have seen from https://leanprover-community.github.io/undergrad_todo.html, https://github.com/leanprover-community/mathlib4/pulls and https://github.com/leanprover-community/mathlib4/issues that there seem to be some gaps in linear algebra such as elementary row and column operations, diagonalization and Gaussian elimination, so I plan to switch my focus to those. I looked in https://github.com/leanprover-community/mathlib4/tree/8e8377ed2588a969b36f61cecc9641ac5f4bb7ed/Mathlib/LinearAlgebra/Matrix, as well as in the lists of pull requests and issues and could not see anything underway on these. Assuming that these are good focus areas for a first contribution, I'll start working on them. If you would suggest different areas - or if you'd prefer for me to post my work-in-progress to the "is-there-code-for-x" or "new-members" channels instead, please let me know.

[Johan Commelin]

@Kiran Singh First of all: welcome to the community! It's great to see you working with Lean as a high school student.
That being said, there is a bit of a warning to be made about open items on the undergrad todo list: almost all of them are open because there is some tricky issue involved. So it would be good to start a discussion somewhere on zulip before diving into a formalization project.
Especially if your aim is to contribute to mathlib, there will be demands on the level of generality etc...

[Martin Dvořák]

Here I'd like to repeat the suggestion that we should maybe create another mathematical library on top of Mathlib, such that it would be easy to understand for undergraduates and would focus more on the user experience than on future extensibility.

[Ruben Van de Velde]

But Johan's comment doesn't mean you can't try to formalize something in a less general way to get more experience - just be aware that mathlib requirements are relatively strict

[Patrick Massot]

I think that doing matrix stuff is a good idea. You would need to carefully study what is already in https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Matrix/RowCol.html and https://leanprover-community.github.io/mathlib4_docs/Mathlib/LinearAlgebra/Matrix/Transvection.html and talk to the people who wrote those files, trying to define what you want to state and prove and see whether it can be deduced from more abstract results we already have.

[Patrick Massot]

Still in the undergrad todo list, the “Bilinear and Quadratic Forms Over a Vector Space” probably also has suitable items. This require studying what is missing from https://leanprover-community.github.io/mathlib4_docs/Mathlib/LinearAlgebra/QuadraticForm/Real.html and talking to authors of this file in particular.

[Patrick Massot]

And if you also like analysis, the whole numerical analysis section is full of low hanging fruits that nobody is working on.

[Kiran Singh]

Thank you everyone for the warm welcome to the community and your very helpful guidance on how to contribute. I'll look at those existing linear algebra and numerical analysis files and see which topic seems the most attainable for the moment. Once I've made some progress, I'll come back to the list/committers on the relevant files.

[A.]

Is something like this true/in Mathlib?

example {f : X × Y → Z} {z₀ : X × Y}
    {fx : X × Y → X →L[𝕜] Z} (fx_cont : ContinuousAt fx z₀)
    (hfx : ∀ᶠ z in 𝓝 z₀, HasFDerivAt (fun x => f (x, z.2)) (fx z) z.1)
    {fy : X × Y → Y →L[𝕜] Z} (fy_cont : ContinuousAt fy z₀)
    (hfy : ∀ᶠ z in 𝓝 z₀, HasFDerivAt (fun y => f (z.1, y)) (fy z) z.2) :
    HasStrictFDerivAt f ((fx z₀).coprod (fy z₀)) z₀ := by
  sorry

[Sébastien Gouëzel]

Definitely not true: it's not even true that, if a function has a derivative on a neighborhood of a point, then it is strictly differentiable at the point (on a general field -- matters are different over the reals or the complexes).

[A.]

Well thanks I am not surprised that the specific statement is incorrect, but is there not something like it? And yes I am only concerned with reals

[A.]

I see that it is in fact true with an assumption of [IsRCLikeNormedField 𝕜].

[Oliver Nash]

I recently made an error formalising something written in the language of partial derivatives and it made me wonder if we could do something here. I appreciate the topic has been discussed at length above and elsewhere. Nevertheless I have a proposal and a test case which I hope might be useful.

[Oliver Nash]

First the test case, I think it is worth asking how we would like to express one of my favourite equations, namely the KdV equation:
$\partial_t \phi + \partial^3_x \phi - 6 \phi \partial_x \phi = 0$.

[Oliver Nash]

I claim that all ways to formalise this using Mathlib are currently really gross.

[Oliver Nash]

Here's a possible suggestion for what we might consider to remedy this (assuming my claim is true):

import Mathlib

namespace PartialDerivatives

-- Can we get this to work for any non-trivially normed field and not just `ℝ`?

scoped macro:100 "∂"i:subscript(term) f:term: term =>
  `(fun x ↦ fderiv ℝ $f x (LinearMap.single ℝ _ $(⟨i.raw[0]⟩) 1))

scoped macro:100 "∂"i:subscript(term) f:term j:superscript(term): term =>
  `(fun x ↦ fderiv ℝ $f x (LinearMap.single ℝ _ $(⟨i.raw[0]⟩) 1) $(⟨j.raw[0]⟩))

end PartialDerivatives

variable
  (g : (Fin 2 → ℝ) → (Fin 3 → ℝ))
  (φ : (Fin 2 → ℝ) → ℝ)
  (x : Fin 2 → ℝ)

-- What I'd really like is to be able to write something like:
-- `open scoped PartialDerivatives with (𝕜 := ℝ)`
open scoped PartialDerivatives

#check ∂₀φ
#check ∂₁φ

#check ∂₀g⁰
#check ∂₀g¹
#check ∂₀g²
#check ∂₁g⁰
#check ∂₁g¹
#check ∂₁g²

--  Can we obviate need for parentheses?
#check (∂₁g²) x

-- Test case, we can write the KdV equation in a sane way!
example : (∂₁φ + ∂₀∂₀∂₀φ - 6 * φ * ∂₀φ) = 0 := by
  sorry

[Oliver Nash]

My questions are:

1. How desirable is some version of the above ?
2. Can we do something to avoid the parentheses (mentioned in code comments)?
3. Can we do something fancy to allow any field rather than just hard-coding the reals. E.g., I'd like to be able to write open scoped PartialDerivatives with (𝕜 := ℝ)

[Yaël Dillies]

I think the brackets can be avoided by inserting :arg for the precedence. Untested, but something like

scoped macro:100 "∂"i:subscript(term) f:term: term:arg =>
  `(fun x ↦ fderiv ℝ $f x (LinearMap.single ℝ _ $(⟨i.raw[0]⟩) 1))

[Yuyang Zhao]

I'll write it like this

scoped macro:max "∂" noWs i:subscript(term:max) noWs f:term:max : term =>
  `(fun x ↦ fderiv ℝ $f x (LinearMap.single ℝ _ $(⟨i.raw[0]⟩) 1))

scoped macro:max "∂" noWs i:subscript(term:max) noWs f:term:max noWs j:superscript(term:max) : term =>
  `(fun x ↦ fderiv ℝ $f x (LinearMap.single ℝ _ $(⟨i.raw[0]⟩) 1) $(⟨j.raw[0]⟩))

But it's possible that no noWs or other priority setting would be more appropriate in practice.

[Yuyang Zhao]

Maybe we should just let Lean infer 𝕜 by unification, and use a bracket to specify it when it's needed.

[Patrick Massot]

Do you really need this Fin n stuff? KdV is only in dimension one, right?

[Yury G. Kudryashov]

• Do we want partial derivatives to work for functions from R × R?
• Please use lineDeriv, because in all textbooks partial derivatives don't require Frechet differentiability.

[Patrick Massot]

In many PDE cases this is not enough, you want to start with much weaker notions of differentiability (for instance distribution theory).

[Tomas Skrivan]

I wrote a short introduction to notation for derivatives in SciLean, link (don't try to read anything else as most of it is still work in progress)

For example expressing Euler-Lagrange equation looks like this

variable (L : ℝ → ℝ → ℝ) (x : ℝ → ℝ) (t : ℝ)

#check
  let v := ∂ x
  ∂ (t':=t), (∂ (v':=v t'), L (x t') v') - ∂ (x':=x t), L x' (v t)

Right now I don't have a neat way of doing higher order derivatives, so my attempt at writing down KdV is a bit unsatisfying

variable (φ : ℝ → ℝ → ℝ) (t x : ℝ)
#check (∂ (φ · x) t) + (∂ (∂ (∂ (φ t ·))) x) - (6 * φ t x * ∂ (φ t ·) x)

[Tomas Skrivan]

Oliver Nash said:

My questions are:

1. How desirable is some version of the above ?
2. Can we do something to avoid the parentheses (mentioned in code comments)?

3. Can we do something fancy to allow any field rather than just hard-coding the reals. E.g., I'd like to be able to write open scoped PartialDerivatives with (𝕜 := ℝ)

Yes it is possible to do something like this. See Kyle's answer here.

[Yuyang Zhao]

This solution will add additional instance parameters to lemmas after lean4#4814.

[Yuyang Zhao]

(but this may be resolved by using omit).

[Yuyang Zhao]

But omit makes this notation unusable in proofs.

[Oliver Nash]

Patrick Massot said:

Do you really need this Fin n stuff? KdV is only in dimension one, right?

You're quite right of course. However I claim it is a benefit if a solution to my test case also provides features for higher dimensions. Maybe the counterargument is that we don't want to give people this tool as mostly it is not what they want even when they think it is?

[Oliver Nash]

Yury G. Kudryashov said:

• Do we want partial derivatives to work for functions from R × R?

This would be nice but I don't demand it.

[Oliver Nash]

On the question of docs#lineDeriv I'm not trying to do any new mathematics for partial derivatives. I'm happy for a solution that lives within the well-behaved world of the Frechet derivative. If /when people show up with delicate questions about functions which are non-Frechet differentiable they'll have to do their own work.

[Oliver Nash]

Finally thanks to @Yuyang Zhao and @Tomas Skrivan for the notation help. It's still not clear to me if my proposal is a good idea, but these are certainly helpful.

[Oliver Nash]

I'm also delighted to have an excuse to look at SciLean again!

[Wuyang]

Dear all: May I have a follow-up relevant question: does mathlib4 support integration over multi-variable functions?

[Luigi Massacci]

Yes of course

[Yury G. Kudryashov]

Yury G. Kudryashov said:

One option is to assume that the mixed second derivatives exist and are continuous at the point.

@Patrick Massot Here is what I meant: #24129 (the last lemma in the new file; not ready for review yet).