Subspace convergence via orthogonal-projector distances

A measurably-varying family of subspaces of EuclideanSpace ℝ (Fin d) is encoded in this formalization by the matrix of its orthogonal projection, Oseledets.orthProjMatrix (Oseledets.Lyapunov.MeasurableSubspace). This module turns the abstract finite-dimensional-completeness CauchySeq machinery of Oseledets.cauchySeq_of_summable_norm_sub (Oseledets.Lyapunov.OseledetsLimit.BandProjector) into a subspace-convergence tool keyed on the differences of those orthogonal-projection matrices.

The metric we attach to a pair of subspaces is the operator-norm distance between their orthogonal projectors, subspaceDist U V = ‖orthProjMatrix U - orthProjMatrix V‖, which is the standard gap (aperture) distance on the Grassmannian. A sequence of subspaces whose consecutive projector gaps are summable then has a convergent projector sequence, and the limit is again an orthogonal projector — self-adjoint and idempotent. This is exactly the soft analysis needed to extract a limiting flag space from a Cauchy sequence of finite-step subspaces (e.g. the eventual-kernel / Oseledets filtration constructions for singular cocycles).

Main definitions

• Oseledets.subspaceDist: the orthogonal-projector operator-norm distance between two subspaces.

Main results

• Oseledets.subspaceDist_self: the distance of a subspace to itself is 0.
• Oseledets.cauchySeq_of_summable_subspaceDist: summable consecutive projector gaps give a Cauchy projector sequence.
• Oseledets.exists_tendsto_orthProjMatrix_of_summable: such a sequence converges to a matrix P that is self-adjoint and idempotent (P * P = P) — an orthogonal projector.

noncomputable def Oseledets.subspaceDist {d : ℕ} (U V : Submodule ℝ (EuclideanSpace ℝ (Fin d))) [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] : ℝ

The orthogonal-projector gap distance between two subspaces of EuclideanSpace ℝ (Fin d): the operator-norm distance between the matrices of their orthogonal projections. This is the aperture (gap) metric on the Grassmannian, the natural distance under which subspace-valued families converge in this formalization.

Equations

• Oseledets.subspaceDist U V = ‖Oseledets.orthProjMatrix U - Oseledets.orthProjMatrix V‖

theorem Oseledets.subspaceDist_self {d : ℕ} (U : Submodule ℝ (EuclideanSpace ℝ (Fin d))) [U.HasOrthogonalProjection] : subspaceDist U U = 0

The gap distance of a subspace to itself is 0.

theorem Oseledets.isSelfAdjoint_orthProjMatrix {d : ℕ} (K : Submodule ℝ (EuclideanSpace ℝ (Fin d))) [K.HasOrthogonalProjection] : IsSelfAdjoint (orthProjMatrix K)

Self-adjointness of the orthogonal-projection matrix. orthProjMatrix K is the image of the (self-adjoint) orthogonal projection K.starProjection under the star algebra equivalence (Matrix.toEuclideanCLM).symm, hence self-adjoint.

theorem Oseledets.isIdempotentElem_orthProjMatrix {d : ℕ} (K : Submodule ℝ (EuclideanSpace ℝ (Fin d))) [K.HasOrthogonalProjection] : orthProjMatrix K * orthProjMatrix K = orthProjMatrix K

Idempotence of the orthogonal-projection matrix. orthProjMatrix K is the image of the idempotent orthogonal projection K.starProjection under the (multiplicative) star algebra equivalence (Matrix.toEuclideanCLM).symm, hence idempotent.

theorem Oseledets.cauchySeq_of_summable_subspaceDist {d : ℕ} {V : ℕ → Submodule ℝ (EuclideanSpace ℝ (Fin d))} [∀ (n : ℕ), (V n).HasOrthogonalProjection] (hsum : Summable fun (n : ℕ) => ‖orthProjMatrix (V (n + 1)) - orthProjMatrix (V n)‖) : CauchySeq fun (n : ℕ) => orthProjMatrix (V n)

Cauchy from summable gaps. If the consecutive projector gaps ‖orthProjMatrix (V (n+1)) - orthProjMatrix (V n)‖ of a sequence of subspaces are summable, then the projector sequence n ↦ orthProjMatrix (V n) is Cauchy in the (L2 operator) matrix metric. This is pure soft analysis: matrices over ℝ form a finite-dimensional, hence complete, normed space.

theorem Oseledets.exists_tendsto_orthProjMatrix_of_summable {d : ℕ} {V : ℕ → Submodule ℝ (EuclideanSpace ℝ (Fin d))} [∀ (n : ℕ), (V n).HasOrthogonalProjection] (hsum : Summable fun (n : ℕ) => ‖orthProjMatrix (V (n + 1)) - orthProjMatrix (V n)‖) : ∃ (P : Matrix (Fin d) (Fin d) ℝ), Filter.Tendsto (fun (n : ℕ) => orthProjMatrix (V n)) Filter.atTop (nhds P) ∧ IsSelfAdjoint P ∧ P * P = P

Convergence to an orthogonal projector. If the consecutive projector gaps of a sequence of subspaces are summable, then n ↦ orthProjMatrix (V n) converges to some matrix P, and the limit is again an orthogonal projector: it is self-adjoint and idempotent (P * P = P).

Self-adjointness passes to the limit because the entrywise Hermitian relation orthProjMatrix (V n) j i = orthProjMatrix (V n) i j is closed under the (finite-dimensional) matrix limit; idempotence passes to the limit because matrix multiplication is continuous in the L2 operator norm and each term satisfies orthProjMatrix_idem.