Diagonal, polarization, and absorption identities for continuous linear operators

This module collects operator identities independent of projection-valued measures.

• ContinuousLinearMap.inner_polarization recovers ⟪ψ, T ξ⟫ from four diagonal values.
• ContinuousLinearMap.eq_of_diagonal uses complex polarization to identify operators from their diagonal inner products.
• ContinuousLinearMap.norm_sub_sq_of_selfAdjoint_idempotent_absorption computes the squared distance between S x and T x when S is a self-adjoint idempotent absorbed by T.
• ContinuousLinearMap.adjoint_ofReal_smul: the adjoint commutes with real scalars.
• ContinuousLinearMap.norm_apply_sq_of_adjoint_comp_eq_smul: if T† T = c for a real scalar c, then ‖T x‖² = c ‖x‖².
• ContinuousLinearMap.adjoint_ofReal_smul_comp_ofReal_smul and ContinuousLinearMap.ofReal_smul_comp_adjoint_ofReal_smul: if T† T (respectively T T†) is a real scalar s, then the same product for c T is c² s.

Use eq_of_diagonal to identify bounded complex-linear operators when their diagonal inner products agree on every vector. Use norm_sub_sq_of_selfAdjoint_idempotent_absorption to compare two operators when the first is a self-adjoint projection absorbed by the second. The latter identity applies over real or complex scalars and does not require the second operator to be self-adjoint.

theorem ContinuousLinearMap.eq_of_diagonal {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (S T : H →L[ℂ] H) (h : ∀ (x : H), inner ℂ x (S x) = inner ℂ x (T x)) : S = T

Complex polarization: equality of all diagonal inner products determines a continuous linear operator. This specializes Mathlib's ext_inner_map to continuous linear maps.

theorem ContinuousLinearMap.inner_polarization {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (T : H →L[ℂ] H) (ψ ξ : H) : 1 / 4 * (inner ℂ (ξ + ψ) (T (ξ + ψ)) + Complex.I * inner ℂ (ξ + Complex.I • ψ) (T (ξ + Complex.I • ψ)) - inner ℂ (ξ - ψ) (T (ξ - ψ)) - Complex.I * inner ℂ (ξ - Complex.I • ψ) (T (ξ - Complex.I • ψ))) = inner ℂ ψ (T ξ)

The complex polarization identity for the sesquilinear form of a bounded operator, recovered from its diagonal quadratic form.

theorem ContinuousLinearMap.norm_sub_sq_of_selfAdjoint_idempotent_absorption {𝕜 : Type u_2} {E : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (S T : E →L[𝕜] E) (hS : IsSelfAdjoint S) (hSS : S * S = S) (hST : S * T = S) (x : E) : ‖S x - T x‖ ^ 2 = ‖T x‖ ^ 2 - ‖S x‖ ^ 2

Over either the real or complex scalars, if S is self-adjoint, idempotent, and satisfies S * T = S, then the squared norm of (S - T) x is the difference of the squared norms. The operator T need not be self-adjoint.

theorem ContinuousLinearMap.adjoint_ofReal_smul {𝕜 : Type u_2} {E : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {F : Type u_4} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (r : ℝ) (T : E →L[𝕜] F) : adjoint (↑r • T) = ↑r • adjoint T

The adjoint commutes with multiplication by a real scalar.

theorem ContinuousLinearMap.norm_apply_sq_of_adjoint_comp_eq_smul {𝕜 : Type u_2} {E : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {F : Type u_4} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {T : E →L[𝕜] F} {c : ℝ} (hT : adjoint T ∘SL T = ↑c • 1) (x : E) : ‖T x‖ ^ 2 = c * ‖x‖ ^ 2

An operator T with T† T = c for a real scalar c multiplies norms squared by c.

theorem ContinuousLinearMap.adjoint_ofReal_smul_comp_ofReal_smul {𝕜 : Type u_2} {E : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {F : Type u_4} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {T : E →L[𝕜] F} {s : ℝ} (hT : adjoint T ∘SL T = ↑s • 1) (c : ℝ) : adjoint (↑c • T) ∘SL (↑c • T) = ↑(c ^ 2 * s) • 1

If T† T = s for a real scalar s, then (c T)† (c T) = c² s for real c.

theorem ContinuousLinearMap.ofReal_smul_comp_adjoint_ofReal_smul {𝕜 : Type u_2} {E : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {F : Type u_4} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {T : E →L[𝕜] F} {s : ℝ} (hT : T ∘SL adjoint T = ↑s • 1) (c : ℝ) : (↑c • T) ∘SL adjoint (↑c • T) = ↑(c ^ 2 * s) • 1

If T T† = s for a real scalar s, then (c T) (c T)† = c² s for real c.