def 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 principalAngle {d : ℕ} (u v : EuclideanSpace ℝ (Fin d)) : ℝ

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

theorem IsSpikedCovariance.posSemidef {d : ℕ} {S : Matrix (Fin d) (Fin d) ℝ} {θ : ℝ} {v : EuclideanSpace ℝ (Fin d)} (h : IsSpikedCovariance S θ v) : S.PosSemidef

The spiked covariance matrix is positive semidefinite.

theorem IsSpikedCovariance.isHermitian {d : ℕ} {S : Matrix (Fin d) (Fin d) ℝ} {θ : ℝ} {v : EuclideanSpace ℝ (Fin d)} (h : IsSpikedCovariance S θ v) : S.IsHermitian

theorem dotProduct_self_eq_one_of_norm_eq_one {d : ℕ} {v : EuclideanSpace ℝ (Fin d)} (hv : ‖v‖ = 1) : v.ofLp ⬝ᵥ v.ofLp = 1

theorem IsSpikedCovariance.mulVec_spike {d : ℕ} {S : Matrix (Fin d) (Fin d) ℝ} {θ : ℝ} {v : EuclideanSpace ℝ (Fin d)} (h : IsSpikedCovariance S θ v) : S.mulVec v.ofLp = (1 + θ) • v.ofLp

The spike v is an eigenvector of S with eigenvalue 1 + θ.

theorem principalAngle_nonneg {d : ℕ} (u v : EuclideanSpace ℝ (Fin d)) : 0 ≤ principalAngle u v

theorem principalAngle_le_pi {d : ℕ} (u v : EuclideanSpace ℝ (Fin d)) : principalAngle u v ≤ Real.pi

theorem principalAngle_le_pi_div_two {d : ℕ} (u v : EuclideanSpace ℝ (Fin d)) : principalAngle u v ≤ Real.pi / 2

theorem principalAngle_comm {d : ℕ} (u v : EuclideanSpace ℝ (Fin d)) : principalAngle u v = principalAngle v u