feat(Analysis/Matrix): add Jacobian matrix for matrix-valued functions by hdmkindom · Pull Request #33786 · leanprover-community/mathlib4

hdmkindom · 2026-01-09T05:13:25Z

This PR introduces the Jacobian matrix for matrix-valued functions F : Matrix m n 𝕜 → Matrix p q 𝕜.

The Jacobian matrix jacobianMatrix F X at point X is indexed by (p × q) × (m × n), where each entry represents the partial derivative with respect to a basis element. To handle instance-mismatch issues with matrix norms, we use local Frobenius norm instances.

This PR adds the new file:
'Analysis/Matrix/Jacobian.lean'

Main definitions

jacobianMatrix F X: The Jacobian matrix at point X, defined by jacobianMatrix F X (i, k) (j, l) = (fderiv ℝ F X (Matrix.single j l 1)) i k

Main theorems

fderiv_eq_jacobian_mul: Express the Fréchet derivative as a contraction with the Jacobian
jacobianMatrix_comp: Chain rule for Jacobian matrices
jacobianMatrix_linear, jacobianMatrix_id, jacobianMatrix_const: Basic properties
jacobianMatrix_add, jacobianMatrix_smul: Linearity properties

github-actions · 2026-01-09T05:14:34Z

PR summary 0b31fd4983

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.Analysis.Matrix.Jacobian` (new file)	2168

Declarations diff

+ fderiv_eq_jacobian_mul
+ jacobianMatrix
+ jacobianMatrix_add
+ jacobianMatrix_comp
+ jacobianMatrix_const
+ jacobianMatrix_eq_fderiv_basis
+ jacobianMatrix_id
+ jacobianMatrix_linear
+ jacobianMatrix_smul
+ matrix_fderiv_comp

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.

No changes to strong technical debt.

No changes to weak technical debt.

jcommelin · 2026-02-17T15:06:00Z

mkdir Analysis/Matrix/Jacobian.lean

Please remove this line from the PR description. If you meant to indicate that you are adding a new file, please say that. mkdir is a command to create new directories.

jcommelin · 2026-02-17T15:10:56Z

+    (F : Matrix m n ℝ → Matrix p q ℝ)
+    (G : Matrix p q ℝ → Matrix r s ℝ)
+    (X : Matrix m n ℝ)


Can you extract these into variable statement as well.

Thanks, I have moved these repeated arguments into variable declarations. I have removed that line from the PR description and rephrased it as a new file addition.

jcommelin · 2026-02-17T15:11:48Z

+`J[(i, k), (j, l)] = (fderiv ℝ F X (Matrix.single j l 1)) i k`.
+-/
+noncomputable def jacobianMatrix
+    (F : Matrix m n ℝ → Matrix p q ℝ) (X : Matrix m n ℝ) :


Can you generalize this from ℝ to non-trivially normed fields?

Thanks for the suggestion. I have generalized the definitions and theorems from ℝ to a nontrivially normed field where possible.

erdOne · 2026-02-17T15:07:43Z

+noncomputable def jacobianMatrix
+    (F : Matrix m n ℝ → Matrix p q ℝ) (X : Matrix m n ℝ) :
+    Matrix (p × q) (m × n) ℝ :=
+  fun (i, k) (j, l) => (fderiv ℝ F X (Matrix.single j l (1 : ℝ))) i k


Suggested change

fun (i, k) (j, l) => (fderiv ℝ F X (Matrix.single j l (1 : ℝ))) i k

fun (i, k) (j, l) => fderiv ℝ F X (Matrix.single j l (1 : ℝ)) i k

Thanks, I have applied this simplification.

erdOne · 2026-02-17T15:18:47Z

+  -- unfold Jacobian entries
+  simp only [jacobianMatrix_eq_fderiv_basis]
+  -- decompose `H` into the standard basis
+  have h_decomp : H = ∑ j : m, ∑ l : n, Matrix.single j l (H j l) := by
+    simpa using (Matrix.matrix_eq_sum_single H)
+  conv_lhs => rw [h_decomp]
+  -- linearity through sums
+  simp only [map_sum]
+  -- pull out entries `(i, k)`
+  rw [Finset.sum_apply, Finset.sum_apply]
+  refine Finset.sum_congr rfl ?_
+  intro j _
+  rw [Finset.sum_apply, Finset.sum_apply]
+  refine Finset.sum_congr rfl ?_
+  intro l _
+  -- rewrite `single j l (H j l)` as a scalar multiple of `single j l 1`
+  have hs : Matrix.single j l (H j l) = (H j l) • Matrix.single j l (1 : ℝ) := by
+    simp only [smul_single, smul_eq_mul, mul_one]
+  -- apply `map_smul` and commute the scalar
+  calc
+    (fderiv ℝ F X) (Matrix.single j l (H j l)) i k
+        = (fderiv ℝ F X) ((H j l) • Matrix.single j l (1 : ℝ)) i k := by
+            rw [hs]
+    _ = (H j l) * (fderiv ℝ F X) (Matrix.single j l (1 : ℝ)) i k := by
+            rw [map_smul, smul_apply, smul_eq_mul]
+    _ = (fderiv ℝ F X) (Matrix.single j l (1 : ℝ)) i k * H j l := by
+            simp [mul_comm]


I think you can try to utilize simp more.

Suggested change

-- unfold Jacobian entries

simp only [jacobianMatrix_eq_fderiv_basis]

-- decompose `H` into the standard basis

have h_decomp : H = ∑ j : m, ∑ l : n, Matrix.single j l (H j l) := by

simpa using (Matrix.matrix_eq_sum_single H)

conv_lhs => rw [h_decomp]

-- linearity through sums

simp only [map_sum]

-- pull out entries `(i, k)`

rw [Finset.sum_apply, Finset.sum_apply]

refine Finset.sum_congr rfl ?_

intro j _

rw [Finset.sum_apply, Finset.sum_apply]

refine Finset.sum_congr rfl ?_

intro l _

-- rewrite `single j l (H j l)` as a scalar multiple of `single j l 1`

have hs : Matrix.single j l (H j l) = (H j l) • Matrix.single j l (1 : ℝ) := by

simp only [smul_single, smul_eq_mul, mul_one]

-- apply `map_smul` and commute the scalar

calc

(fderiv ℝ F X) (Matrix.single j l (H j l)) i k

= (fderiv ℝ F X) ((H j l) • Matrix.single j l (1 : ℝ)) i k := by

rw [hs]

_ = (H j l) * (fderiv ℝ F X) (Matrix.single j l (1 : ℝ)) i k := by

rw [map_smul, smul_apply, smul_eq_mul]

_ = (fderiv ℝ F X) (Matrix.single j l (1 : ℝ)) i k * H j l := by

simp [mul_comm]

-- decompose `H` into the standard basis

have h_decomp : H = ∑ j : m, ∑ l : n, H j l • Matrix.single j l 1 := by

simpa using Matrix.matrix_eq_sum_single H

conv_lhs => rw [h_decomp]

simp [-smul_single, Matrix.sum_apply, mul_comm]

Thanks, I have simplified this proof using simp as suggested.

erdOne · 2026-02-17T15:22:35Z

+@[simp]
+theorem jacobianMatrix_eq_fderiv_basis
+    (F : Matrix m n ℝ → Matrix p q ℝ) (X : Matrix m n ℝ)
+    (i : p) (k : q) (j : m) (l : n) :
+    jacobianMatrix F X (i, k) (j, l) =
+      (fderiv ℝ F X) (Matrix.single j l (1 : ℝ)) i k := by
+  rfl


Suggested change

@[simp]

theorem jacobianMatrix_eq_fderiv_basis

(F : Matrix m n ℝ → Matrix p q ℝ) (X : Matrix m n ℝ)

(i : p) (k : q) (j : m) (l : n) :

jacobianMatrix F X (i, k) (j, l) =

(fderiv ℝ F X) (Matrix.single j l (1 : ℝ)) i k := by

rfl

@[simp]

theorem jacobianMatrix_eq_fderiv_basis

(F : Matrix m n ℝ → Matrix p q ℝ) (X : Matrix m n ℝ)

(ik : p × q) (jl : m × n) :

jacobianMatrix F X ik jl = fderiv ℝ F X (Matrix.single jl.1 jl.2 1) ik.1 ik.2 := rfl

The left hand side is syntactically more general when you do not assume it is applied to arguments of the form (i, k) and applies more easily.

rfl as a proof is better than by rfl because the former proof registers the lemma as a dsimp lemma.

Thanks, I have changed this lemma to use pair arguments and proved it by rfl.

erdOne · 2026-02-17T15:23:47Z

+      if i = j ∧ k = l then (1 : ℝ) else 0 := by
+  classical
+  simp only [jacobianMatrix, fderiv_id, ContinuousLinearMap.coe_id', id_eq]
+  by_cases h : (i = j ∧ k = l)
+  · rcases h with ⟨rfl, rfl⟩
+    simp only [Matrix.single_apply_same]
+    simp only [and_self, ↓reduceIte]
+  · have h' : ¬ (j = i ∧ l = k) := by
+      intro hji
+      apply h
+      exact ⟨hji.1.symm, hji.2.symm⟩
+    simp only [h, Matrix.single_apply_of_ne (i := j) (j := l) (c := (1 : ℝ)) (i' := i) (j' := k) h']
+    simp only [↓reduceIte]


Suggested change

if i = j ∧ k = l then (1 : ℝ) else 0 := by

classical

simp only [jacobianMatrix, fderiv_id, ContinuousLinearMap.coe_id', id_eq]

by_cases h : (i = j ∧ k = l)

· rcases h with ⟨rfl, rfl⟩

simp only [Matrix.single_apply_same]

simp only [and_self, ↓reduceIte]

· have h' : ¬ (j = i ∧ l = k) := by

intro hji

apply h

exact ⟨hji.1.symm, hji.2.symm⟩

simp only [h, Matrix.single_apply_of_ne (i := j) (j := l) (c := (1 : ℝ)) (i' := i) (j' := k) h']

simp only [↓reduceIte]

if i = j ∧ k = l then 1 else 0 := by

simp [Matrix.single_apply]

grind

Thanks for the suggestion, I have simplified this proof using simp and grind. I have a small style question: in this kind of proof, is a plain simp preferred, or would simp only [...] be better? I was concerned that using plain simp might make the proof less explicit and therefore slightly less readable.

erdOne · 2026-02-17T15:24:08Z

+  classical
+  simp only [jacobianMatrix, fderiv_fun_const, Pi.zero_apply, ContinuousLinearMap.zero_apply,
+    zero_apply]


Suggested change

classical

simp only [jacobianMatrix, fderiv_fun_const, Pi.zero_apply, ContinuousLinearMap.zero_apply,

zero_apply]

simp

Thanks, I have simplified this proof using simp only [jacobianMatrix_eq_fderiv_basis, fderiv_fun_const, Pi.zero_apply, ContinuousLinearMap.zero_apply, zero_apply].

erdOne · 2026-02-17T15:25:00Z

+      jacobianMatrix F X (i, k) (j, l) + jacobianMatrix G X (i, k) (j, l) := by
+  unfold jacobianMatrix
+  have h_add : (fun Y => F Y + G Y) = fun Y => (F + G) Y := rfl
+  rw [h_add]
+  rw [fderiv_add hF hG]
+  simp only [ContinuousLinearMap.add_apply]
+  rfl


Suggested change

jacobianMatrix F X (i, k) (j, l) + jacobianMatrix G X (i, k) (j, l) := by

unfold jacobianMatrix

have h_add : (fun Y => F Y + G Y) = fun Y => (F + G) Y := rfl

rw [h_add]

rw [fderiv_add hF hG]

simp only [ContinuousLinearMap.add_apply]

rfl

jacobianMatrix F X (i, k) (j, l) + jacobianMatrix G X (i, k) (j, l) := by

simp [fderiv_fun_add, *]

Thanks, I have simplified this proof using simp [fderiv_fun_add, *].

erdOne · 2026-02-17T15:25:33Z

+  unfold jacobianMatrix
+  have h_smul : (fun Y => c • F Y) = fun Y => (c • F) Y := rfl
+  rw [h_smul]
+  rw [fderiv_const_smul hF]
+  simp only [ContinuousLinearMap.smul_apply]
+  rfl


Suggested change

unfold jacobianMatrix

have h_smul : (fun Y => c • F Y) = fun Y => (c • F) Y := rfl

rw [h_smul]

rw [fderiv_const_smul hF]

simp only [ContinuousLinearMap.smul_apply]

rfl

simp [fderiv_fun_const_smul, *]

Thanks, I have simplified this proof using simp [fderiv_fun_const_smul, *].

This PR introduces the Jacobian matrix for functions F : Matrix m n ℝ → Matrix p q ℝ. Main definitions: - `jacobianMatrix F X`: The Jacobian matrix at point X, indexed by (p × q) × (m × n) Main theorems: - `fderiv_eq_jacobian_mul`: Express fderiv in terms of Jacobian entries - `jacobianMatrix_comp`: Chain rule for Jacobian matrices - Basic rules: linearity, identity, constant, addition, scalar multiplication

hdmkindom · 2026-05-19T17:00:46Z

Thanks for the reviews.

I have pushed an updated version addressing the previous comments:

removed the incorrect mkdir ... line from the PR description;
moved repeated arguments into variable declarations where appropriate;
generalized the definitions and statements from ℝ to a nontrivially normed field where possible;
simplified several proofs using simp;
adjusted the simp lemma shape for jacobianMatrix_eq_fderiv_basis.

This is my first time revising a mathlib PR, and I accidentally rewrote the branch history while updating the PR. Sorry for the inconvenience.

github-actions Bot added new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-analysis Analysis (normed *, calculus) labels Jan 9, 2026

leanprover-community-bot-assistant assigned ADedecker Jan 13, 2026

jcommelin reviewed Feb 17, 2026

View reviewed changes

jcommelin added the awaiting-author A reviewer has asked the author a question or requested changes. label Feb 17, 2026

jcommelin assigned sgouezel and unassigned ADedecker Feb 17, 2026

erdOne reviewed Feb 17, 2026

View reviewed changes

hdmkindom force-pushed the gradient branch from 4ab6ca5 to b6aab79 Compare May 19, 2026 16:15

fix Fintype

0b31fd4

	fun (i, k) (j, l) => (fderiv ℝ F X (Matrix.single j l (1 : ℝ))) i k
	fun (i, k) (j, l) => fderiv ℝ F X (Matrix.single j l (1 : ℝ)) i k

Uh oh!

Conversation

hdmkindom commented Jan 9, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Main definitions

Main theorems

Uh oh!

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

Uh oh!

PR summary 0b31fd4983

Import changes for modified files

Declarations diff

Uh oh!

jcommelin commented Feb 17, 2026

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

hdmkindom May 19, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

hdmkindom commented May 19, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

hdmkindom commented Jan 9, 2026 •

edited

Loading

github-actions Bot commented Jan 9, 2026 •

edited

Loading

hdmkindom May 19, 2026 •

edited

Loading