Two-vector quadratic-form identities in real or complex inner-product spaces

Five elementary lemmas useful for block-operator perturbation estimates and planar motions:

• LinearMap.IsSymmetric.re_inner_map_symm: the real mixed coefficients agree for symmetric maps;
• LinearMap.re_inner_smul_add_smul_map: expand the real quadratic form of a two-vector real-linear combination;
• TauCeti.abs_re_inner_le_of_norm_le: ‖w‖ ≤ ε * ‖v‖ bounds |re ⟪u, w⟫| by ‖u‖ * ‖v‖ * ε, so an operator bound ‖H v‖ ≤ ε * ‖v‖ bounds the real part of every coefficient ⟪u, H v⟫;
• TauCeti.norm_smul_add_smul_sq: the Pythagorean norm formula for a two-vector real-linear combination when the real part of the mixed inner product vanishes;
• TauCeti.norm_smul_add_smul_eq_one_of_sq_add_sq: its unit-circle case, ‖γ y + σ z‖ = 1 for orthonormal y, z and γ² + σ² = 1.

No finite-dimensionality, spectral-gap, or eigenvector assumptions are needed. The results are used by the per-eigenvector double-angle estimates in DoubleAngle.Vector.

Adapted from the Apache-2.0 DKPS formalization (Kitware, Inc.).

theorem LinearMap.IsSymmetric.re_inner_map_symm {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {H : E →ₗ[𝕜] E} (hH : H.IsSymmetric) (y z : E) : RCLike.re (inner 𝕜 z (H y)) = RCLike.re (inner 𝕜 y (H z))

Real parts of the two mixed entries of a symmetric operator agree; the reason no complex phase alignment is needed anywhere in this file.

theorem LinearMap.re_inner_smul_add_smul_map {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (H : E →ₗ[𝕜] E) (y z : E) (γ σ : ℝ) : RCLike.re (inner 𝕜 (↑γ • y + ↑σ • z) (H (↑γ • y + ↑σ • z))) = γ ^ 2 * RCLike.re (inner 𝕜 y (H y)) + σ ^ 2 * RCLike.re (inner 𝕜 z (H z)) + γ * σ * (RCLike.re (inner 𝕜 y (H z)) + RCLike.re (inner 𝕜 z (H y)))

Quadratic form of an operator at a real linear combination of two vectors, expanded into the four scalar entries. Pure sesquilinear algebra.

theorem TauCeti.abs_re_inner_le_of_norm_le {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (u : E) {v w : E} {ε : ℝ} (hw : ‖w‖ ≤ ε * ‖v‖) : |RCLike.re (inner 𝕜 u w)| ≤ ‖u‖ * ‖v‖ * ε

If ‖w‖ ≤ ε * ‖v‖, then |re ⟪u, w⟫| ≤ ‖u‖ * ‖v‖ * ε. For w = H v this says that an operator bound ‖H v‖ ≤ ε * ‖v‖ bounds the real part of every coefficient ⟪u, H v⟫.

theorem TauCeti.norm_smul_add_smul_sq {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {y z : E} (hyz : RCLike.re (inner 𝕜 y z) = 0) (γ σ : ℝ) : ‖↑γ • y + ↑σ • z‖ ^ 2 = γ ^ 2 * ‖y‖ ^ 2 + σ ^ 2 * ‖z‖ ^ 2

Squared norm of a real linear combination of two vectors orthogonal with respect to the real part of the inner product.

theorem TauCeti.norm_smul_add_smul_eq_one_of_sq_add_sq {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {y z : E} (hy : ‖y‖ = 1) (hz : ‖z‖ = 1) (hyz : RCLike.re (inner 𝕜 y z) = 0) {γ σ : ℝ} (hγσ : γ ^ 2 + σ ^ 2 = 1) : ‖↑γ • y + ↑σ • z‖ = 1

For unit vectors y, z orthogonal with respect to the real part of the inner product, the real linear combination γ y + σ z with γ² + σ² = 1 is a unit vector; this is norm_smul_add_smul_sq read on the unit circle.