Documentation

TauCeti.Analysis.InnerProductSpace.DoubleAngle.Vector

Per-eigenvector Davis sin 2θ and off-diagonal tan 2θ bounds #

Let T and H be symmetric operators on a real or complex inner-product space. Suppose U is invariant under T, and T has two separated quadratic-form bounds: at least b * ‖u‖² on U and at most a * ‖z‖² on Uᗮ. For a unit eigenvector x of T + H, write x = y + z with y ∈ U and z ∈ Uᗮ.

The sharp per-eigenvector double-angle product estimate is (b-a) * ‖y‖ * ‖z‖ ≤ ε when ‖H v‖ ≤ ε * ‖v‖. With an orthogonal projection onto U, θ = arccos ‖P_U x‖ gives the angle form (b-a) * sin (2θ) ≤ 2ε. If b > a, these imply the usual divided bound sin (2θ) ≤ 2ε / (b-a); positivity of the gap is required for division.

If the two diagonal blocks of H with respect to U ⊕ Uᗮ vanish, the sharper, homogeneous off-diagonal product estimate is (b-a) * ‖y‖ * ‖z‖ ≤ |‖y‖² - ‖z‖²| * ε. For a unit vector, b > a, and cos (2θ) ≠ 0, this implies the absolute tangent bound |tan (2θ)| ≤ 2ε / (b-a). The product estimate itself requires neither unit normalization nor a tangent pole restriction.

These are eigenvector bounds, not the finite-dimensional unitarily invariant subspace sin 2Θ theorem or the general sin Θ theorems. They do not require finite-dimensionality. The proof uses a phase-free block-energy identity and real two-vector quadratic-form identities.

Main declarations #

References and provenance #

source
theorem LinearMap.IsSymmetric.sin_two_theta_le_of_mem {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T H : E →ₗ[𝕜] E} (hT : T.IsSymmetric) (hH : H.IsSymmetric) {U : Submodule 𝕜 E} (hUinv : ∀ u ∈ U, T u ∈ U) {a b ε : ℝ} (hb : ∀ u ∈ U, b * ‖u‖ ^ 2 ≤ RCLike.re (inner 𝕜 (T u) u)) (ha : ∀ w ∈ Uᗮ, RCLike.re (inner 𝕜 (T w) w) ≤ a * ‖w‖ ^ 2) (hε : ∀ (v : E), ‖H v‖ ≤ ε * ‖v‖) {y z : E} (hyU : y ∈ U) (hzU : z ∈ Uᗮ) (hx : ‖y + z‖ = 1) {μ : ℝ} (hμ : T (y + z) + H (y + z) = ↑μ • (y + z)) :
(b - a) * (‖y‖ * ‖z‖) ≤ ε

Davis's sin 2θ theorem, orthogonal-decomposition form. Let T, H be symmetric, U a T-invariant subspace with the quadratic form of T at least b * ‖·‖ ^ 2 on U and at most a * ‖·‖ ^ 2 on Uᗮ, and let y + z (y ∈ U, z ∈ Uᗮ) be a unit eigenvector of T + H with real eigenvalue μ — no location assumption on μ. If ‖H v‖ ≤ ε * ‖v‖ for all v, then

(b - a) * (‖y‖ * ‖z‖) ≤ ε.

For the angle θ of the unit eigenvector with U, 2 * ‖y‖ * ‖z‖ = sin (2θ). Only when b > a can the product inequality be divided by the spectral gap to obtain sin (2θ) ≤ 2ε / (b-a). The product statement also holds for b ≤ a and does not require an orthogonal projection onto U.

source
theorem LinearMap.IsSymmetric.sin_two_theta_le {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T H : E →ₗ[𝕜] E} (hT : T.IsSymmetric) (hH : H.IsSymmetric) {U : Submodule 𝕜 E} [U.HasOrthogonalProjection] (hUinv : ∀ u ∈ U, T u ∈ U) {a b ε : ℝ} (hb : ∀ u ∈ U, b * ‖u‖ ^ 2 ≤ RCLike.re (inner 𝕜 (T u) u)) (ha : ∀ w ∈ Uᗮ, RCLike.re (inner 𝕜 (T w) w) ≤ a * ‖w‖ ^ 2) (hε : ∀ (v : E), ‖H v‖ ≤ ε * ‖v‖) {x : E} (hx : ‖x‖ = 1) {μ : ℝ} (hμ : T x + H x = ↑μ • x) :
(b - a) * (‖U.starProjection x‖ * ‖x - U.starProjection x‖) ≤ ε

Davis's sin 2θ theorem, per-eigenvector product form. Under the hypotheses of sin_two_theta_le_of_mem, for a unit eigenvector x of T + H and P = U.starProjection,

(b - a) * (‖P x‖ * ‖x - P x‖) ≤ ε,

When b > a, this implies the divided sin (2θ) ≤ 2ε / (b-a) bound for the angle θ between x and U.

source
theorem LinearMap.IsSymmetric.sin_two_arccos_le {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T H : E →ₗ[𝕜] E} (hT : T.IsSymmetric) (hH : H.IsSymmetric) {U : Submodule 𝕜 E} [U.HasOrthogonalProjection] (hUinv : ∀ u ∈ U, T u ∈ U) {a b ε : ℝ} (hb : ∀ u ∈ U, b * ‖u‖ ^ 2 ≤ RCLike.re (inner 𝕜 (T u) u)) (ha : ∀ w ∈ Uᗮ, RCLike.re (inner 𝕜 (T w) w) ≤ a * ‖w‖ ^ 2) (hε : ∀ (v : E), ‖H v‖ ≤ ε * ‖v‖) {x : E} (hx : ‖x‖ = 1) {μ : ℝ} (hμ : T x + H x = ↑μ • x) :
(b - a) * Real.sin (2 * Real.arccos ‖U.starProjection x‖) ≤ 2 * ε

Davis's sin 2θ theorem, angle form. Under the hypotheses of sin_two_theta_le, with θ = arccos ‖P x‖ the angle between the unit eigenvector x and the invariant subspace U,

(b - a) * sin (2θ) ≤ 2 * ε, with no division by b-a.

source
theorem LinearMap.IsSymmetric.tan_two_theta_le_of_mem {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T H : E →ₗ[𝕜] E} (hT : T.IsSymmetric) (hH : H.IsSymmetric) {U : Submodule 𝕜 E} (hUinv : ∀ u ∈ U, T u ∈ U) {a b ε : ℝ} (hb : ∀ u ∈ U, b * ‖u‖ ^ 2 ≤ RCLike.re (inner 𝕜 (T u) u)) (ha : ∀ w ∈ Uᗮ, RCLike.re (inner 𝕜 (T w) w) ≤ a * ‖w‖ ^ 2) (hε : ∀ (v : E), ‖H v‖ ≤ ε * ‖v‖) (hHU : ∀ u ∈ U, ∀ u' ∈ U, inner 𝕜 u (H u') = 0) (hHUperp : ∀ w ∈ Uᗮ, ∀ w' ∈ Uᗮ, inner 𝕜 w (H w') = 0) {y z : E} (hyU : y ∈ U) (hzU : z ∈ Uᗮ) {μ : ℝ} (hμ : T (y + z) + H (y + z) = ↑μ • (y + z)) :
(b - a) * (‖y‖ * ‖z‖) ≤ |‖y‖ ^ 2 - ‖z‖ ^ 2| * ε

Off-diagonal double-angle product bound. Suppose the diagonal blocks of H relative to U ⊕ Uᗮ vanish. For any (possibly nonunit) eigenvector y+z of T+H, with y ∈ U and z ∈ Uᗮ,

(b-a) * ‖y‖ * ‖z‖ ≤ |‖y‖² - ‖z‖²| * ε.

The result is homogeneous and has no positivity-of-gap or transversality side conditions. For unit eigenvectors, with b>a and cos (2θ) ≠ 0, it yields |tan (2θ)| ≤ 2ε/(b-a); the absolute value and the pole exclusion are essential. The proof uses the same block-energy identity as the sine estimate.

source
theorem LinearMap.IsSymmetric.tan_two_theta_le {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T H : E →ₗ[𝕜] E} (hT : T.IsSymmetric) (hH : H.IsSymmetric) {U : Submodule 𝕜 E} [U.HasOrthogonalProjection] (hUinv : ∀ u ∈ U, T u ∈ U) {a b ε : ℝ} (hb : ∀ u ∈ U, b * ‖u‖ ^ 2 ≤ RCLike.re (inner 𝕜 (T u) u)) (ha : ∀ w ∈ Uᗮ, RCLike.re (inner 𝕜 (T w) w) ≤ a * ‖w‖ ^ 2) (hε : ∀ (v : E), ‖H v‖ ≤ ε * ‖v‖) (hHU : ∀ u ∈ U, ∀ u' ∈ U, inner 𝕜 u (H u') = 0) (hHUperp : ∀ w ∈ Uᗮ, ∀ w' ∈ Uᗮ, inner 𝕜 w (H w') = 0) {x : E} {μ : ℝ} (hμ : T x + H x = ↑μ • x) :
(b - a) * (‖U.starProjection x‖ * ‖x - U.starProjection x‖) ≤ |‖U.starProjection x‖ ^ 2 - ‖x - U.starProjection x‖ ^ 2| * ε

Off-diagonal double-angle product bound, projection form. Under the hypotheses of tan_two_theta_le_of_mem, for any eigenvector x of T+H and P=U.starProjection,

(b-a) * ‖P x‖ * ‖x-P x‖ ≤ |‖P x‖² - ‖x-P x‖²| * ε.

The statement is homogeneous: ‖x‖=1 is not required. For unit x, b>a, and away from cos (2θ)=0, this gives the absolute tan (2θ) bound.