The defect form of a bounded operator

For a bounded operator X : F →L[𝕜] E between seminormed inner product spaces, the real form (v, w) ↦ ‖X‖² re ⟪v, w⟫ - re ⟪X v, X w⟫ is positive semidefinite, since its diagonal value ‖X‖² ‖v‖² - ‖X v‖² is nonnegative by the definition of the operator norm. It therefore satisfies the Cauchy–Schwarz inequality. If a unit vector v nearly attains the norm of X, this makes re ⟪X w, X v⟫ close to ‖X‖² re ⟪w, v⟫, with an error of at most ‖X‖ ‖w‖ √(‖X‖² - ‖X v‖²).

Main statements

• ContinuousLinearMap.sq_opNorm_sq_mul_re_inner_sub_re_inner_le: the Cauchy–Schwarz inequality for the defect form of an operator.

theorem ContinuousLinearMap.sq_opNorm_sq_mul_re_inner_sub_re_inner_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] [SeminormedAddCommGroup F] [InnerProductSpace 𝕜 F] (X : F →L[𝕜] E) (v w : F) : (‖X‖ ^ 2 * RCLike.re (inner 𝕜 v w) - RCLike.re (inner 𝕜 (X v) (X w))) ^ 2 ≤ (‖X‖ ^ 2 * ‖v‖ ^ 2 - ‖X v‖ ^ 2) * (‖X‖ ^ 2 * ‖w‖ ^ 2 - ‖X w‖ ^ 2)

Cauchy–Schwarz for the defect form of an operator. For X : F →L[𝕜] E, the real form (v, w) ↦ ‖X‖² re ⟪v, w⟫ - re ⟪X v, X w⟫ is positive semidefinite, so it satisfies the Cauchy–Schwarz inequality. In particular, for a unit vector v, re ⟪X w, X v⟫ differs from ‖X‖² re ⟪w, v⟫ by at most ‖X‖ ‖w‖ √(‖X‖² - ‖X v‖²).