Hessian matrix

DefinitionHessian matrix#✓fully proved

For a function \(f : \mathbb{R}^n \to \mathbb{R}\) and a point \(x \in \mathbb{R}^n\), the Hessian matrix of \(f\) at \(x\) is the \(n \times n\) real matrix whose \((i, j)\) entry is \(\frac{d}{ds}\big|_{s=0} \frac{d}{dt}\big|_{t=0} f(x + s e_i + t e_j)\), where \(e_1, \dots, e_n\) is the standard basis of \(\mathbb{R}^n\) and a derivative that does not exist is taken to be \(0\).

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

Sources

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

Used by 4

Used byEntries of the Hessian matrix · Hessian entries as second Fréchet derivatives · Symmetry of the Hessian · Second-derivative test, necessary condition

TheoremEntries of the Hessian matrix#✓fully proved

For \(f : \mathbb{R}^n \to \mathbb{R}\), a point \(x \in \mathbb{R}^n\) and indices \(i, j\), the \((i, j)\) entry of the Hessian matrix of \(f\) at \(x\) is \(\frac{d}{ds}\big|_{s=0} \frac{d}{dt}\big|_{t=0} f(x + s e_i + t e_j)\), where \(e_1, \dots, e_n\) is the standard basis of \(\mathbb{R}^n\) and a derivative that does not exist is taken to be \(0\): differentiate first along \(e_j\), then along \(e_i\).

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

Sources

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

Uses 1 · Used by 1

Statement usesHessian matrix

Used byHessian entries as second Fréchet derivatives

TheoremHessian entries as second Fréchet derivatives#✓fully proved

Let \(f : \mathbb{R}^n \to \mathbb{R}\) be twice continuously differentiable and let \(x \in \mathbb{R}^n\). For all indices \(i, j\), the \((i, j)\) entry of the Hessian matrix of \(f\) at \(x\) equals \(D(Df)(x)(e_i)(e_j)\), the derivative of the Fréchet derivative \(Df\) at \(x\) in the direction \(e_i\), applied to \(e_j\), where \(e_1, \dots, e_n\) is the standard basis of \(\mathbb{R}^n\).

theorem hessianMatrix_eq_fderiv_fderiv {n : ℕ} (f : (Fin n → ℝ) → ℝ)
    (hf : ContDiff ℝ 2 f) (x : Fin n → ℝ) (i j : Fin n) :
    hessianMatrix f x i j =
      fderiv ℝ (fderiv ℝ f) x (Pi.single i 1) (Pi.single j 1)

Uses 2 · Used by 2

Statement usesHessian matrix

Proof usesEntries of the Hessian matrix

Used bySymmetry of the Hessian · Second-derivative test, necessary condition

TheoremSymmetry of the Hessian#✓fully proved

If \(f : \mathbb{R}^n \to \mathbb{R}\) is twice continuously differentiable, then for every \(x \in \mathbb{R}^n\) the Hessian matrix of \(f\) at \(x\) is symmetric: it equals its transpose.

Proof: Rewrite the matrix entries as evaluations of the second Fréchet derivative and apply Schwarz's theorem on the symmetry of second derivatives, as proved in Mathlib, following Wikipedia's “Symmetry of second derivatives”.

theorem hessianMatrix_symmetric {n : ℕ} (f : (Fin n → ℝ) → ℝ)
    (hf : ContDiff ℝ 2 f) (x : Fin n → ℝ) :
    (hessianMatrix f x).transpose = hessianMatrix f x

Sources

• W. Rudin, Principles of Mathematical Analysis, 3rd ed., Theorem 9.41 (pp. 235–236).

Uses 2

Statement usesHessian matrix

Proof usesHessian entries as second Fréchet derivatives

TheoremThe second derivative is nonnegative at a local minimum#✓fully proved

Let \(g : \mathbb{R} \to \mathbb{R}\) be twice continuously differentiable. If \(g\) has a local minimum at \(x\), then \(g''(x) \ge 0\).

This is the necessary direction of the one-variable second derivative test.

theorem _root_.IsLocalMin.deriv_deriv_nonneg {g : ℝ → ℝ} {x : ℝ}
    (hmin : IsLocalMin g x) (hg : ContDiff ℝ 2 g) : 0 ≤ deriv (deriv g) x

Used by 1

Used bySecond-derivative test, necessary condition

TheoremSecond-derivative test, necessary condition#✓fully proved

Let \(f : \mathbb{R}^n \to \mathbb{R}\) be twice continuously differentiable and let \(x\) be a local minimum of \(f\). Then the Hessian quadratic form of \(f\) at \(x\) is nonnegative: writing \(H\) for the Hessian matrix of \(f\) at \(x\), every \(v \in \mathbb{R}^n\) satisfies \(\sum_{i, j} v_i H_{ij} v_j \ge 0\).

Proof: Restrict the function to the affine line through \(x\) in direction \(v\), apply the necessary direction of the one-variable second derivative test, then expand the second Fréchet derivative in the standard basis. The one-variable step argues by contradiction as in the proof of the second-derivative test in Wikipedia's “Derivative test”: a negative second derivative makes the first derivative negative just right of the critical point, so the function decreases there.

theorem isLocalMin_hessian_quadratic_nonneg {n : ℕ} (f : (Fin n → ℝ) → ℝ)
    (hf : ContDiff ℝ 2 f) (x : Fin n → ℝ) (hmin : IsLocalMin f x)
    (v : Fin n → ℝ) :
    0 ≤ ∑ i, ∑ j, v i * hessianMatrix f x i j * v j

Sources

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

Uses 3

Statement usesHessian matrix

Proof usesThe second derivative is nonnegative at a local minimum · Hessian entries as second Fréchet derivatives

6 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.