English
For an idempotent operator p, the following are equivalent: (i) the orthogonal complement of the range of p equals the kernel of p; (ii) p is normal; (iii) p is self-adjoint; (iv) p is positive.
Русский
Для идемпотентного оператора p равны эквивалентны: (i) ортогональное дополнение диапазона p равно ядру p; (ii) p нормален; (iii) p самопряжён; (iv) p положителен.
LaTeX
$$$\big( (\operatorname{range} p)^{\perp} = \ker p \big) \;\iff\; IsStarNormal(p) \;\iff\; IsSelfAdjoint(p) \;\iff\; p.IsPositive$$$
Lean4
/-- A star projection operator is positive.
The proof of this will soon be simplified to `IsStarProjection.nonneg` when we
have `StarOrderedRing (E →L[𝕜] E)`. -/
@[aesop 10% apply, grind →]
theorem of_isStarProjection {p : E →L[𝕜] E} (hp : IsStarProjection p) : p.IsPositive :=
hp.isIdempotentElem.isPositive_iff_isSelfAdjoint.mpr hp.isSelfAdjoint
