Local definitions (inlined to avoid cross-file import chains)

def Thm48.IsSpikedCovariance {d : ℕ} (S : Matrix (Fin d) (Fin d) ℝ) (θ : ℝ) (v : EuclideanSpace ℝ (Fin d)) : Prop

Definition 4.7 (Spiked covariance model). A matrix S satisfies the spiked covariance model with parameter θ > 0 and spike v (a unit vector) if S = θ • (v · vᵀ) + I_d.

noncomputable def Thm48.principalAngle {d : ℕ} (u v : EuclideanSpace ℝ (Fin d)) : ℝ

The principal angle between two vectors u and v is arccos |⟨u, v⟩|.

noncomputable def Thm48.matrixOpNorm {d : ℕ} (A : Matrix (Fin d) (Fin d) ℝ) : ℝ

The operator norm of a matrix: ‖A‖_op = sup_{‖x‖=1} ‖Ax‖, defined via the continuous linear map norm on Euclidean spaces.

def Thm48.IsLargestEigenvector {d : ℕ} (M : Matrix (Fin d) (Fin d) ℝ) (w : EuclideanSpace ℝ (Fin d)) : Prop

IsLargestEigenvector M w means w is a unit eigenvector of M corresponding to the largest eigenvalue: it has unit norm and maximizes the Rayleigh quotient wᵀ M w over all unit vectors.

theorem Thm48.IsLargestEigenvector.norm_eq_one {d : ℕ} {M : Matrix (Fin d) (Fin d) ℝ} {w : EuclideanSpace ℝ (Fin d)} (h : IsLargestEigenvector M w) : ‖w‖ = 1

A largest eigenvector has unit norm.

Theorem 4.8 (Davis-Kahan sin(θ) theorem)

The theorem states that for the spiked covariance model Σ = θ v vᵀ + I_d and any PSD estimator Σ̃ with largest eigenvector ṽ:

min_{ε ∈ {±1}} ‖ε·ṽ − v‖₂² ≤ 2 sin²(∠(ṽ, v)) ≤ (8/θ²) ‖Σ̃ − Σ‖_op²

theorem Thm48.theorem_4_8_left {d : ℕ} (vtilde v : EuclideanSpace ℝ (Fin d)) (hvt : ‖vtilde‖ = 1) (hv : ‖v‖ = 1) : min (‖vtilde - v‖ ^ 2) (‖vtilde + v‖ ^ 2) ≤ 2 * Real.sin (principalAngle vtilde v) ^ 2

Theorem 4.8, left inequality. For any two unit vectors, the minimum sign-adjusted squared distance is at most 2 sin² of the principal angle: min(‖ṽ − v‖², ‖ṽ + v‖²) ≤ 2 sin²(∠(ṽ, v)).

Helper lemmas for operator norm and Rayleigh quotients

theorem Thm48.smul_mulVec_distrib {d : ℕ} (θ : ℝ) (M : Matrix (Fin d) (Fin d) ℝ) (u : Fin d → ℝ) : (θ • M).mulVec u = θ • M.mulVec u

Scalar-matrix product applied to mulVec distributes.

theorem Thm48.vecMulVec_self_mulVec {d : ℕ} (v x : Fin d → ℝ) : (Matrix.vecMulVec v v).mulVec x = (v ⬝ᵥ x) • v

vecMulVec v v applied to x gives (v ⬝ᵥ x) • v.

theorem Thm48.dotProduct_vecMulVec_self {d : ℕ} (v x : Fin d → ℝ) : x ⬝ᵥ (Matrix.vecMulVec v v).mulVec x = (v ⬝ᵥ x) ^ 2

Quadratic form of vecMulVec v v equals the square of the dot product.

theorem Thm48.rayleigh_spiked_model {d : ℕ} (θ : ℝ) (v u : Fin d → ℝ) : u ⬝ᵥ (θ • Matrix.vecMulVec v v + 1).mulVec u = θ * (v ⬝ᵥ u) ^ 2 + u ⬝ᵥ u

Rayleigh quotient of the spiked covariance θ • vvᵀ + I is θ(v·u)² + ‖u‖².

theorem Thm48.dotProduct_self_unit {d : ℕ} (u : EuclideanSpace ℝ (Fin d)) (hu : ‖u‖ = 1) : (EuclideanSpace.equiv (Fin d) ℝ) u ⬝ᵥ (EuclideanSpace.equiv (Fin d) ℝ) u = 1

For unit vectors in EuclideanSpace ℝ, the self dot product equals 1.

theorem Thm48.inner_eq_dotProduct {d : ℕ} (u v : EuclideanSpace ℝ (Fin d)) : inner ℝ u v = (EuclideanSpace.equiv (Fin d) ℝ) u ⬝ᵥ (EuclideanSpace.equiv (Fin d) ℝ) v

Inner product on EuclideanSpace ℝ equals dot product of coordinates.

theorem Thm48.toEuclideanLin_ofLp {d : ℕ} (A : Matrix (Fin d) (Fin d) ℝ) (x : EuclideanSpace ℝ (Fin d)) : ((Matrix.toEuclideanLin A) x).ofLp = A.mulVec x.ofLp

Connection: toEuclideanLin A x applied to ofLp gives A.mulVec (x.ofLp).

theorem Thm48.inner_toEuclideanLin {d : ℕ} (A : Matrix (Fin d) (Fin d) ℝ) (x : EuclideanSpace ℝ (Fin d)) : inner ℝ ((Matrix.toEuclideanLin A) x) x = x.ofLp ⬝ᵥ A.mulVec x.ofLp

Inner product ⟨toEuclideanLin A x, x⟩ equals the quadratic form x·(Ax).

theorem Thm48.abs_quadForm_le_opNorm {d : ℕ} (A : Matrix (Fin d) (Fin d) ℝ) (x : EuclideanSpace ℝ (Fin d)) (hx : ‖x‖ = 1) : |x.ofLp ⬝ᵥ A.mulVec x.ofLp| ≤ matrixOpNorm A

The absolute value of a quadratic form is bounded by the operator norm for unit vectors.

theorem Thm48.symmetric_dotProduct_mulVec {d : ℕ} (M : Matrix (Fin d) (Fin d) ℝ) (hM : M.transpose = M) (u w : Fin d → ℝ) : u ⬝ᵥ M.mulVec w = w ⬝ᵥ M.mulVec u

For symmetric M (Mᵀ = M), the bilinear form is symmetric: u ⬝ᵥ (M v) = v ⬝ᵥ (M u).

theorem Thm48.bilinear_identity {d : ℕ} (M : Matrix (Fin d) (Fin d) ℝ) (hM : M.transpose = M) (u w : Fin d → ℝ) : u ⬝ᵥ M.mulVec u - w ⬝ᵥ M.mulVec w = (u - w) ⬝ᵥ M.mulVec (u + w)

Bilinear identity for symmetric M: u·(Mu) - w·(Mw) = (u-w)·(M(u+w)).

theorem Thm48.inner_toEuclideanLin' {d : ℕ} (A : Matrix (Fin d) (Fin d) ℝ) (u w : EuclideanSpace ℝ (Fin d)) : inner ℝ u ((Matrix.toEuclideanLin A) w) = u.ofLp ⬝ᵥ A.mulVec w.ofLp

Inner product ⟨u, toEuclideanLin A w⟩ equals the bilinear form u·(Aw).

theorem Thm48.abs_bilinear_le_opNorm {d : ℕ} (A : Matrix (Fin d) (Fin d) ℝ) (u w : EuclideanSpace ℝ (Fin d)) : |u.ofLp ⬝ᵥ A.mulVec w.ofLp| ≤ ‖u‖ * matrixOpNorm A * ‖w‖

The Cauchy-Schwarz bound for bilinear forms with operator norm: |u ⬝ᵥ (A v)| ≤ ‖u‖ * ‖A‖_op * ‖v‖.

theorem Thm48.spiked_transpose_eq {d : ℕ} (θ : ℝ) (v : EuclideanSpace ℝ (Fin d)) : (θ • Matrix.vecMulVec v.ofLp v.ofLp + 1).transpose = θ • Matrix.vecMulVec v.ofLp v.ofLp + 1

The spiked covariance matrix is symmetric.

theorem Thm48.davis_kahan_sin_bound {d : ℕ} (Sig : Matrix (Fin d) (Fin d) ℝ) (θ : ℝ) (v : EuclideanSpace ℝ (Fin d)) (hSpike : IsSpikedCovariance Sig θ v) (SigTilde : Matrix (Fin d) (Fin d) ℝ) (hPSD : SigTilde.PosSemidef) (vtilde : EuclideanSpace ℝ (Fin d)) (hvt : ‖vtilde‖ = 1) (hEig : IsLargestEigenvector SigTilde vtilde) : Real.sin (principalAngle vtilde v) ≤ 2 / θ * matrixOpNorm (SigTilde - Sig)

Key Davis-Kahan inequality: sin(angle) le (2/theta) opnorm(SigTilde - Sig).

theorem Thm48.theorem_4_8_right {d : ℕ} (Sig : Matrix (Fin d) (Fin d) ℝ) (θ : ℝ) (v : EuclideanSpace ℝ (Fin d)) (hSpike : IsSpikedCovariance Sig θ v) (SigTilde : Matrix (Fin d) (Fin d) ℝ) (hPSD : SigTilde.PosSemidef) (vtilde : EuclideanSpace ℝ (Fin d)) (hvt : ‖vtilde‖ = 1) (hEig : IsLargestEigenvector SigTilde vtilde) : 2 * Real.sin (principalAngle vtilde v) ^ 2 ≤ 8 / θ ^ 2 * matrixOpNorm (SigTilde - Sig) ^ 2

theorem Thm48.theorem_4_8 {d : ℕ} (Sig : Matrix (Fin d) (Fin d) ℝ) (θ : ℝ) (v : EuclideanSpace ℝ (Fin d)) (hSpike : IsSpikedCovariance Sig θ v) (SigTilde : Matrix (Fin d) (Fin d) ℝ) (hPSD : SigTilde.PosSemidef) (vtilde : EuclideanSpace ℝ (Fin d)) (hvt : ‖vtilde‖ = 1) (hEig : IsLargestEigenvector SigTilde vtilde) : min (‖vtilde - v‖ ^ 2) (‖vtilde + v‖ ^ 2) ≤ 8 / θ ^ 2 * matrixOpNorm (SigTilde - Sig) ^ 2

Theorem 4.8 (Davis-Kahan sin(θ) theorem), full chain. Combines both inequalities into the end-to-end bound: min_{ε ∈ {±1}} ‖ε·ṽ − v‖₂² ≤ (8/θ²) ‖Σ̃ − Σ‖_op².