Polarisation of the orthogonal projector onto a subspace

For a finite-dimensional real inner-product space EuclideanSpace ℝ (Fin d) and a subspace K, this module records the polarisation identity for the orthogonal projector K.starProjection, expressing every coordinate of a projected vector as a fixed real-arithmetic combination of the scalar distance-to-subspace maps c ↦ infDist c K.

Writing P := K.starProjection for the orthogonal projection onto K (every subspace of a finite-dimensional space is complete, hence has an orthogonal projection) and e_a for the standard basis vector EuclideanSpace.single a 1, self-adjointness and idempotency of P give ⟪e_b, P e_a⟫ = ⟪P e_b, P e_a⟫, so every coordinate of P e_a is an inner product of two projections. The polarisation identity expands such an inner product into a combination of the squared norms ‖P c‖², and Pythagoras gives ‖P c‖² = ‖c‖² − infDist c K² (c = P c + (c − P c) is an orthogonal decomposition and infDist c K realises ‖c − P c‖). Hence every coordinate of every projected vector P c is a real-arithmetic combination of the scalar distance maps infDist · K.

This algebraic core is the sorry-free heart of the singular ("issue #6") measurable-projector converter: composed with the measurability of the distance maps it makes the orthogonal projector of a measurably-varying subspace family (a.e.) measurable.

Main results

• Oseledets.infDist_eq_norm_sub_starProjection: infDist c K = ‖c − K.starProjection c‖.
• Oseledets.norm_starProjection_sq: Pythagoras, ‖K.starProjection c‖² = ‖c‖² − infDist c K².
• Oseledets.starProjection_apply_coord: the projector-coordinate polarisation identity, writing (K.starProjection u) b as a real combination of three squared-norm–minus–infDist² terms.

Literature: Kuratowski–Ryll-Nardzewski, A general theorem on selectors (1965); Castaing–Valadier, Convex Analysis and Measurable Multifunctions; C. González-Tokman, A. Quas, A semi-invertible operator Oseledets theorem (ETDS 2014), Appendix B.

theorem Oseledets.infDist_eq_norm_sub_starProjection {d : ℕ} (K : Submodule ℝ (EuclideanSpace ℝ (Fin d))) (c : EuclideanSpace ℝ (Fin d)) : Metric.infDist c ↑K = ‖c - K.starProjection c‖

Distance to a subspace is the norm of the projection residual. For a closed (here: finite-dimensional, hence complete) subspace K, infDist c K = ‖c − K.starProjection c‖. The orthogonal projection realises the infimum ⨅ x : K, ‖c − x‖ (starProjection_minimal), and infDist is exactly that infimum (infDist_eq_iInf, with dist = ‖· − ·‖).

theorem Oseledets.norm_starProjection_sq {d : ℕ} (K : Submodule ℝ (EuclideanSpace ℝ (Fin d))) (c : EuclideanSpace ℝ (Fin d)) : ‖K.starProjection c‖ ^ 2 = ‖c‖ ^ 2 - Metric.infDist c ↑K ^ 2

Pythagoras for the projector. ‖K.starProjection c‖² = ‖c‖² − infDist c K ². The orthogonal decomposition c = K.starProjection c + (c − K.starProjection c) has orthogonal summands, so ‖c‖² = ‖K.starProjection c‖² + ‖c − K.starProjection c‖², and the residual norm is infDist c K by infDist_eq_norm_sub_starProjection.

theorem Oseledets.starProjection_apply_coord {d : ℕ} (K : Submodule ℝ (EuclideanSpace ℝ (Fin d))) (u : EuclideanSpace ℝ (Fin d)) (b : Fin d) : (K.starProjection u).ofLp b = (‖EuclideanSpace.single b 1‖ ^ 2 - Metric.infDist (EuclideanSpace.single b 1) ↑K ^ 2 + (‖u‖ ^ 2 - Metric.infDist u ↑K ^ 2) - (‖EuclideanSpace.single b 1 - u‖ ^ 2 - Metric.infDist (EuclideanSpace.single b 1 - u) ↑K ^ 2)) / 2

A projector coordinate is a distance combination. The b-th coordinate of the projected vector K.starProjection u equals ½[(‖single b‖² − infDist (single b) K²) + (‖u‖² − infDist u K²) − (‖single b − u‖² − infDist (single b − u) K²)]. Self-adjointness and idempotency give (K.starProjection u) b = ⟪K.starProjection (single b), K.starProjection u⟫; polarisation expands the inner product into squared norms of projections; each squared norm is ‖·‖² − infDist · K² by norm_starProjection_sq (with K.starProjection (single b) − K.starProjection u = K.starProjection (single b − u)).