Cauchy interlacing theorem

DefinitionCompression of an operator to a subspace#✓fully proved

The compression of an operator T to a subspace S: project T x orthogonally back onto S.

noncomputable def compression (T : E →ₗ[𝕜] E) (S : Submodule 𝕜 E)
    [S.HasOrthogonalProjection] : S →ₗ[𝕜] S :=
  (S.orthogonalProjectionOnto : E →L[𝕜] S).toLinearMap ∘ₗ T ∘ₗ S.subtype

Used by 6

Used byCauchy interlacing · Action of the compression of an operator · Compression of a symmetric operator is symmetric · Rayleigh form of a compression · Cauchy interlacing, upper half · Cauchy interlacing, lower half

TheoremAction of the compression of an operator#✓fully proved

The compression acts by projecting the image back onto the subspace.

theorem compression_apply (T : E →ₗ[𝕜] E) (S : Submodule 𝕜 E)
    [S.HasOrthogonalProjection] (y : S) :
    compression T S y = S.orthogonalProjectionOnto (T (y : E))

Uses 1 · Used by 2

Statement usesCompression of an operator to a subspace

Used byCompression of a symmetric operator is symmetric · Rayleigh form of a compression

TheoremCompression of a symmetric operator is symmetric#✓fully proved

The compression of a symmetric operator is symmetric.

theorem compression_isSymmetric {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric)
    (S : Submodule 𝕜 E) [S.HasOrthogonalProjection] :
    (compression T S).IsSymmetric

Uses 2 · Used by 3

Statement usesCompression of an operator to a subspace

Proof usesAction of the compression of an operator

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

TheoremRayleigh form of a compression#✓fully proved

The Rayleigh form of the compression at y equals the Rayleigh form of the original operator at the underlying vector (y : E).

theorem compression_rayleigh {T : E →ₗ[𝕜] E}
    (S : Submodule 𝕜 E) [S.HasOrthogonalProjection] (y : S) :
    rayleighForm (compression T S) y = rayleighForm T (y : E)

Uses 3 · Used by 2

Statement usesCompression of an operator to a subspace · Rayleigh form of an operator

Proof usesAction of the compression of an operator

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

TheoremSubspaces of every smaller dimension inside a given subspace#✓fully proved

A subspace of dimension m can be thinned to a subspace of any smaller dimension.

theorem exists_submodule_le_finrank_eq {W : Submodule 𝕜 E} {m : ℕ}
    (h : m ≤ Module.finrank 𝕜 W) :
    ∃ W' : Submodule 𝕜 E, W' ≤ W ∧ Module.finrank 𝕜 W' = m

Used by 1

Used byCauchy interlacing, upper half

TheoremCauchy interlacing, upper half#✓fully proved

The k-th eigenvalue of the compression to a codimension-one subspace is at most the k-th eigenvalue of the original operator.

theorem eigenvalue_compression_le_eigenvalue (S : Submodule 𝕜 E)
    [S.HasOrthogonalProjection] (hS : Module.finrank 𝕜 S = n - 1)
    {k : ℕ} (hk : k + 1 < n) :
    (compression_isSymmetric hT S).eigenvalues hS ⟨k, by omega⟩ ≤
      hT.eigenvalues hn ⟨k, by omega⟩

Uses 7 · Used by 1

Statement usesCompression of an operator to a subspace · Compression of a symmetric operator is symmetric

Proof usesRayleigh form of a compression · Subspaces of every smaller dimension inside a given subspace · Courant–Fischer min–max, extremal subspace form · Courant–Fischer min–max, lower-bound form · Rayleigh form of an operator

Used byCauchy interlacing

TheoremCauchy interlacing, lower half#✓fully proved

The k-th eigenvalue of the compression to a codimension-one subspace is at least the (k+1)-st eigenvalue of the original operator.

theorem eigenvalue_le_eigenvalue_compression (S : Submodule 𝕜 E)
    [S.HasOrthogonalProjection] (hS : Module.finrank 𝕜 S = n - 1)
    {k : ℕ} (hk : k + 1 < n) :
    hT.eigenvalues hn ⟨k + 1, hk⟩ ≤
      (compression_isSymmetric hT S).eigenvalues hS ⟨k, by omega⟩

Uses 6 · Used by 1

Statement usesCompression of an operator to a subspace · Compression of a symmetric operator is symmetric

Proof usesRayleigh form of a compression · Courant–Fischer min–max, extremal subspace form · Courant–Fischer min–max, lower-bound form · Rayleigh form of an operator

Used byCauchy interlacing

TheoremCauchy interlacing#✓fully proved

For a codimension-one subspace S, the eigenvalues μₖ of the compression of a self-adjoint operator T interlace the eigenvalues λₖ of T: λₖ₊₁ ≤ μₖ ≤ λₖ.

theorem cauchy_interlacing (S : Submodule 𝕜 E) [S.HasOrthogonalProjection]
    (hS : Module.finrank 𝕜 S = n - 1) {k : ℕ} (hk : k + 1 < n) :
    hT.eigenvalues hn ⟨k + 1, hk⟩ ≤
        (compression_isSymmetric hT S).eigenvalues hS ⟨k, by omega⟩ ∧
      (compression_isSymmetric hT S).eigenvalues hS ⟨k, by omega⟩ ≤
        hT.eigenvalues hn ⟨k, by omega⟩

Uses 4

Statement usesCompression of an operator to a subspace · Compression of a symmetric operator is symmetric

Proof usesCauchy interlacing, upper half · Cauchy interlacing, lower half

8 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.