From 1580d744c40dcbd9b3c3f35110a338259050fc5f Mon Sep 17 00:00:00 2001 From: Tomas Skrivan Date: Thu, 26 Feb 2026 14:43:20 +0100 Subject: [PATCH 1/3] partial derivatives guide --- templates/theories.md | 1 + templates/theories/partial_derivatives.md | 148 ++++++++++++++++++++++ 2 files changed, 149 insertions(+) create mode 100644 templates/theories/partial_derivatives.md diff --git a/templates/theories.md b/templates/theories.md index b56f7f33ba..2746b53355 100644 --- a/templates/theories.md +++ b/templates/theories.md @@ -7,3 +7,4 @@ The following document some theories spanning multiple files. * [Linear algebra](theories/linear_algebra.html) * [The natural numbers](theories/naturals.html) * [Topological, uniform and metric spaces](theories/topology.html) +* [Partial Derivatives](theories/partial_derivatives.html) diff --git a/templates/theories/partial_derivatives.md b/templates/theories/partial_derivatives.md new file mode 100644 index 0000000000..83073689c7 --- /dev/null +++ b/templates/theories/partial_derivatives.md @@ -0,0 +1,148 @@ +# Maths in Lean: partial derivatives + +Where are partial derivatives in Mathlib? There is only Fréchet derivative `fderiv` which might be surprising but it is sufficient to express all possible derivatives. + +### 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`: + +```lean +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: + +```lean +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 derivatives you will need to state that `f` is differentiable in `x` and `y`. The ways to state differentiability of `f` in `(x,y)` are: + - `(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`: +```lean +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 +``` + +#### 3. 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: + +```lean +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`: + +```lean +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: + +```lean +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 +``` + + +### Writing all this is such a chore ... + +I hear you! You can define custom notation: +```lean +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 +``` From a8287344de18051207aaba045c4359ccdee2a555 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tom=C3=A1=C5=A1=20Sk=C5=99ivan?= Date: Thu, 26 Feb 2026 15:15:52 +0100 Subject: [PATCH 2/3] Apply suggestions from code review Looks good Co-authored-by: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com> --- templates/theories/partial_derivatives.md | 36 ++++++++++++++--------- 1 file changed, 22 insertions(+), 14 deletions(-) diff --git a/templates/theories/partial_derivatives.md b/templates/theories/partial_derivatives.md index 83073689c7..97f1aad7c7 100644 --- a/templates/theories/partial_derivatives.md +++ b/templates/theories/partial_derivatives.md @@ -15,6 +15,7 @@ variable {n m : ℕ} (f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin (x : EuclideanSpace ℝ (Fin n)) (i : Fin n) open EuclideanSpace + -- ∂f/∂xᵢ at x #check fderiv ℝ f x (single i 1) ``` @@ -39,15 +40,16 @@ 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 +#check fderiv ℝ (f · y) x 1 -- ∂f/∂y at (x,y) -#check fderiv ℝ (fun y' => f x y') y 1 +#check fderiv ℝ (f x ·) y 1 ``` To actually prove anything about these derivatives you will need to state that `f` is differentiable in `x` and `y`. The ways to state differentiability of `f` in `(x,y)` are: - - `(hf : Differentiable ℝ (fun (x,y) => f x y))` - - `(hf : Differentiable ℝ (fun xy : ℝ×ℝ => f xy.1 xy.2)` + - `(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. @@ -58,10 +60,10 @@ import Mathlib variable {m : ℕ} (f : ℝ → ℝ → EuclideanSpace ℝ (Fin m)) (x y : ℝ) example (hf : Differentiable ℝ ↿f) : - Differentiable ℝ (fun x => f x y) := by fun_prop + Differentiable ℝ (f · y) := by fun_prop -example (hf : Differentiable ℝ (fun (x,y) => f x y)) : - Differentiable ℝ (fun y => f x y) := by fun_prop +example (hf : Differentiable ℝ (fun (x, y) ↦ f x y)) : + Differentiable ℝ (f x ·) := by fun_prop ``` #### 3. Mixed Approach @@ -75,10 +77,11 @@ variable {n m k : ℕ} (f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (F (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) +#check fderiv ℝ (f · y) x (single i 1) -- ∂f/∂yⱼ at (x,y) -#check fderiv ℝ (fun y' => f x y') y (single j 1) +#check fderiv ℝ (f x ·) y (single j 1) ``` ### Special Cases @@ -96,14 +99,16 @@ variable {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 +#check deriv (g · y) x -- ∂ g / ∂ y at (x,y) -#check deriv (fun y' => g x y') y +#check deriv (g x ·) y ``` #### 2. When the Output is ℝ (`gradient`) @@ -119,12 +124,15 @@ variable {n m : ℕ} (x y) open EuclideanSpace + -- ∇ₓ f at x #check gradient f x + -- ∇ₓ g at (x,y) -#check gradient (fun x' => g x' y) x +#check gradient (g · y) x + -- ∇_y g at (x,y) -#check gradient (fun y' => g x y') y +#check gradient (g x ·) y ``` @@ -134,7 +142,7 @@ I hear you! You can define custom notation: ```lean import Mathlib -macro "ℝ[" n:term "]" : term => `(EuclideanSpace ℝ (Fin $n)) +local macro:max "ℝ" noWs n:superscript(term) : term => `(EuclideanSpace ℝ (Fin $(⟨n.raw[0]⟩))) 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]) From f7dbd7a3bfb4a074b63164510da4e2027df50841 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tom=C3=A1=C5=A1=20Sk=C5=99ivan?= Date: Fri, 27 Feb 2026 07:55:24 +0100 Subject: [PATCH 3/3] Update templates/theories/partial_derivatives.md Co-authored-by: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com> --- templates/theories/partial_derivatives.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/templates/theories/partial_derivatives.md b/templates/theories/partial_derivatives.md index 97f1aad7c7..6c0ad6588a 100644 --- a/templates/theories/partial_derivatives.md +++ b/templates/theories/partial_derivatives.md @@ -145,7 +145,7 @@ import Mathlib local macro:max "ℝ" noWs n:superscript(term) : term => `(EuclideanSpace ℝ (Fin $(⟨n.raw[0]⟩))) 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]) +variable {m n k : ℕ} (f : ℝⁿ → ℝᵐ → ℝᵏ) (x : ℝⁿ) (y : ℝᵐ) (i : Fin n) (j : Fin m) -- `∂ f / ∂ xᵢ` at `(x,y)`