theorem ContinuousLinearMap.norm_adjoint_eq {H : Type u} {K : Type v} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] [NormedAddCommGroup K] [InnerProductSpace ℝ K] [CompleteSpace K] (T : H →L[ℝ] K) : ‖adjoint T‖ = ‖T‖

Fact 2.25: taking adjoints preserves the operator norm.

theorem ContinuousLinearMap.norm_eq_sqrt_norm_adjoint_comp {H : Type u} {K : Type v} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] [NormedAddCommGroup K] [InnerProductSpace ℝ K] [CompleteSpace K] (T : H →L[ℝ] K) : ‖T‖ = √‖adjoint T ∘SL T‖

Fact 2.25: the operator norm is the square root of the norm of the Gram operator T†T.

theorem ContinuousLinearMap.closure_range_self_comp_adjoint {H : Type u} {K : Type v} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] [NormedAddCommGroup K] [InnerProductSpace ℝ K] [CompleteSpace K] (T : H →L[ℝ] K) : (↑(T ∘SL adjoint T)).range.topologicalClosure = (↑T).range.topologicalClosure

Fact 2.25: the closures of the ranges of TT† and T coincide.

theorem ContinuousLinearMap.orthogonal_hilbertGraph {H : Type u} {K : Type v} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] [NormedAddCommGroup K] [InnerProductSpace ℝ K] [CompleteSpace K] (T : H →L[ℝ] K) : (Submodule.map (↑(WithLp.linearEquiv 2 ℝ (H × K)).symm) (↑T).graph)ᗮ = (↑(WithLp.fstL 2 ℝ H K + adjoint T ∘SL WithLp.sndL 2 ℝ H K)).ker

Fact 2.25: in the Hilbert direct sum H ⊕ K, the orthogonal complement of the graph of T is the kernel of the canonical graph map fst + T† ∘ snd.

theorem IsSelfAdjoint.norm_eq_sSup_abs_inner_closedBall {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {T : H →L[ℝ] H} (hT : IsSelfAdjoint T) : ‖T‖ = sSup ((fun (x : H) => |inner ℝ (T x) x|) '' Metric.closedBall 0 1)

For a self-adjoint operator, the norm is the supremum of the quadratic form on the unit ball.