English
If A is self-adjoint, then A is symmetric as a linear map over E.
Русский
Если A самосопряжён, то A симметричен как линейное отображение на E.
LaTeX
$$IsSelfAdjoint A \Rightarrow (A : E \to_𝕜 E).IsSymmetric$$
Lean4
theorem norm_adjoint_comp_self (A : E →L[𝕜] F) : ‖A† ∘L A‖ = ‖A‖ * ‖A‖ :=
by
refine le_antisymm ?_ ?_
·
calc
‖A† ∘L A‖ ≤ ‖A†‖ * ‖A‖ := opNorm_comp_le _ _
_ = ‖A‖ * ‖A‖ := by rw [LinearIsometryEquiv.norm_map]
· rw [← sq, ← Real.sqrt_le_sqrt_iff (norm_nonneg _), Real.sqrt_sq (norm_nonneg _)]
refine opNorm_le_bound _ (Real.sqrt_nonneg _) fun x => ?_
have :=
calc
re ⟪(A† ∘L A) x, x⟫ ≤ ‖(A† ∘L A) x‖ * ‖x‖ := re_inner_le_norm _ _
_ ≤ ‖A† ∘L A‖ * ‖x‖ * ‖x‖ := mul_le_mul_of_nonneg_right (le_opNorm _ _) (norm_nonneg _)
calc
‖A x‖ = √(re ⟪(A† ∘L A) x, x⟫) := by rw [apply_norm_eq_sqrt_inner_adjoint_left]
_ ≤ √(‖A† ∘L A‖ * ‖x‖ * ‖x‖) := (Real.sqrt_le_sqrt this)
_ = √‖A† ∘L A‖ * ‖x‖ := by
simp_rw [mul_assoc, Real.sqrt_mul (norm_nonneg _) (‖x‖ * ‖x‖), Real.sqrt_mul_self (norm_nonneg x)]
