Projection blocks and reflections

General RCLike block decomposition relative to an orthogonally complemented subspace. This module is independent of the Davis--Kahan theory.

Provenance

• Original repository: Davis--Kahan/DKPS formalization (Kitware, Inc.).
• Original module: authored directly in ForMathlib at Davis--Kahan commit df036cd; it has had no prior home.
• Extraction class: authored in place, for Tau Ceti — ForMathlib was retired on 2026-07-29 and ForTauCeti is the single staging library, whose destination is Tau Ceti and not Mathlib (ForTauCeti/README.md).
• Original authors / copyright: Jon Crall, GPT 5.6 High; Copyright (c) 2026 Kitware, Inc.; Apache 2.0.
• Spectra influence: none — the ForTauCeti import firewall admits only Mathlib, TauCeti and ForTauCeti (enforced by scripts/check_dependency_layers.py).

theorem Submodule.starProjection_congr {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {p q : Submodule 𝕜 E} [p.HasOrthogonalProjection] [q.HasOrthogonalProjection] (h : p = q) : p.starProjection = q.starProjection

Equal subspaces have the same orthogonal projection.

HasOrthogonalProjection is a Prop class, so once the subspaces are identified the two instance arguments coincide by proof irrelevance. This is needed wherever a spectral development names one subspace two ways -- the range selected by a complement set and the orthogonal complement of the range, say -- because rw on the subspace itself produces an ill-typed motive: starProjection takes an instance derived from the subspace being rewritten.

theorem Submodule.starProjection_congr_apply {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {p q : Submodule 𝕜 E} [p.HasOrthogonalProjection] [q.HasOrthogonalProjection] (h : p = q) (x : E) : p.starProjection x = q.starProjection x

Pointwise form of Submodule.starProjection_congr, for rewriting under an application.

noncomputable def Submodule.reflectionOperator {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] : E →L[𝕜] E

Reflection through an orthogonally complemented subspace.

Equations

• U.reflectionOperator = U.reflection.toLinearIsometry.toContinuousLinearMap

noncomputable def Submodule.diagonalPart {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] (A : E →L[𝕜] E) : E →L[𝕜] E

Diagonal part of an operator relative to U ⊕ Uᗮ.

Equations

• U.diagonalPart A = U.starProjection ∘SL A ∘SL U.starProjection + Uᗮ.starProjection ∘SL A ∘SL Uᗮ.starProjection

noncomputable def Submodule.offDiagonalPart {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] (A : E →L[𝕜] E) : E →L[𝕜] E

Off-diagonal part of an operator relative to U ⊕ Uᗮ.

Equations

• U.offDiagonalPart A = A - U.diagonalPart A

def Submodule.IsOffDiagonal {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] (A : E →L[𝕜] E) : Prop

The operator has vanishing diagonal blocks relative to U.

Equations

• U.IsOffDiagonal A = (U.diagonalPart A = 0)

theorem Submodule.diagonalPart_eq {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] (A : E →L[𝕜] E) : U.diagonalPart A = U.starProjection ∘SL A ∘SL U.starProjection + Uᗮ.starProjection ∘SL A ∘SL Uᗮ.starProjection

The diagonal part as a sum of two pinches. The definition is not exposed across module boundaries, so consumers rewrite with this.

theorem Submodule.offDiagonalPart_eq {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] (A : E →L[𝕜] E) : U.offDiagonalPart A = A - U.diagonalPart A

The off-diagonal part as the diagonal-part defect.

theorem Submodule.diagonalPart_apply {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] (A : E →L[𝕜] E) (x : E) : (U.diagonalPart A) x = U.starProjection (A (U.starProjection x)) + Uᗮ.starProjection (A (Uᗮ.starProjection x))

Pointwise form of the diagonal part.

theorem Submodule.offDiagonalPart_apply {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] (A : E →L[𝕜] E) (x : E) : (U.offDiagonalPart A) x = A x - (U.diagonalPart A) x

Pointwise form of the off-diagonal part.

@[simp]

theorem Submodule.reflectionOperator_apply {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] (x : E) : U.reflectionOperator x = 2 • U.starProjection x - x

Pointwise formula for reflection.

theorem Submodule.reflectionOperator_apply_of_mem {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] {x : E} (hx : x ∈ U) : U.reflectionOperator x = x

Reflection fixes the subspace it reflects through.

The pointwise formula gives 2 • P x - x, which is x exactly on U. Stated separately because the useful form is the fixed-point one: a compression whose input is restricted to U does not see the reflection at all.

theorem Submodule.reflectionOperator_apply_eq_reflection {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] (x : E) : U.reflectionOperator x = U.reflection x

The bundled reflection operator is Mathlib's Submodule.reflection. Stated because reflectionOperator is not exposed across module boundaries, so a consumer that needs the LinearIsometryEquiv -- to feed a naturality theorem that quantifies over unitaries, say -- cannot see that the two agree.

theorem Submodule.reflectionOperator_involutive {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] : U.reflectionOperator ∘SL U.reflectionOperator = ContinuousLinearMap.id 𝕜 E

Reflection is involutive.

theorem Submodule.reflectionOperator_eq_two_smul_sub_id {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] : U.reflectionOperator = 2 • U.starProjection - ContinuousLinearMap.id 𝕜 E

The reflection in operator form: J_U = 2 P_U - I.

The pointwise formula reflectionOperator_apply is what simp uses, but the two-projection algebra needs the operator identity, so that products of two reflections can be expanded by ring normalisation rather than by chasing vectors.

theorem Submodule.reflectionOperator_norm_map {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] (x : E) : ‖U.reflectionOperator x‖ = ‖x‖

Reflection preserves norms.

theorem Submodule.reflectionOperator_surjective {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] : Function.Surjective ⇑U.reflectionOperator

Reflection is onto.

theorem Submodule.norm_reflectionOperator_le_one {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] : ‖U.reflectionOperator‖ ≤ 1

Reflection has operator norm at most one.

theorem Submodule.reflectionOperator_comm_of_reduces {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (A : E →L[𝕜] E) (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] (hU : A.Reduces U) : U.reflectionOperator ∘SL A = A ∘SL U.reflectionOperator

A reducing operator commutes with the corresponding reflection.

theorem Submodule.starProjection_orthogonal_apply {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] (x : E) : Uᗮ.starProjection x = x - U.starProjection x

Complementary projection as I-P, pointwise.

theorem Submodule.two_smul_diagonalPart_eq_add_reflectionConjugate {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] (A : E →L[𝕜] E) : 2 • U.diagonalPart A = A + U.reflectionOperator ∘SL A ∘SL U.reflectionOperator

Twice the diagonal pinch is A + JAJ.

theorem Submodule.two_smul_offDiagonalPart_eq_sub_reflectionConjugate {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] (A : E →L[𝕜] E) : 2 • U.offDiagonalPart A = A - U.reflectionOperator ∘SL A ∘SL U.reflectionOperator

Twice the off-diagonal extraction is A-JAJ.

Numerical range of a block-diagonal operator

An operator that commutes with the reflection is determined block by block, and so is its numerical range: the quadratic form splits as a sum over U and Uᗮ with no cross term. Consequently a sign condition tested separately on the two summands propagates to the whole space. This is the mechanism by which "the diagonal blocks are positive" upgrades to "the numerical range is nonnegative"; it is what the two-projection literature uses to characterise the direct rotation among unitary square roots of the reflection product, and it is about projections only.

theorem Submodule.inner_diagonalPart_apply_self {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] (A : E →L[𝕜] E) (x : E) : inner 𝕜 ((U.diagonalPart A) x) x = inner 𝕜 (A (U.starProjection x)) (U.starProjection x) + inner 𝕜 (A (Uᗮ.starProjection x)) (Uᗮ.starProjection x)

The quadratic form of the diagonal pinch splits along U ⊕ Uᗮ.

⟪(P A P + P' A P') x, x⟫ = ⟪A (P x), P x⟫ + ⟪A (P' x), P' x⟫, each pinch term read off on its own summand. No hypothesis on A: the pinch is defined to discard the cross terms, and this identity says what survives.

theorem Submodule.diagonalPart_eq_self_of_reflectionConjugate {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] {A : E →L[𝕜] E} (hA : U.reflectionOperator ∘SL A ∘SL U.reflectionOperator = A) : U.diagonalPart A = A

Commuting with the reflection is the same as being block diagonal.

J A J = A forces A to equal its own diagonal pinch. Immediate from two_smul_diagonalPart_eq_add_reflectionConjugate, which says 2 (P A P + P' A P') = A + J A J.

theorem Submodule.re_inner_apply_self_nonneg_of_reflectionConjugate {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] {A : E →L[𝕜] E} (hA : U.reflectionOperator ∘SL A ∘SL U.reflectionOperator = A) (hU : ∀ x ∈ U, 0 ≤ RCLike.re (inner 𝕜 (A x) x)) (hUperp : ∀ x ∈ Uᗮ, 0 ≤ RCLike.re (inner 𝕜 (A x) x)) (x : E) : 0 ≤ RCLike.re (inner 𝕜 (A x) x)

A block-diagonal operator with nonnegative blocks has nonnegative numerical range.

The hypotheses only constrain A on U and on Uᗮ separately, which for a general operator says nothing about a mixed vector; commuting with the reflection is exactly what removes the cross term.