Courant–Fischer min–max theorem

DefinitionRayleigh form of an operator#✓fully proved

The Rayleigh form of a vector for an operator T: re ⟪T x, x⟫. On unit vectors this is the Rayleigh quotient.

noncomputable def rayleighForm (T : E →ₗ[𝕜] E) (x : E) : ℝ :=
  RCLike.re ⟪T x, x⟫_𝕜

Used by 17

Used byRayleigh form of a compression · Cauchy interlacing, upper half · Cauchy interlacing, lower half · The k-th eigenvector attains the Rayleigh bound on the head · The k-th eigenvector attains the Rayleigh bound on the tail · Courant–Fischer max–min, extremal subspace form · Courant–Fischer min–max, extremal subspace form · Courant–Fischer min–max, lower-bound form · Courant–Fischer max–min, lower-bound form · Eigenbasis expansion of the Rayleigh form · Lower bound for the Rayleigh form on the eigenbasis head · Upper bound for the Rayleigh form on the eigenbasis tail · Rayleigh form scales quadratically · Weyl's inequality (lower bound) · Weyl's inequality (upper bound) · Courant–Fischer min–max, matrix form · Courant–Fischer max–min, matrix form

TheoremRayleigh form scales quadratically#✓fully proved

Scaling a vector by a real scalar scales the Rayleigh form by the square of the scalar.

theorem rayleighForm_smul (T : E →ₗ[𝕜] E) (c : ℝ) (x : E) :
    rayleighForm T ((c : 𝕜) • x) = c ^ 2 * rayleighForm T x

Uses 1 · Used by 2

Statement usesRayleigh form of an operator

Used byCourant–Fischer min–max, lower-bound form · Courant–Fischer max–min, lower-bound form

TheoremEigenbasis expansion of the quadratic form of a self-adjoint operator#✓fully proved

Expansion of ⟪x, T x⟫ in the orthonormal eigenbasis: a weighted sum of the eigenvalues with weights ‖⟪eᵢ, x⟫‖².

theorem inner_self_apply_eq_expansion (x : E) :
    ⟪x, T x⟫_𝕜 = ((∑ i : Fin n, hT.eigenvalues hn i *
      ‖⟪(hT.eigenvectorBasis hn) i, x⟫_𝕜‖ ^ 2 : ℝ) : 𝕜)

Used by 2

Used byEigenbasis expansion of the Rayleigh form · Quadratic form expanded in the ordered eigenbasis

TheoremEigenbasis expansion of the Rayleigh form#✓fully proved

The Rayleigh form expanded in the orthonormal eigenbasis.

theorem rayleighForm_eq_expansion (x : E) :
    rayleighForm T x = ∑ i : Fin n, hT.eigenvalues hn i *
      ‖⟪(hT.eigenvectorBasis hn) i, x⟫_𝕜‖ ^ 2

Uses 2 · Used by 4

Statement usesRayleigh form of an operator

Proof usesEigenbasis expansion of the quadratic form of a self-adjoint operator

Used byThe k-th eigenvector attains the Rayleigh bound on the head · The k-th eigenvector attains the Rayleigh bound on the tail · Lower bound for the Rayleigh form on the eigenbasis head · Upper bound for the Rayleigh form on the eigenbasis tail

TheoremSpan of some eigenvectors is orthogonal to the remaining ones#✓fully proved

A vector in the span of some of the eigenvectors is orthogonal to the remaining eigenvectors.

theorem inner_eigenvectorBasis_eq_zero_of_mem_span {m : ℕ} {v : Fin m → E}
    {x : E} (hx : x ∈ Submodule.span 𝕜 (Set.range v)) {i : Fin n}
    (hi : ∀ j, ⟪(hT.eigenvectorBasis hn) i, v j⟫_𝕜 = 0) :
    ⟪(hT.eigenvectorBasis hn) i, x⟫_𝕜 = 0

Used by 2

Used byLower bound for the Rayleigh form on the eigenbasis head · Upper bound for the Rayleigh form on the eigenbasis tail

DefinitionTail of an orthonormal eigenbasis#✓fully proved

The tail of the eigenbasis: the eigenvectors with index ≥ k, as a family indexed by Fin (n - k).

noncomputable def tailFamily {k : ℕ} (hk : k < n) : Fin (n - k) → E :=
  fun j => (hT.eigenvectorBasis hn) ⟨k + j.val, by have hj := j.isLt; omega⟩

Used by 8

Used byThe k-th eigenvector attains the Rayleigh bound on the tail · Courant–Fischer min–max, extremal subspace form · Courant–Fischer max–min, lower-bound form · Dimension of the span of the eigenbasis tail · Upper bound for the Rayleigh form on the eigenbasis tail · Linear independence of the eigenbasis tail · Weyl's inequality (lower bound) · Weyl's inequality (upper bound)

DefinitionHead of an orthonormal eigenbasis#✓fully proved

The head of the eigenbasis: the eigenvectors with index ≤ k, as a family indexed by Fin (k + 1).

noncomputable def headFamily {k : ℕ} (hk : k < n) : Fin (k + 1) → E :=
  fun j => (hT.eigenvectorBasis hn) ⟨j.val, by have hj := j.isLt; omega⟩

Used by 8

Used byThe k-th eigenvector attains the Rayleigh bound on the head · Courant–Fischer max–min, extremal subspace form · Courant–Fischer min–max, lower-bound form · Dimension of the span of the eigenbasis head · Linear independence of the eigenbasis head · Lower bound for the Rayleigh form on the eigenbasis head · Weyl's inequality (lower bound) · Weyl's inequality (upper bound)

TheoremLinear independence of the eigenbasis tail#✓fully proved

The tail family is linearly independent, as a restriction of the orthonormal eigenbasis.

theorem tailFamily_linearIndependent {k : ℕ} (hk : k < n) :
    LinearIndependent 𝕜 (tailFamily hT hn hk)

Uses 1 · Used by 1

Statement usesTail of an orthonormal eigenbasis

Used byDimension of the span of the eigenbasis tail

TheoremLinear independence of the eigenbasis head#✓fully proved

The head family is linearly independent, as a restriction of the orthonormal eigenbasis.

theorem headFamily_linearIndependent {k : ℕ} (hk : k < n) :
    LinearIndependent 𝕜 (headFamily hT hn hk)

Uses 1 · Used by 1

Statement usesHead of an orthonormal eigenbasis

Used byDimension of the span of the eigenbasis head

TheoremDimension of the span of the eigenbasis tail#✓fully proved

The span of the tail of the eigenbasis has dimension n - k.

theorem finrank_span_tailFamily {k : ℕ} (hk : k < n) :
    Module.finrank 𝕜 (Submodule.span 𝕜 (Set.range (tailFamily hT hn hk))) = n - k

Uses 2 · Used by 4

Statement usesTail of an orthonormal eigenbasis

Proof usesLinear independence of the eigenbasis tail

Used byCourant–Fischer min–max, extremal subspace form · Courant–Fischer max–min, lower-bound form · Weyl's inequality (lower bound) · Weyl's inequality (upper bound)

TheoremDimension of the span of the eigenbasis head#✓fully proved

The span of the head of the eigenbasis has dimension k + 1.

theorem finrank_span_headFamily {k : ℕ} (hk : k < n) :
    Module.finrank 𝕜 (Submodule.span 𝕜 (Set.range (headFamily hT hn hk))) = k + 1

Uses 2 · Used by 4

Statement usesHead of an orthonormal eigenbasis

Proof usesLinear independence of the eigenbasis head

Used byCourant–Fischer max–min, extremal subspace form · Courant–Fischer min–max, lower-bound form · Weyl's inequality (lower bound) · Weyl's inequality (upper bound)

TheoremUpper bound for the Rayleigh form on the eigenbasis tail#✓fully proved

On the span of the tail of the eigenbasis, the Rayleigh form is at most λₖ * ‖x‖².

theorem rayleighForm_le_of_mem_tail {k : ℕ} (hk : k < n) {x : E}
    (hx : x ∈ Submodule.span 𝕜 (Set.range (tailFamily hT hn hk))) :
    rayleighForm T x ≤ hT.eigenvalues hn ⟨k, hk⟩ * ‖x‖ ^ 2

Uses 4 · Used by 4

Statement usesRayleigh form of an operator · Tail of an orthonormal eigenbasis

Proof usesSpan of some eigenvectors is orthogonal to the remaining ones · Eigenbasis expansion of the Rayleigh form

Used byCourant–Fischer min–max, extremal subspace form · Courant–Fischer max–min, lower-bound form · Weyl's inequality (lower bound) · Weyl's inequality (upper bound)

TheoremLower bound for the Rayleigh form on the eigenbasis head#✓fully proved

On the span of the head of the eigenbasis, the Rayleigh form is at least λₖ * ‖x‖².

theorem rayleighForm_ge_of_mem_head {k : ℕ} (hk : k < n) {x : E}
    (hx : x ∈ Submodule.span 𝕜 (Set.range (headFamily hT hn hk))) :
    hT.eigenvalues hn ⟨k, hk⟩ * ‖x‖ ^ 2 ≤ rayleighForm T x

Uses 4 · Used by 4

Statement usesHead of an orthonormal eigenbasis · Rayleigh form of an operator

Proof usesSpan of some eigenvectors is orthogonal to the remaining ones · Eigenbasis expansion of the Rayleigh form

Used byCourant–Fischer max–min, extremal subspace form · Courant–Fischer min–max, lower-bound form · Weyl's inequality (lower bound) · Weyl's inequality (upper bound)

TheoremThe k-th eigenvector attains the Rayleigh bound on the tail#✓fully proved

The k-th eigenvector lies in the tail span, is a unit vector, and attains the Rayleigh value λₖ.

theorem exists_eigenvector_mem_tail {k : ℕ} (hk : k < n) :
    ∃ x ∈ Submodule.span 𝕜 (Set.range (tailFamily hT hn hk)), ‖x‖ = 1 ∧
      rayleighForm T x = hT.eigenvalues hn ⟨k, hk⟩

Uses 3 · Used by 1

Statement usesRayleigh form of an operator · Tail of an orthonormal eigenbasis

Proof usesEigenbasis expansion of the Rayleigh form

Used byCourant–Fischer min–max, extremal subspace form

TheoremThe k-th eigenvector attains the Rayleigh bound on the head#✓fully proved

The k-th eigenvector lies in the head span, is a unit vector, and attains the Rayleigh value λₖ.

theorem exists_eigenvector_mem_head {k : ℕ} (hk : k < n) :
    ∃ x ∈ Submodule.span 𝕜 (Set.range (headFamily hT hn hk)), ‖x‖ = 1 ∧
      rayleighForm T x = hT.eigenvalues hn ⟨k, hk⟩

Uses 3 · Used by 1

Statement usesHead of an orthonormal eigenbasis · Rayleigh form of an operator

Proof usesEigenbasis expansion of the Rayleigh form

Used byCourant–Fischer max–min, extremal subspace form

TheoremCourant–Fischer min–max, extremal subspace form#✓fully proved

There is a subspace W of dimension n - k on which every unit vector has Rayleigh quotient at most λₖ, and the bound is attained.

theorem exists_tail_submodule {k : ℕ} (hk : k < n) :
    ∃ W : Submodule 𝕜 E, Module.finrank 𝕜 W = n - k ∧
      (∀ x ∈ W, ‖x‖ = 1 → rayleighForm T x ≤ hT.eigenvalues hn ⟨k, hk⟩) ∧
      ∃ x ∈ W, ‖x‖ = 1 ∧ rayleighForm T x = hT.eigenvalues hn ⟨k, hk⟩

Uses 5 · Used by 2

Statement usesRayleigh form of an operator

Proof usesThe k-th eigenvector attains the Rayleigh bound on the tail · Dimension of the span of the eigenbasis tail · Upper bound for the Rayleigh form on the eigenbasis tail · Tail of an orthonormal eigenbasis

Used byCauchy interlacing, upper half · Cauchy interlacing, lower half

TheoremCourant–Fischer min–max, lower-bound form#✓fully proved

Every subspace of dimension n - k contains a unit vector with Rayleigh quotient at least λₖ.

theorem exists_unit_ge_of_submodule {k : ℕ} (hk : k < n) (W : Submodule 𝕜 E)
    (hW : Module.finrank 𝕜 W = n - k) :
    ∃ x ∈ W, ‖x‖ = 1 ∧ hT.eigenvalues hn ⟨k, hk⟩ ≤ rayleighForm T x

Uses 5 · Used by 3

Statement usesRayleigh form of an operator

Proof usesDimension of the span of the eigenbasis head · Head of an orthonormal eigenbasis · Lower bound for the Rayleigh form on the eigenbasis head · Rayleigh form scales quadratically

Used byCauchy interlacing, upper half · Cauchy interlacing, lower half · Courant–Fischer min–max, matrix form

TheoremCourant–Fischer max–min, extremal subspace form#✓fully proved

There is a subspace U of dimension k + 1 on which every unit vector has Rayleigh quotient at least λₖ, and the bound is attained.

theorem exists_head_submodule {k : ℕ} (hk : k < n) :
    ∃ U : Submodule 𝕜 E, Module.finrank 𝕜 U = k + 1 ∧
      (∀ x ∈ U, ‖x‖ = 1 → hT.eigenvalues hn ⟨k, hk⟩ ≤ rayleighForm T x) ∧
      ∃ x ∈ U, ‖x‖ = 1 ∧ rayleighForm T x = hT.eigenvalues hn ⟨k, hk⟩

Uses 5

Statement usesRayleigh form of an operator

Proof usesThe k-th eigenvector attains the Rayleigh bound on the head · Dimension of the span of the eigenbasis head · Head of an orthonormal eigenbasis · Lower bound for the Rayleigh form on the eigenbasis head

TheoremCourant–Fischer max–min, lower-bound form#✓fully proved

Every subspace of dimension k + 1 contains a unit vector with Rayleigh quotient at most λₖ.

theorem exists_unit_le_of_submodule {k : ℕ} (hk : k < n) (U : Submodule 𝕜 E)
    (hU : Module.finrank 𝕜 U = k + 1) :
    ∃ x ∈ U, ‖x‖ = 1 ∧ rayleighForm T x ≤ hT.eigenvalues hn ⟨k, hk⟩

Uses 5 · Used by 1

Statement usesRayleigh form of an operator

Proof usesDimension of the span of the eigenbasis tail · Upper bound for the Rayleigh form on the eigenbasis tail · Rayleigh form scales quadratically · Tail of an orthonormal eigenbasis

Used byCourant–Fischer max–min, matrix form

19 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.