Elementary inequalities for positive operators

For a positive operator T on a possibly infinite-dimensional Hilbert space, 1 + T is invertible (ContinuousLinearMap.IsPositive.isUnit_one_add), because re ⟪(1 + T) x, x⟫ ≥ ‖x‖² bounds it below. This applies in particular to T = X†X, which makes (1 + X†X)⁻¹ available in formulas such as the orthogonal projection onto a graph subspace.

The quadratic form of a positive endomorphism A controls its off-diagonal entries, 2 re ⟪x, A y⟫ ≤ re ⟪x, A x⟫ + re ⟪y, A y⟫ (LinearMap.IsPositive.two_mul_re_inner_le), and on a finite-dimensional space the diagonal entries along any orthonormal family sum to at most the trace (LinearMap.IsPositive.sum_re_inner_le_re_trace). These are the inputs to Ky Fan's maximum principle for positive operators.

A contraction between real or complex Hilbert spaces satisfies D D† ≤ 1 in the Loewner order (ContinuousLinearMap.self_comp_adjoint_le_one), so its defect operator 1 - D D† is positive.

theorem LinearMap.IsPositive.two_mul_re_inner_le {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {A : E →ₗ[𝕜] E} (hA : A.IsPositive) (x y : E) : 2 * RCLike.re (inner 𝕜 x (A y)) ≤ RCLike.re (inner 𝕜 x (A x)) + RCLike.re (inner 𝕜 y (A y))

For a positive endomorphism A, 2 re ⟪x, A y⟫ ≤ re ⟪x, A x⟫ + re ⟪y, A y⟫.

theorem LinearMap.IsPositive.sum_re_inner_le_re_trace {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {A : E →ₗ[𝕜] E} (hA : A.IsPositive) {ι : Type u_3} [Fintype ι] {v : ι → E} (hv : Orthonormal 𝕜 v) : ∑ i : ι, RCLike.re (inner 𝕜 (v i) (A (v i))) ≤ RCLike.re ((trace 𝕜 E) A)

For a positive endomorphism A of a finite-dimensional space, the diagonal entries of A along an orthonormal family have real parts summing to at most the real part of the trace.

theorem ContinuousLinearMap.IsPositive.isUnit_one_add {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {T : E →L[𝕜] E} (hT : T.IsPositive) : IsUnit (1 + T)

On a complete space, 1 + T is invertible for every positive operator T, since re ⟪(1 + T) x, x⟫ = ‖x‖² + re ⟪T x, x⟫ ≥ ‖x‖². For instance 1 + X†X is invertible, by ContinuousLinearMap.isPositive_adjoint_comp_self.

theorem ContinuousLinearMap.self_comp_adjoint_le_one {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (D : F →L[𝕜] E) (hD : ‖D‖ ≤ 1) : D ∘SL adjoint D ≤ 1

A contraction composed with its adjoint is bounded above by the identity in the Loewner order. Equivalently, its defect operator is positive.