Jacobian matrix

DefinitionJacobian matrix#✓fully proved

For \(f : \mathbb{R}^m \to \mathbb{R}^n\) and \(x \in \mathbb{R}^m\), the Jacobian matrix of \(f\) at \(x\) is the \(n \times m\) real matrix whose \((i, j)\) entry is the partial derivative of the \(i\)-th component \(f_i\) of \(f\) in the \(j\)-th coordinate direction at \(x\): the derivative at \(t = 0\) of \(t \mapsto f_i(x + t e_j)\), where \(e_j\) is the \(j\)-th standard basis vector of \(\mathbb{R}^m\). A partial derivative that does not exist is taken to be \(0\).

noncomputable def jacobianMatrix {m n : ℕ} (f : (Fin m → ℝ) → (Fin n → ℝ))
    (x : Fin m → ℝ) : Matrix (Fin n) (Fin m) ℝ :=
  fun i j => deriv (fun t : ℝ => f (x + t • Pi.single j (1 : ℝ)) i) 0

Sources

• W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 9; stable ref https://en.wikipedia.org/wiki/Jacobian_matrix_and_determinant.

Used by 8

Used byEntries of the Jacobian matrix are partial derivatives · Jacobian entries at a point of differentiability · Chain rule for Jacobian matrices · The Jacobian is the matrix of the derivative · Jacobian of a linear map given by a matrix · The Jacobian matrix computes the derivative · Computation of the Gierer–Meinhardt Jacobian at the steady state · Computation of the Schnakenberg Jacobian at the steady state

TheoremEntries of the Jacobian matrix are partial derivatives#✓fully proved

Let \(f : \mathbb{R}^m \to \mathbb{R}^n\) and \(x \in \mathbb{R}^m\). For every row index \(i\) and column index \(j\), the \((i, j)\) entry of the Jacobian matrix of \(f\) at \(x\) is the derivative at \(t = 0\) of \(t \mapsto f_i(x + t e_j)\), where \(f_i\) is the \(i\)-th component of \(f\) and \(e_j\) is the \(j\)-th standard basis vector of \(\mathbb{R}^m\). This derivative is taken to be \(0\) when it does not exist.

theorem jacobianMatrix_apply {m n : ℕ} (f : (Fin m → ℝ) → (Fin n → ℝ))
    (x : Fin m → ℝ) (i : Fin n) (j : Fin m) :
    jacobianMatrix f x i j =
      deriv (fun t : ℝ => f (x + t • Pi.single j (1 : ℝ)) i) 0

Sources

• W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 9.

Uses 1 · Used by 1

Statement usesJacobian matrix

Used byJacobian entries at a point of differentiability

TheoremJacobian entries at a point of differentiability#✓fully proved

Let \(f : \mathbb{R}^m \to \mathbb{R}^n\) be differentiable at \(x \in \mathbb{R}^m\). Then for every row index \(i\) and column index \(j\), the \((i, j)\) entry of the Jacobian matrix of \(f\) at \(x\) is the \(i\)-th coordinate of \(Df(x)\, e_j\), where \(Df(x)\) is the Fréchet derivative of \(f\) at \(x\) and \(e_j\) is the \(j\)-th standard basis vector of \(\mathbb{R}^m\).

theorem jacobianMatrix_apply_of_differentiableAt {m n : ℕ}
    (f : (Fin m → ℝ) → (Fin n → ℝ)) (x : Fin m → ℝ)
    (hf : DifferentiableAt ℝ f x) (i : Fin n) (j : Fin m) :
    jacobianMatrix f x i j = fderiv ℝ f x (Pi.single j (1 : ℝ)) i

Uses 2 · Used by 2

Statement usesJacobian matrix

Proof usesEntries of the Jacobian matrix are partial derivatives

Used byThe Jacobian is the matrix of the derivative · Jacobian of a linear map given by a matrix

TheoremThe Jacobian is the matrix of the derivative#✓fully proved

Let \(f : \mathbb{R}^m \to \mathbb{R}^n\) be differentiable at \(x \in \mathbb{R}^m\). Then the Jacobian matrix of \(f\) at \(x\) is the matrix, in the standard bases of \(\mathbb{R}^m\) and \(\mathbb{R}^n\), of the Fréchet derivative of \(f\) at \(x\), viewed as a linear map \(\mathbb{R}^m \to \mathbb{R}^n\).

theorem jacobianMatrix_eq_toMatrix'_fderiv {m n : ℕ}
    (f : (Fin m → ℝ) → (Fin n → ℝ)) (x : Fin m → ℝ)
    (hf : DifferentiableAt ℝ f x) :
    jacobianMatrix f x = LinearMap.toMatrix' (fderiv ℝ f x).toLinearMap

Uses 2 · Used by 2

Statement usesJacobian matrix

Proof usesJacobian entries at a point of differentiability

Used byChain rule for Jacobian matrices · The Jacobian matrix computes the derivative

TheoremJacobian of a linear map given by a matrix#✓fully proved

Let \(M\) be a real \(n \times m\) matrix. At every point \(x \in \mathbb{R}^m\), the Jacobian matrix of the map \(y \mapsto M y\) from \(\mathbb{R}^m\) to \(\mathbb{R}^n\) is \(M\).

theorem jacobianMatrix_fun_mulVec {m n : ℕ}
    (M : Matrix (Fin n) (Fin m) ℝ) (x : Fin m → ℝ) :
    jacobianMatrix (fun y => M *ᵥ y) x = M

Uses 2

Statement usesJacobian matrix

Proof usesJacobian entries at a point of differentiability

TheoremThe Jacobian matrix computes the derivative#✓fully proved

Let \(f : \mathbb{R}^m \to \mathbb{R}^n\) be differentiable at \(x \in \mathbb{R}^m\), and let \(J\) be the Jacobian matrix of \(f\) at \(x\). Then for every \(v \in \mathbb{R}^m\), the product \(J v\) equals \(Df(x)\, v\), the Fréchet derivative of \(f\) at \(x\) applied to \(v\).

Proof: The Jacobian is the matrix of the Fréchet derivative (Wikipedia, "Jacobian matrix and determinant": it represents the total derivative), and multiplying a vector by the matrix of a linear map applies the map to that vector.

theorem jacobianMatrix_mulVec_eq_fderiv {m n : ℕ}
    (f : (Fin m → ℝ) → (Fin n → ℝ)) (x : Fin m → ℝ)
    (hf : DifferentiableAt ℝ f x) (v : Fin m → ℝ) :
    (jacobianMatrix f x).mulVec v = fderiv ℝ f x v

Sources

• W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 9.

Uses 2

Statement usesJacobian matrix

Proof usesThe Jacobian is the matrix of the derivative

TheoremChain rule for Jacobian matrices#✓fully proved

Let \(f : \mathbb{R}^m \to \mathbb{R}^n\), \(g : \mathbb{R}^n \to \mathbb{R}^p\) and \(x \in \mathbb{R}^m\), and write \(J_h(y)\) for the Jacobian matrix of \(h\) at \(y\). If \(f\) is differentiable at \(x\) and \(g\) is differentiable at \(f(x)\), then \(J_{g \circ f}(x) = J_g(f(x))\, J_f(x)\), a product of a \(p \times n\) and an \(n \times m\) matrix.

Proof: As in Wikipedia, "Jacobian matrix and determinant" (chain rule), write each Jacobian as the matrix of the Fréchet derivative, then use the chain rule for Fréchet derivatives and the fact that the matrix of a composition of linear maps is the product of their matrices.

theorem jacobianMatrix_comp {m n p : ℕ}
    (f : (Fin m → ℝ) → (Fin n → ℝ)) (g : (Fin n → ℝ) → (Fin p → ℝ))
    (x : Fin m → ℝ)
    (hf : DifferentiableAt ℝ f x) (hg : DifferentiableAt ℝ g (f x)) :
    jacobianMatrix (g ∘ f) x =
      (jacobianMatrix g (f x)) * (jacobianMatrix f x)

Sources

• W. Rudin, Principles of Mathematical Analysis, 3rd ed., Theorem 9.15.

Uses 2

Statement usesJacobian matrix

Proof usesThe Jacobian is the matrix of the derivative

7 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.