English
An operator T is normal if and only if for every vector v, the norms satisfy ‖T v‖ = ‖adjoint T v‖.
Русский
Оператор T нормален тогда и только тогда, когда для каждого вектора v выполняется тождество норм: ‖Tv‖ = ‖T* v‖.
LaTeX
$$$\\text{IsStarNormal}(T) \\iff \\forall v\\in E, \\|T v\\| = \\|\\operatorname{adjoint}(T) v\\|$$$
Lean4
/-- An operator `T` is normal iff `‖T v‖ = ‖(adjoint T) v‖` for all `v`. -/
theorem isStarNormal_iff_norm_eq_adjoint : IsStarNormal T ↔ ∀ v : E, ‖T v‖ = ‖adjoint T v‖ :=
by
rw [isStarNormal_iff, Commute, SemiconjBy, ← sub_eq_zero]
simp_rw [ContinuousLinearMap.ext_iff, ← coe_coe, coe_sub, ← LinearMap.ext_iff, coe_zero]
have :=
star_eq_adjoint T ▸
coe_sub (star _ * T) _ ▸ ((IsSelfAdjoint.star_mul_self T).sub (IsSelfAdjoint.mul_star_self T)).isSymmetric
simp_rw [star_eq_adjoint, ← LinearMap.IsSymmetric.inner_map_self_eq_zero this, LinearMap.sub_apply, inner_sub_left,
coe_coe, mul_apply, adjoint_inner_left, inner_self_eq_norm_sq_to_K, ← adjoint_inner_right T,
inner_self_eq_norm_sq_to_K, sub_eq_zero, ← sq_eq_sq₀ (norm_nonneg _) (norm_nonneg _)]
norm_cast
