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.

mkdir 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

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

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

PR summary bd33e8d4d0

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)	1993

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

## 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).

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

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.

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?

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

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]

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.

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

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

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, *]

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, *]

hdmkindom added 2 commits January 9, 2026 12:41

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

hdmkindom and others added 6 commits January 9, 2026 13:29

Merge upstream/master to get updated linter

95ec360

fix error

9161c5d

Merge branch 'gradient' of github.com:hdmkindom/mathlib4 into gradient

cbc93dd

Merge branch 'master' into gradient

0a1bf33

Merge branch 'master' into gradient

4ab6ca5

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

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat(Analysis/Matrix): add Jacobian matrix for matrix-valued functions#33786

feat(Analysis/Matrix): add Jacobian matrix for matrix-valued functions#33786
hdmkindom wants to merge 8 commits intoleanprover-community:masterfrom
hdmkindom:gradient

hdmkindom commented Jan 9, 2026

Uh oh!

github-actions Bot commented Jan 9, 2026 •

edited

Loading

Declarations diff

Uh oh!

jcommelin commented Feb 17, 2026

Uh oh!

jcommelin Feb 17, 2026

Uh oh!

jcommelin Feb 17, 2026

Uh oh!

erdOne Feb 17, 2026

Uh oh!

erdOne Feb 17, 2026

Uh oh!

erdOne Feb 17, 2026

Uh oh!

erdOne Feb 17, 2026

Uh oh!

erdOne Feb 17, 2026

Uh oh!

erdOne Feb 17, 2026

Uh oh!

erdOne Feb 17, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

	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

Conversation

hdmkindom commented Jan 9, 2026

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 bd33e8d4d0

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!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

github-actions Bot commented Jan 9, 2026 •

edited

Loading