Minimal projections

In this file we show some necessary results for positive operators on a Hilbert space.

main results

Theorem. If $p,q$ are (orthogonal) projections on $E$, then the following are equivalent:

• (i) $pq = p = qp$
• (ii) $p(E) \subseteq q(E)$
• (iii) $q - p$ is an (orthogonal) projection
• (iv) $q - p$ is positive

for part (iii), it suffices to show that the element is an idempotent since $q - p$ is self-adjoint

it turns out that $qp = p$ (from (i)) if and only if (ii) and (i) if and only if (iii) for idempotent operators on a module over a ring (see IsIdempotentElem.comp_idempotent_iff and linear_map.commutes_iff_isIdempotent_elem)

obviously when $p,q$ are self-adjoint operators, then $pq = p$ iff $qp=p$ (see self_adjoint_commutes_iff)

so then, obviously, (ii) if and only if (iii) for idempotent self-adjoint operators as well (see continuous_linear_map.image_subset_iff_sub_of_is_idempotent)

we finally have (i) if and only if (iv) for idempotent self-adjoint operators on a finite-dimensional complex-Hilbert space: (see orthogonal_projection_is_positive_iff_commutes)

main definition

• an operator is non-negative means that it is positive: $0 \leq p$ if and only if $p$ is positive (see is_positive.is_nonneg)

theorem IsIdempotentElem.mem_range_iff {R : Type u_1} {E : Type u_2} [Ring R] [AddCommGroup E] [Module R E] {p : E →ₗ[R] E} (hp : IsIdempotentElem p) {x : E} : x ∈ LinearMap.range p ↔ p x = x

given an idempotent linear operator $p$, we have $x \in \textnormal{range}(p)$ if and only if $p(x) = x$ (for all $x \in E$)

theorem IsIdempotentElem.comp_idempotent_iff {R : Type u_2} {E : Type u_3} [Ring R] [AddCommGroup E] [Module R E] {q : E →ₗ[R] E} (hq : IsIdempotentElem q) {E₂ : Type u_1} [AddCommGroup E₂] [Module R E₂] (p : E₂ →ₗ[R] E) : q ∘ₗ p = p ↔ LinearMap.range p ≤ LinearMap.range q

given idempotent linear operators $p,q$, we have $qp = p$ iff $p(E) \subseteq q(E)$

theorem IsIdempotentElem.comp_idempotent_iff' {R : Type u_2} {E : Type u_3} [Ring R] [AddCommGroup E] [Module R E] {q : E →ₗ[R] E} (hq : IsIdempotentElem q) {E₂ : Type u_1} [AddCommGroup E₂] [Module R E₂] (p : E₂ →ₗ[R] E) : q ∘ₗ p = p ↔ Submodule.map p ⊤ ≤ Submodule.map q ⊤

theorem LinearMap.isIdempotentElem_sub_of {R : Type u_2} {E : Type u_1} [Ring R] [AddCommGroup E] [Module R E] {q : E →ₗ[R] E} (hq : IsIdempotentElem q) {p : E →ₗ[R] E} (hp : IsIdempotentElem p) (h : p ∘ₗ q = p ∧ q ∘ₗ p = p) : IsIdempotentElem (q - p)

if $p,q$ are idempotent operators and $pq = p = qp$, then $q - p$ is an idempotent operator

theorem LinearMap.commutes_of_isIdempotentElem {E : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] {p : E →ₗ[𝕜] E} {q : E →ₗ[𝕜] E} (hp : IsIdempotentElem p) (hq : IsIdempotentElem q) (h : IsIdempotentElem (q - p)) : p ∘ₗ q = p ∧ q ∘ₗ p = p

if $p,q$ are idempotent operators and $q - p$ is also an idempotent operator, then $pq = p = qp$

theorem LinearMap.commutes_iff_isIdempotentElem {E : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] {p : E →ₗ[𝕜] E} {q : E →ₗ[𝕜] E} (hp : IsIdempotentElem p) (hq : IsIdempotentElem q) : p ∘ₗ q = p ∧ q ∘ₗ p = p ↔ IsIdempotentElem (q - p)

given idempotent operators $p,q$, we have $pq = p = qp$ iff $q - p$ is an idempotent operator

theorem self_adjoint_proj_commutes {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {p : E →L[𝕜] E} {q : E →L[𝕜] E} (hpa : IsSelfAdjoint p) (hqa : IsSelfAdjoint q) : p.comp q = p ↔ q.comp p = p

given self-adjoint operators $p,q$, we have $pq=p$ iff $qp=p$

theorem orthogonalProjection.isIdempotentElem {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) [HasOrthogonalProjection U] : IsIdempotentElem (orthogonalProjection' U)

class ContinuousLinearMap.IsOrthogonalProjection {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (T : E →L[𝕜] E) : Prop

• isIdempotent : IsIdempotentElem T
• kerEqRangeOrtho : LinearMap.ker T = (LinearMap.range T)ᗮ

theorem ContinuousLinearMap.IsOrthogonalProjection.isIdempotent {𝕜 : Type u_1} {E : Type u_2} : ∀ {inst : RCLike 𝕜} {inst_1 : NormedAddCommGroup E} {inst_2 : InnerProductSpace 𝕜 E} {T : E →L[𝕜] E} [self : T.IsOrthogonalProjection], IsIdempotentElem T

theorem ContinuousLinearMap.IsOrthogonalProjection.kerEqRangeOrtho {𝕜 : Type u_1} {E : Type u_2} : ∀ {inst : RCLike 𝕜} {inst_1 : NormedAddCommGroup E} {inst_2 : InnerProductSpace 𝕜 E} {T : E →L[𝕜] E} [self : T.IsOrthogonalProjection], LinearMap.ker T = (LinearMap.range T)ᗮ

theorem ContinuousLinearMap.IsOrthogonalProjection.eq {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →L[𝕜] E} (hT : T.IsOrthogonalProjection) : IsIdempotentElem T ∧ LinearMap.ker T = (LinearMap.range T)ᗮ

theorem IsIdempotentElem.clm_to_lm {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →L[𝕜] E} : IsIdempotentElem T ↔ IsIdempotentElem ↑T

theorem ContinuousLinearMap.HasOrthogonalProjection_of_isOrthogonalProjection {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →L[𝕜] E} [h : T.IsOrthogonalProjection] : HasOrthogonalProjection (LinearMap.range T)

theorem ker_to_clm {R : Type u_1} {R₂ : Type u_2} {M : Type u_3} {M₂ : Type u_4} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [TopologicalSpace M] [TopologicalSpace M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} (f : M →SL[τ₁₂] M₂) : LinearMap.ker ↑f = LinearMap.ker f

theorem subtype_compL_ker {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) (f : E →L[𝕜] ↥U) : LinearMap.ker (U.subtypeL.comp f) = LinearMap.ker f

theorem orthogonalProjection.isOrthogonalProjection {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) [h : HasOrthogonalProjection U] : (orthogonalProjection' U).IsOrthogonalProjection

theorem IsIdempotentElem.isCompl_range_ker {V : Type u_1} {R : Type u_2} [Semiring R] [AddCommGroup V] [Module R V] {T : V →ₗ[R] V} (h : IsIdempotentElem T) : IsCompl (LinearMap.ker T) (LinearMap.range T)

given any idempotent operator $T ∈ L(V)$, then is_compl T.ker T.range, in other words, there exists unique $v ∈ \textnormal{ker}(T)$ and $w ∈ \textnormal{range}(T)$ such that $x = v + w$

theorem IsCompl.of_orthogonal_projection {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →L[𝕜] E} (h : T.IsOrthogonalProjection) : IsCompl (LinearMap.ker T) (LinearMap.range T)

@[simp]

theorem orthogonalProjection.ker {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} [HasOrthogonalProjection K] : LinearMap.ker (orthogonalProjection' K) = Kᗮ

theorem LinearMap.isIdempotentElem_of_isProj {V : Type u_1} {R : Type u_2} [Semiring R] [AddCommGroup V] [Module R V] {T : V →ₗ[R] V} {U : Submodule R V} (h : LinearMap.IsProj U T) : IsIdempotentElem T

theorem sub_of_isOrthogonalProjection {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] {U : Submodule ℂ E} {V : Submodule ℂ E} [CompleteSpace ↥U] [CompleteSpace ↥V] : (orthogonalProjection' V).comp (orthogonalProjection' U) = orthogonalProjection' U ↔ (orthogonalProjection' V - orthogonalProjection' U).IsOrthogonalProjection

$P_V P_U = P_U$ if and only if $P_V - P_U$ is an orthogonal projection

instance LinearMap.IsSymmetric.hasLe {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] : LE (E →ₗ[𝕜] E)

instance for ≤ on linear maps

Equations

• LinearMap.IsSymmetric.hasLe = { le := fun (u v : E →ₗ[𝕜] E) => (v - u).IsPositive }

@[reducible]

def SymmetricLM (g : Type u_1) [NormedAddCommGroup g] [InnerProductSpace ℂ g] : Set (g →ₗ[ℂ] g)

Equations

• SymmetricLM g = {x : g →ₗ[ℂ] g | x.IsSymmetric}

@[reducible]

def SelfAdjointCLM (g : Type u_1) [NormedAddCommGroup g] [InnerProductSpace ℂ g] [CompleteSpace g] : Set (g →L[ℂ] g)

Equations

• SelfAdjointCLM g = {x : g →L[ℂ] g | IsSelfAdjoint x}

instance instPartialOrderLinearMapId_monlib {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] : PartialOrder (E →ₗ[𝕜] E)

Equations

• instPartialOrderLinearMapId_monlib = PartialOrder.mk ⋯

theorem LinearMap.IsPositive.hasLe {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {p : ↑(SymmetricLM E)} {q : ↑(SymmetricLM E)} : p ≤ q ↔ (↑q - ↑p).IsPositive

p ≤ q means q - p is positive

noncomputable instance IsSymmetric.hasZero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] : Zero ↑{x : E →ₗ[ℂ] E | x.IsSymmetric}

Equations

• IsSymmetric.hasZero = { zero := ⟨0, ⋯⟩ }

theorem LinearMap.IsPositive.is_nonneg {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {p : E →ₗ[𝕜] E} : p.IsPositive ↔ 0 ≤ p

saying p is positive is the same as saying 0 ≤ p

theorem SelfAdjointAndIdempotent.is_positive {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {p : E →L[𝕜] E} (hp : IsIdempotentElem p) (hpa : IsSelfAdjoint p) : 0 ≤ p

a self-adjoint idempotent operator is positive

theorem IsIdempotentElem.is_positive_iff_self_adjoint {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {p : E →L[𝕜] E} (hp : IsIdempotentElem p) : 0 ≤ p ↔ IsSelfAdjoint p

an idempotent is positive if and only if it is self-adjoint

theorem IsIdempotentElem.self_adjoint_is_positive_isOrthogonalProjection_tFAE {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] {p : E →L[ℂ] E} (hp : IsIdempotentElem p) : [IsSelfAdjoint p, p.IsOrthogonalProjection, 0 ≤ p].TFAE

theorem orthogonalProjection.is_positive {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {U : Submodule ℂ E} [CompleteSpace E] [CompleteSpace ↥U] : 0 ≤ U.subtypeL.comp (orthogonalProjection U)

orthogonal projections are obviously positive

theorem SelfAdjointAndIdempotent.sub_is_positive_of {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {p : E →L[𝕜] E} {q : E →L[𝕜] E} (hp : IsIdempotentElem p) (hq : IsIdempotentElem q) (hpa : IsSelfAdjoint p) (hqa : IsSelfAdjoint q) (h : p.comp q = p) : 0 ≤ q - p

theorem orthogonalProjection.sub_is_positive_of {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {U : Submodule ℂ E} {V : Submodule ℂ E} [CompleteSpace ↥U] [CompleteSpace ↥V] [CompleteSpace E] (h : (orthogonalProjection' U).comp (orthogonalProjection' V) = orthogonalProjection' U) : 0 ≤ orthogonalProjection' V - orthogonalProjection' U

given orthogonal projections Pᵤ,Pᵥ, then Pᵤ(Pᵥ)=Pᵤ implies Pᵥ-Pᵤ is positive (i.e., Pᵤ ≤ Pᵥ)

theorem orthogonal_projection_commutes_of_is_idempotent {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {U : Submodule ℂ E} {V : Submodule ℂ E} [CompleteSpace ↥U] [CompleteSpace ↥V] [CompleteSpace E] (h : IsIdempotentElem (orthogonalProjection' V - orthogonalProjection' U)) : (orthogonalProjection' V).comp (orthogonalProjection' U) = orthogonalProjection' U

given orthogonal projections Pᵤ,Pᵥ, then if Pᵥ - Pᵤ is idempotent, then Pᵤ Pᵥ = Pᵤ

theorem ContinuousLinearMap.isPositive_iff_exists_adjoint_hMul_self {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (T : E →L[𝕜] E) : T.IsPositive ↔ ∃ (S : E →L[𝕜] E), T = ContinuousLinearMap.adjoint S * S

copy of linear_map.is_positive_iff_exists_adjoint_mul_self

theorem ContinuousLinearMap.is_positive_le_iff_inner {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {p : E →L[𝕜] E} {q : E →L[𝕜] E} (hpa : IsSelfAdjoint p) (hqa : IsSelfAdjoint q) : p ≤ q ↔ ∀ (x : E), RCLike.re (inner x (p x)) ≤ RCLike.re (inner x (q x))

in a finite-dimensional complex Hilbert space E, if p,q are self-adjoint operators, then p ≤ q iff ∀ x ∈ E : ⟪x, p x⟫ ≤ ⟪x, q x⟫

theorem ContinuousLinearMap.hasLe_norm {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {p : E →L[𝕜] E} {q : E →L[𝕜] E} (hp : IsIdempotentElem p) (hq : IsIdempotentElem q) (hpa : IsSelfAdjoint p) (hqa : IsSelfAdjoint q) : (∀ (x : E), RCLike.re (inner x (p x)) ≤ RCLike.re (inner x (q x))) ↔ ∀ (x : E), ‖p x‖ ≤ ‖q x‖

given self-adjoint idempotent operators p,q, we have ∀ x ∈ E : ⟪x, p x⟫ ≤ ⟪x, q x⟫ ↔ ∀ x ∈ E, ‖p x‖ ≤ ‖q x‖

@[simp]

theorem IsPositive.HasLe.sub {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {p : E →L[𝕜] E} {q : E →L[𝕜] E} : p ≤ q ↔ 0 ≤ q - p

theorem self_adjoint_and_idempotent_is_positive_iff_commutes {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] {p : E →L[ℂ] E} {q : E →L[ℂ] E} (hp : IsIdempotentElem p) (hq : IsIdempotentElem q) (hpa : IsSelfAdjoint p) (hqa : IsSelfAdjoint q) : p ≤ q ↔ q.comp p = p

theorem orthogonal_projection_is_le_iff_commutes {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {U : Submodule ℂ E} {V : Submodule ℂ E} [CompleteSpace E] [CompleteSpace ↥U] [CompleteSpace ↥V] : orthogonalProjection' U ≤ orthogonalProjection' V ↔ (orthogonalProjection' V).comp (orthogonalProjection' U) = orthogonalProjection' U

in a complex-finite-dimensional Hilbert space E, we have Pᵤ ≤ Pᵤ iff PᵥPᵤ = Pᵤ

theorem orthogonalProjection.is_le_iff_subset {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {U : Submodule ℂ E} {V : Submodule ℂ E} [CompleteSpace E] [CompleteSpace ↥U] [CompleteSpace ↥V] : orthogonalProjection' U ≤ orthogonalProjection' V ↔ U ≤ V

theorem Submodule.map_to_linearMap {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [Module 𝕜 E] {p : E →L[𝕜] E} {U : Submodule 𝕜 E} : Submodule.map (↑p) U = Submodule.map p U

theorem ContinuousLinearMap.image_subset_iff_sub_of_is_idempotent {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {p : E →L[𝕜] E} {q : E →L[𝕜] E} (hp : IsIdempotentElem p) (hq : IsIdempotentElem q) (hpa : IsSelfAdjoint p) (hqa : IsSelfAdjoint q) : LinearMap.range p ≤ LinearMap.range q ↔ IsIdempotentElem (q - p)

given self-adjoint idempotent operators p,q we have, p(E) ⊆ q(E) iff q - p is an idempotent operator

def ContinuousLinearMap.IsMinimalProjection {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (x : E →L[𝕜] E) (U : Submodule 𝕜 E) : Prop

definition of a map being a minimal projection

Equations

• x.IsMinimalProjection U = (IsSelfAdjoint x ∧ Module.finrank 𝕜 ↥U = 1 ∧ LinearMap.IsProj U x)

def orthogonalProjection.IsMinimalProjection {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) [CompleteSpace ↥U] : Prop

definition of orthogonal projection being minimal i.e., when the dimension of its space equals one

Equations

• orthogonalProjection.IsMinimalProjection U = (Module.finrank 𝕜 ↥U = 1)

theorem Submodule.le_finrank_one {R : Type u_1} {M : Type u_2} [Field R] [AddCommGroup M] [Module R M] (U : Submodule R M) (V : Submodule R M) [Module.Finite R ↥U] [Module.Finite R ↥V] (hU : Module.finrank R ↥U = 1) : V ≤ U ↔ V = U ∨ V = 0

when a submodule U has dimension 1, then for any submodule V, we have V ≤ U if and only if V = U or V = 0

theorem orthogonalProjection.isMinimalProjection_of {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (U : Submodule ℂ E) (W : Submodule ℂ E) [Module.Finite ℂ ↥U] [Module.Finite ℂ ↥W] (hU : orthogonalProjection.IsMinimalProjection U) (hW : orthogonalProjection' W ≤ orthogonalProjection' U) (h : orthogonalProjection' W ≠ 0) : orthogonalProjection' W = orthogonalProjection' U

for orthogonal projections Pᵤ,Pᵥ, if Pᵤ is a minimal orthogonal projection, then for any Pᵥ if Pᵥ ≤ Pᵤ and Pᵥ ≠ 0, then Pᵥ = Pᵤ

theorem rankOne_self_isMinimalProjection {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] {x : E} (h : ‖x‖ = 1) : (((rankOne ℂ) x) x).IsMinimalProjection (Submodule.span ℂ {x})

any rank one operator given by a norm one vector is a minimal projection

theorem normalize_op {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (x : E) : (∃ (y : E) (r : ℝ), ‖y‖ = 1 ∧ x = ↑r • y) ∨ x = 0

if x ∈ E then we can normalize this (i.e., there exists y ∈ E such that ∥y∥ = 1 where x = r • y for some r ∈ ℝ) unless x = 0

theorem rankOne_self_isMinimalProjection' {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] {x : E} (h : x ≠ 0) : ((1 / ‖x‖ ^ 2) • ((rankOne ℂ) x) x).IsMinimalProjection (Submodule.span ℂ {x})

given any non-zero x ∈ E, we have 1 / ‖x‖ ^ 2 • |x⟩⟨x| is a minimal projection

theorem LinearMap.range_of_isProj {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommGroup M] [Module R M] {p : M →ₗ[R] M} {U : Submodule R M} (hp : LinearMap.IsProj U p) : LinearMap.range p = U

theorem orthogonal_projection_iff {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {p : E →L[𝕜] E} : (∃ (U : Submodule 𝕜 E), orthogonalProjection' U = p) ↔ IsSelfAdjoint p ∧ IsIdempotentElem p

a linear operator is an orthogonal projection onto a submodule, if and only if it is self-adjoint and idempotent; so it always suffices to say p = p⋆ = p²

theorem orthogonal_projection_iff' {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {p : E →L[𝕜] E} (U : Submodule 𝕜 E) : orthogonalProjection' U = p ↔ IsSelfAdjoint p ∧ LinearMap.IsProj U p

a linear operator is an orthogonal projection onto a submodule, if and only if it is a self-adjoint linear projection onto the submodule; also see orthogonal_projection_iff

theorem orthogonalProjection.isMinimalProjection_to_clm {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (U : Submodule 𝕜 E) : (orthogonalProjection' U).IsMinimalProjection U ↔ orthogonalProjection.IsMinimalProjection U

theorem Submodule.isOrtho_iff_inner_eq' {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {U : Submodule 𝕜 E} {W : Submodule 𝕜 E} : U ⟂ W ↔ ∀ (u : ↥U) (w : ↥W), inner ↑u ↑w = 0

theorem Submodule.is_pairwise_orthogonal_iff_orthogonal_projection_comp_eq_zero {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) (W : Submodule 𝕜 E) [HasOrthogonalProjection U] [HasOrthogonalProjection W] : U ⟂ W ↔ (orthogonalProjection' U).comp (orthogonalProjection' W) = 0

U and W are mutually orthogonal if and only if (P U).comp (P W) = 0, where P U is orthogonal_projection U

theorem orthogonalProjection.orthogonal_complement_eq {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) [HasOrthogonalProjection U] : orthogonalProjection' Uᗮ = 1 - orthogonalProjection' U

theorem ContinuousLinearMap.isOrthogonalProjection_iff {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (T : E →L[𝕜] E) : T.IsOrthogonalProjection ↔ IsIdempotentElem T ∧ LinearMap.ker T = (LinearMap.range T)ᗮ

theorem ContinuousLinearMap.isOrthogonalProjection_iff' {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [FiniteDimensional ℂ E] {p : E →L[ℂ] E} : p.IsOrthogonalProjection ↔ IsIdempotentElem p ∧ IsSelfAdjoint p

theorem LinearMap.isSelfAdjoint_toContinuousLinearMap {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (f : E →ₗ[𝕜] E) : IsSelfAdjoint (LinearMap.toContinuousLinearMap f) ↔ IsSelfAdjoint f

theorem LinearMap.isOrthogonalProjection_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [FiniteDimensional ℂ E] (T : E →ₗ[ℂ] E) : (LinearMap.toContinuousLinearMap T).IsOrthogonalProjection ↔ IsIdempotentElem T ∧ IsSelfAdjoint T

theorem lmul_isIdempotentElem_iff {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] (a : A) : IsIdempotentElem (lmul a) ↔ IsIdempotentElem a

theorem lmul_tmul {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Semiring B] [Module R A] [Module R B] [SMulCommClass R A A] [SMulCommClass R B B] [IsScalarTower R A A] [IsScalarTower R B B] (a : A) (b : B) : lmul (a ⊗ₜ[R] b) = TensorProduct.map (lmul a) (lmul b)

theorem lmul_eq_lmul_iff {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] (a : A) (b : A) : lmul a = lmul b ↔ a = b

theorem isIdempotentElem_algEquiv_iff {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (φ : A ≃ₐ[R] B) (a : A) : IsIdempotentElem (φ a) ↔ IsIdempotentElem a

theorem orthogonalProjection'_isProj {R : Type u_1} {M : Type u_2} [RCLike R] [NormedAddCommGroup M] [InnerProductSpace R M] (U : Submodule R M) [HasOrthogonalProjection U] : LinearMap.IsProj U (orthogonalProjection' U)

theorem LinearMap.isProj_iff {S : Type u_1} {M : Type u_2} {F : Type u_3} [Semiring S] [AddCommMonoid M] [Module S M] (m : Submodule S M) [FunLike F M M] (f : F) : LinearMap.IsProj m f ↔ (∀ (x : M), f x ∈ m) ∧ ∀ x ∈ m, f x = x

theorem LinearMap.isProj_coe {R : Type u_1} {M : Type u_2} [RCLike R] [NormedAddCommGroup M] [InnerProductSpace R M] (T : M →L[R] M) (U : Submodule R M) : LinearMap.IsProj U ↑T ↔ LinearMap.IsProj U T

theorem orthogonalProjection_trace {R : Type u_1} {M : Type u_2} [RCLike R] [NormedAddCommGroup M] [InnerProductSpace R M] [FiniteDimensional R M] (U : Submodule R M) : (LinearMap.trace R M) ↑(orthogonalProjection' U) = ↑(Module.finrank R ↥U)

theorem ContinuousLinearMap.eq_comp_orthogonalProjection_ker_ortho {𝕜 : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} [RCLike 𝕜] [NormedAddCommGroup M₁] [InnerProductSpace 𝕜 M₁] [NormedAddCommGroup M₂] [InnerProductSpace 𝕜 M₂] {T : M₁ →L[𝕜] M₂} [HasOrthogonalProjection (LinearMap.ker T)] [HasOrthogonalProjection (LinearMap.range T)] [CompleteSpace M₁] [CompleteSpace M₂] : T = T.comp (orthogonalProjection' (LinearMap.ker T)ᗮ) ∧ T = (orthogonalProjection' (LinearMap.range T)).comp T

theorem orthogonalProjection_of_top {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace ↥⊤] : orthogonalProjection' ⊤ = 1

theorem LinearMap.IsProj.top (S : Type u_1) (M : Type u_2) [Semiring S] [AddCommMonoid M] [Module S M] : LinearMap.IsProj ⊤ LinearMap.id

theorem LinearMap.IsProj.codRestrict_of_top {S : Type u_1} {M : Type u_2} [Semiring S] [AddCommMonoid M] [Module S M] : ⊤.subtype ∘ₗ ⋯.codRestrict = LinearMap.id

theorem LinearMap.IsProj.subtype_comp_codRestrict {S : Type u_1} {M : Type u_2} [Semiring S] [AddCommMonoid M] [Module S M] {U : Submodule S M} {f : M →ₗ[S] M} (hf : LinearMap.IsProj U f) : U.subtype ∘ₗ hf.codRestrict = f

theorem LinearMap.IsProj.codRestrict_eq_dim_iff {S : Type u_1} {M : Type u_2} [Semiring S] [AddCommMonoid M] [Module S M] {f : M →ₗ[S] M} {U : Submodule S M} (hf : LinearMap.IsProj U f) : U = ⊤ ↔ U.subtype ∘ₗ hf.codRestrict = LinearMap.id