English
For an idempotent operator p, the following list is equivalent: range-ker orthogonality, normality, self-adjointness, and positivity.
Русский
Для идемпотентного оператора p перечисленные свойства: ортогональное отношение между диапазоном и ядром, нормальность, самопряжённость и положительность — эквивалентны.
LaTeX
$$$[\text{range-ker orthogonality}, \text{normal}, \text{self-adjoint}, \text{positive}].\text{TFAE}$$$
Lean4
/-- For an idempotent operator `p`, TFAE:
* `(range p)ᗮ = ker p`
* `p` is normal
* `p` is self-adjoint
* `p` is positive -/
theorem TFAE {p : E →L[𝕜] E} (hp : IsIdempotentElem p) :
[(LinearMap.range p)ᗮ = LinearMap.ker p, IsStarNormal p, IsSelfAdjoint p, p.IsPositive].TFAE :=
by
tfae_have 2 ↔ 3 := hp.isSelfAdjoint_iff_isStarNormal.symm
tfae_have 3 ↔ 4 := hp.isPositive_iff_isSelfAdjoint.symm
tfae_have 3 ↔ 1 :=
p.isSelfAdjoint_iff_isSymmetric.eq ▸ (ContinuousLinearMap.IsIdempotentElem.isSymmetric_iff_orthogonal_range hp)
tfae_finish
