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)
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$)
given idempotent linear operators $p,q$, we have $qp = p$ iff $p(E) \subseteq q(E)$
if $p,q$ are idempotent operators and $pq = p = qp$, then $q - p$ is an idempotent operator
if $p,q$ are idempotent operators and $q - p$ is also an idempotent operator, then $pq = p = qp$
given idempotent operators $p,q$, we have $pq = p = qp$ iff $q - p$ is an idempotent operator
given self-adjoint operators $p,q$, we have $pq=p$ iff $qp=p$
- isIdempotent : IsIdempotentElem T
Instances
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$
$P_V P_U = P_U$ if and only if $P_V - P_U$ is an orthogonal projection
instance for ≤ on linear maps
Equations
- LinearMap.IsSymmetric.hasLe = { le := fun (u v : E →ₗ[𝕜] E) => (v - u).IsPositive }
Equations
- SelfAdjointCLM g = {x : g →L[ℂ] g | IsSelfAdjoint x}
Instances For
Equations
p ≤ q means q - p is positive
Equations
- IsSymmetric.hasZero = { zero := ⟨0, ⋯⟩ }
saying p is positive is the same as saying 0 ≤ p
a self-adjoint idempotent operator is positive
an idempotent is positive if and only if it is self-adjoint
orthogonal projections are obviously positive
given orthogonal projections Pᵤ,Pᵥ,
then Pᵤ(Pᵥ)=Pᵤ implies Pᵥ-Pᵤ is positive (i.e., Pᵤ ≤ Pᵥ)
given orthogonal projections Pᵤ,Pᵥ,
then if Pᵥ - Pᵤ is idempotent, then Pᵤ Pᵥ = Pᵤ
copy of linear_map.is_positive_iff_exists_adjoint_mul_self
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⟫
given self-adjoint idempotent operators p,q, we have
∀ x ∈ E : ⟪x, p x⟫ ≤ ⟪x, q x⟫ ↔ ∀ x ∈ E, ‖p x‖ ≤ ‖q x‖
in a complex-finite-dimensional Hilbert space E, we have
Pᵤ ≤ Pᵤ iff PᵥPᵤ = Pᵤ
given self-adjoint idempotent operators p,q we have,
p(E) ⊆ q(E) iff q - p is an idempotent operator
definition of a map being a minimal projection
Equations
- x.IsMinimalProjection U = (IsSelfAdjoint x ∧ Module.finrank 𝕜 ↥U = 1 ∧ LinearMap.IsProj U x)
Instances For
definition of orthogonal projection being minimal i.e., when the dimension of its space equals one
Equations
- orthogonalProjection.IsMinimalProjection U = (Module.finrank 𝕜 ↥U = 1)
Instances For
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
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ᵤ
any rank one operator given by a norm one vector is a minimal projection
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
given any non-zero x ∈ E, we have
1 / ‖x‖ ^ 2 • |x⟩⟨x| is a minimal projection
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²
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
U and W are mutually orthogonal if and only if (P U).comp (P W) = 0,
where P U is orthogonal_projection U