partial derivative of a vector field

Stream: new members

[Carefree]

Hello everyone, I am a lean beginner. I want to define a vector space V=(v1 (x, t), v2 (x, t)) and find the partial derivative of V with respect to x, t. I checked Mathlib in the mathlib library Analysis.Calculus.FDeriv.Basic， But I still can't get the answer.

[Riccardo Brasca]

What is the derivative of a vector space?

[Carefree]

This vector space has no specific form, but mathematically speaking, dV\dx=(dV\dv1)(dv1\dx)+(dV\dv2)(dv2\dx)

[Johan Commelin]

Do you mean vector field?

[Carefree]

yes!

[Tomas Skrivan]

This question comes up over and over and the answer is always bla bla .. use fderiv and single somehow. So I wrote a little guide how to go about this that we can use for future reference. Any suggestions on how to improve this are welcome.

[Tomas Skrivan]

Writing Partial Derivatives in Lean

Quick Answer

Given a function $f : \mathbb{R}^n \to \mathbb{R}^m$, how do you write $\frac{\partial f}{\partial x_i}$ in Lean?

Lean represents $\mathbb{R}^n$ as EuclideanSpace ℝ (Fin n). You can express partial derivatives using the fderiv function and the basis vector single i 1:

import Mathlib

variable {n m : ℕ} (f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin m))
  (x : EuclideanSpace ℝ (Fin n)) (i : Fin n)

open EuclideanSpace
-- ∂f/∂xᵢ at x
#check fderiv ℝ f x (single i 1)

The fderiv ℝ f x expression gives the full Jacobian of f, which is a linear map $L(\mathbb{R}^n, \mathbb{R}^m)$. Evaluating this map on the basis vector $e_i$ (represented by single i (1 : ℝ)) gives the partial derivative.

---

Longer Answer

There are two primary approaches to handling partial derivatives in Lean, depending on whether the input dimension is variable or fixed.

1. Functions Over an n-Dimensional Space

If you work with a general function $f : \mathbb{R}^n \to \mathbb{R}^m$, use the approach described above with fderiv and single.

2. Functions with Fixed Arguments

For functions with a known number of arguments, like $f(x, y)$, it's often better to define f as ℝ → ℝ → EuclideanSpace ℝ (Fin m) rather than EuclideanSpace ℝ (Fin 2) → EuclideanSpace ℝ (Fin m). Here is how to compute partial derivatives with respect to each argument:

import Mathlib

variable {m : ℕ} (f : ℝ → ℝ → EuclideanSpace ℝ (Fin m)) (x y : ℝ)

open EuclideanSpace
-- ∂f/∂x at (x,y)
#check fderiv ℝ (fun x' => f x' y) x 1
-- ∂f/∂y at (x,y)
#check fderiv ℝ (fun y' => f x y') y 1

To actually prove anything about these derivative you will need to state that f is differentiable in x and y. The way to state this is differentiability of f in (x,y) is

- (hf : Differentiable ℝ (fun (x,y) => f x y))
- (hf : Differentiable ℝ (fun xy : ℝ×ℝ => f xy.1 xy.2)
- (hf : Differentiable ℝ ↿f)
they are syntactic variants of the same thing. Pick one you prefer writing. The first one does not work with variable though.

Requiring differentiability in (x,y) gives you differentiability in x and differentiability in y

import Mathlib

variable {m : ℕ} (f : ℝ → ℝ → EuclideanSpace ℝ (Fin m)) (x y : ℝ)

example (hf : Differentiable ℝ ↿f) :
    Differentiable ℝ (fun x => f x y) := by fun_prop

example (hf : Differentiable ℝ (fun (x,y) => f x y)) :
    Differentiable ℝ (fun y => f x y) := by fun_prop

Mixed Approach

When working with functions that mix fixed and variable dimensions (e.g., $f(x, y)$ where $x \in \mathbb{R}^n$ and $y \in \mathbb{R}^m$), you can apply fderiv to each argument separately:

import Mathlib

variable {n m k : ℕ} (f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin k))
  (x y) (i : Fin n) (j : Fin m)

open EuclideanSpace
-- ∂f/∂xᵢ at (x,y)
#check fderiv ℝ (fun x' => f x' y) x (single i 1)
-- ∂f/∂yⱼ at (x,y)
#check fderiv ℝ (fun y' => f x y') y (single j 1)

---

Special Cases

1. When the Input is ℝ (deriv)

If the function's input is ℝ, you can use deriv as a simpler alternative to fderiv:

import Mathlib

variable {n : ℕ}
  (f : ℝ → EuclideanSpace ℝ (Fin n))
  (g : ℝ → ℝ → EuclideanSpace ℝ (Fin n))
  (x y : ℝ)

open EuclideanSpace
-- d f / d x at x
#check deriv f x
-- Equivalent to fderiv
example : deriv f x = fderiv ℝ f x 1 := by rfl
-- ∂ g / ∂ x at (x,y)
#check deriv (fun x' => g x' y) x
-- ∂ g / ∂ y at (x,y)
#check deriv (fun y' => g x y') y

2. When the Output is ℝ (gradient)

If the function's output is ℝ, you may want the gradient (a vector of all partial derivatives). For this, use the gradient function:

import Mathlib

variable {n m : ℕ}
  (f : EuclideanSpace ℝ (Fin n) → ℝ)
  (g : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin m) → ℝ)
  (x y)

open EuclideanSpace
-- ∇ₓ f at x
#check gradient f x
-- ∇ₓ g at (x,y)
#check gradient (fun x' => g x' y) x
-- ∇_y g at (x,y)
#check gradient (fun y' => g x y') y

[Johan Commelin]

Very nice! @Tomas Skrivan do you want to post this somewhere a bit more permanent? The community blog maybe?

[Tomas Skrivan]

Johan Commelin said:

Very nice! Tomas Skrivan do you want to post this somewhere a bit more permanent? The community blog maybe?

Yes that would be nice to make it more discoverable and permanent.

[Tomas Skrivan]

Ohh I should also add that for multiple arguments you show formulate differentiability as (hg : Differentiable ℝ (fun (x,y) => g x y)) or (hg : Differentiable ℝ ↿g)

[Jireh Loreaux]

I might suggest a separate page on the website, rather than a blog post.

[Tomas Skrivan]

And finally

Writing all this is such a chore ...

I hear you! You can define custom notation:

import Mathlib

macro "ℝ[" n:term "]" : term => `(EuclideanSpace ℝ (Fin $n))
macro "∂[" i:term "]" : term => `(fun f x => fderiv ℝ f x (EuclideanSpace.single $i (1:ℝ)))

variable {m n k : ℕ} (f : ℝ[n] → ℝ[m] → ℝ[k]) (x : ℝ[n]) (y : ℝ[m])
   (i : Fin n) (j : Fin m)

-- `∂ f / ∂ xᵢ` at `(x,y)`
#check ∂[i] (f · y) x

-- `∂ f / ∂ yⱼ` at `(x,y)`
#check ∂[j] (f x ·) y

Maybe stabilizing a notation like this would be a good idea and would make partial derivatives a lot more approachable to new comers.

[Tomas Skrivan]

Jireh Loreaux said:

I might suggest a separate page on the website, rather than a blog post.

Anyone who knows how to do it and can, please feel free to do so.

[Tomas Skrivan]

The stress test of a partial derivative notation is the Euler-Lagrange equation (which highlights how bad standard notation for partial derivatives actually is)

$\frac{\partial L}{\partial q^i}(t,\boldsymbol q(t),\dot{\boldsymbol q}(t))-\frac{\mathrm{d}}{\mathrm{d}t}\frac{\partial L}{\partial \dot q^i}(t,\boldsymbol q(t),\dot{\boldsymbol q}(t)) = 0$

import Mathlib

macro "ℝ[" n:term "]" : term => `(EuclideanSpace ℝ (Fin $n))
macro "∂[" i:term "]" : term => `(fun f x => fderiv ℝ f x (EuclideanSpace.single $i (1:ℝ)))
prefix:max " ∇ " => gradient
prefix:max " 𝕕 " => deriv

variable (L : ℝ → ℝ[n] → ℝ[n] → ℝ) (x : ℝ → ℝ[n])

-- Euler-Lagrange equation
-- ∇ₓ L - d/dt (∇ᵥ L)  = 0
#check ∀ t, ∇ (L t · (𝕕 x t)) (x t) - 𝕕 (fun t' => ∇ (L t' (x t') ·) (𝕕 x t')) t  = 0

[Tomas Skrivan]

I would suggest custom elaborator for R^[n] for EuclideanSpace R n

It has to be an elaborator to disambiguate few cases:

Does R elaborate as type?

• Yes - Does n elaborate as Nat?
  • Yes: return EuclideanSpace R (Fin n)
  • No: return EuclideanSpace R n
• No - we want iterated function composition
  • return Nat.iterate R n

[Tomas Skrivan]

$\mathbb{R}^n$ and $\mathbb{C}^n$ are such central objects in mathematics and they deserve better than EuclideanSpace ℝ (Fin n).

[Tomas Skrivan]

Here I have a custom elaborator that does that and also supports things like ℝ^[m,n] ==> EucliedeanSpace ℝ (Fin m × Fin n). In SciLean, I expand to DataArrayN rather than to EucliedeanSpace because I want to work with an actual arrays holding data but that should be an easy change.

[Eric Wieser]

Another option would be something like

import Mathlib

open Lean Meta Elab Term Macro TSyntax PrettyPrinter.Delaborator SubExpr
open Mathlib.Tactic (superscriptTerm)

syntax (name := superEuc) term noWs superscriptTerm : term
macro_rules | `($R:term$n:superscript) => `(EuclideanSpace $R (Fin $n:term))

/-- Unexpander for the `!₂[x, y, ...]` notation. -/
@[app_delab EuclideanSpace]
def EuclideanSpace.delabNotation : Delab :=
  whenNotPPOption getPPExplicit <| whenPPOption getPPNotation <| withOverApp 2 do
    let R : Term ← withAppFn <| withAppArg delab
    let n : Term ← withAppArg do
      let_expr Fin _ := ← getExpr | failure
      withAppArg delab
    -- to be conservative, only allow superscripts which are numerals
    guard <| n matches `($_:num)
    `($R:term$n:superscript)

#check EuclideanSpace ℝ (Fin 2) -- ℝ²
#check ℝ² -- ℝ²

[Tomas Skrivan]

Even better! I think having both would be good idea as the superscript is not as flexible but having ℝⁿ would be really nice.

[Kevin Buzzard]

Whenever I've figured out "how to do standard mathy thing using mathlib" I've added it as a section to my course notes. This feels like it would be perfect there; the material could be written over several files, with some sorries which the user could fill in. It could also go in Mathematics In Lean.

[Sébastien Gouëzel]

An issue with standard notations for $\R^n$ and $\mathbb{C}^n$ is that it will encourage people to write things just in this setting, while most of the time it is better to write things in a general Euclidean space (or even in a general normed space) -- otherwise the results won't apply to product spaces, or to infinite dimensional spaces, or whatever. (The best approach is probably to teach people that they shouldn't use partial derivatives :-)

[Tomas Skrivan]

Sébastien Gouëzel said:

An issue with standard notations for $\R^n$ and $\mathbb{C}^n$ is that it will encourage people to write things just in this setting, while most of the time it is better to write things in a general Euclidean space (or even in a general normed space) -- otherwise the results won't apply to product spaces, or to infinite dimensional spaces, or whatever. (The best approach is probably to teach people that they shouldn't use partial derivatives :-)

I agree and disagree with this. Many times people come here and ask for partial derivatives, we tell them to write abomination like

variable {𝕜} [NontriviallyNormedField 𝕜]
  {X} [NormedAddCommGroup X] [NormedSpace 𝕜 X]
  {Y} [NormedAddCommGroup Y] [NormedSpace 𝕜 Y]

variable (f : X → Y)

#check fderiv 𝕜 f

and we never hear from them ever again.

We need to meet people where they are at! Show them how to do the familiar thing and once they write a PR to mathlib we tell them how to generalize it to the mess above. Which should be easy or they are doing something specific to  $\mathbb{R}^n$.

[Tomas Skrivan]

Sébastien Gouëzel said:

otherwise the results won't apply to product spaces

Well this is a stupid design choice of mathlib that product space and arrow spaces(over Fintype) do not form InnerProductSpace. My suggestion would be to make InnerProductSpace weaker, only require topological equivalence between the norm and norm induced by the inner product. To recover original InnerProductSpace we would add a Propclass saying that they are actually equal. With this setup up we can equip Prod and _ → _ with InnerProductSpace. Is that correct? Or am I missing something?

[Eric Wieser]

I think this increases the chance of a user being surprised by norm being the wrong thing

[Eric Wieser]

Today they'll usually reach for inner shortly after norm, and then discover that the instance is missing, and they that they should be using WithLp instead

[Johan Commelin]

@Tomas Skrivan But if you prove something for $\R^n$, then it won't apply to $\R^n \times \R^m$, right? That has nothing to do with design choices in mathlib.

[Tomas Skrivan]

Eric Wieser said:

I think this increases the chance of a user being surprised by norm being the wrong thing

Is that really worse than having to write WithLp everywhere?

[Eric Wieser]

My point is that they still have to do that, but now only when they take the norm of a vector

[Eric Wieser]

I think making EuclideanSpace ℝ (Fin n) easier to write is a good thing, because otherwise people just write Fin n -> ℝ and end up in worse trouble

[Tomas Skrivan]

Maybe all my arguments are mainly from a person writing tactics. Not having product and arrow types makes it a lot harder to the point where I just gave up. If you create a new proposition on InnerProductSpacethen fun_prop will not work for it. The same way my differentiation tactic does not work for gradient.

[Eric Wieser]

Johan Commelin said:

Tomas Skrivan But if you prove something for $\R^n$, then it won't apply to $\R^n \times \R^m$, right? That has nothing to do with design choices in mathlib.

if by $\R^n \times \R^m$ you mean (Fin n → ℝ) × (Fin m → ℝ), then writing the general abstract version doesn't help you at all. You have to write WithLp 2 (WithLp 2 (Fin n → ℝ) × WithLp 2 (Fin m → ℝ)) in order for it to be an instantiation of the general case, which would be much less bad with the proposed notation as WithLp 2 (ℝ^[n] × ℝ^[m]).

[Tomas Skrivan]

Johan Commelin said:

Tomas Skrivan But if you prove something for $\R^n$, then it won't apply to $\R^n \times \R^m$, right? That has nothing to do with design choices in mathlib.

That is correct, but I do not see the problem of showing new commers how to do the stuff over familiar $\R^n$ first and then generalize it to abstract space.

[Anatole Dedecker]

Eric Wieser said:

Johan Commelin said:

Tomas Skrivan But if you prove something for $\R^n$, then it won't apply to $\R^n \times \R^m$, right? That has nothing to do with design choices in mathlib.

if by $\R^n \times \R^m$ you mean (Fin n → ℝ) × (Fin m → ℝ), then writing the general abstract version doesn't help you at all. You have to write WithLp 2 (WithLp 2 (Fin n → ℝ) × WithLp 2 (Fin m → ℝ)) in order for it to be an instantiation of the general case, which would be much less bad with the proposed notation as WithLp 2 (ℝ^[n] × ℝ^[m]).

I think Johan's point is that you should only have abstract finite normed spaces / inner product spaces, eventually with chosen bases, and never any concrete one.

[Eric Wieser]

Isn't part of mathlib's job to provide instances for concrete types so that users can work with them and leverage general lemmas?

[Eric Wieser]

Is the claim that EuclideanSpace shouldn't exist at all?

[Anatole Dedecker]

Well yes, it should work, but then you have to be aware that a bunch of things aren't $\mathbb{R}^n$ anyways, wether it means Fin n -> \R or EuclideanSpace \R (Fin n)

[Johan Commelin]

My only point was that I didn't understand this response.
Tomas Skrivan said:

Sébastien Gouëzel said:

otherwise the results won't apply to product spaces

Well this is a stupid design choice of mathlib that product space and arrow spaces(over Fintype) do not form InnerProductSpace. My suggestion would be to make InnerProductSpace weaker, only require topological equivalence between the norm and norm induced by the inner product. To recover original InnerProductSpace we would add a Propclass saying that they are actually equal. With this setup up we can equip Prod and _ → _ with InnerProductSpace. Is that correct? Or am I missing something?

[Eric Wieser]

I think the first part of that comment is along the lines of my message above

[Tomas Skrivan]

Johan Commelin said:

My only point was that I didn't understand this response.
Tomas Skrivan said:

Sébastien Gouëzel said:

otherwise the results won't apply to product spaces

Well this is a stupid design choice of mathlib that product space and arrow spaces(over Fintype) do not form InnerProductSpace. My suggestion would be to make InnerProductSpace weaker, only require topological equivalence between the norm and norm induced by the inner product. To recover original InnerProductSpace we would add a Propclass saying that they are actually equal. With this setup up we can equip Prod and _ → _ with InnerProductSpace. Is that correct? Or am I missing something?

In that response I misunderstood Sébastien, he clearly meant what you pointed out. Not having InnerProductSpace on product spaces is a pet peeve of mine and anytime I see something resembling it I start ranting. Sorry for that.

[Johan Commelin]

Got it. No worries.

[Joseph Myers]

EuclideanSpace should exist, but mainly for use of leaf code rather than in mathlib itself. (My suggested IMO problem statement formalization conventions say to use it only for problems that explicitly refer to coordinates, such as IMO 2016 P3, and to use more general type classes for problems not explicitly involving coordinates or a choice of origin.)

[Eric Wieser]

In practice I feel like doing things in the mathematically correct generality puts you far more at risk of mathlib letting you down. For instance, docs#convexHull is obviously an affine notion, but it only works today for vector spaces. Of course you can specialize a little bit (from affine to vector spaces) rather than all the way (from affine spaces to euclidean space), but it's much easier to come up with a proof for a concrete statement using abstract lemmas, then generalize it, than it is to write the abstract version and repeatedly trip over absent generality elsewhere in mathlib.

[Yaël Dillies]

I am unfortunately forced to agree. Once the convexity refactor actually happens, this should be less of an issue though

[Kevin Buzzard]

I don't experience this in commutative algebra: everything is set up in the correct generality there; in fact it is often the case that one finds the result one needs in mathlib in far more generality than needed. This phenomenon might be topic-dependent.

[Kevin Buzzard]

(PS I edited the topic; it was driving me nuts that we were having an interesting conversation in a thread with a manifestly nonsense title because of the typo which was identified many messages ago)

[Yaël Dillies]

This is definitely topic-dependent

[Carefree]

Thanks so much!To be honest, as a beginner, I cannot understand most of the above. But I will continue to learn. Thank you!!