English
For an idempotent operator T, T is self-adjoint if and only if T is normal.
Русский
Для идемпотентного оператора T верно: T самосопряжён тогда и только тогда, когда T нормален.
LaTeX
$$$\\text{IsIdempotentElem}(T) \\;\\Rightarrow\\; (\\text{IsSelfAdjoint}(T) \\iff \\text{IsStarNormal}(T))$$$
Lean4
/-- An idempotent operator is self-adjoint iff it is normal. -/
theorem isSelfAdjoint_iff_isStarNormal (hT : IsIdempotentElem T) : IsSelfAdjoint T ↔ IsStarNormal T :=
by
refine ⟨fun h => by rw [isStarNormal_iff, h], fun h => ?_⟩
suffices T = star T * T from this ▸ IsSelfAdjoint.star_mul_self _
rw [← sub_eq_zero, ContinuousLinearMap.ext_iff]
simp_rw [zero_apply, ← norm_eq_zero (E := E)]
have :=
calc
(∀ x : E, ‖(T - star T * T) x‖ = 0) ↔ ∀ x, ‖(adjoint (1 - T)) (T x)‖ = 0 := by
simp [coe_sub', coe_mul, Pi.sub_apply, Function.comp_apply, norm_eq_zero, ← star_eq_adjoint, star_sub, star_one,
one_apply]
_ ↔ ∀ x, ‖(1 - T) (T x)‖ = 0 := by simp only [isStarNormal_iff_norm_eq_adjoint.mp h.one_sub]
_ ↔ ∀ x, ‖(T - T * T) x‖ = 0 := by simp
_ ↔ T - T * T = 0 := by simp only [norm_eq_zero, ContinuousLinearMap.ext_iff, zero_apply]
_ ↔ IsIdempotentElem T := by simp only [sub_eq_zero, IsIdempotentElem, eq_comm]
exact this.mpr hT
