Accepted with source warningTheorem · Statement with omitted proof

Expected spectral error of randomized Nyström approximation

The source relates Nyström approximation error to the eigenvalue tail of a positive semidefinite matrix.

Martinsson & Tropp ↗
Source label: Theorem rand-nys

Download Lean file ↓

Formal statement. The assumptions and conclusion are explicit; the theorem proof is omitted (sorry).

01 / MATHEMATICAL STATEMENT

Meaning & conditions

Mathematical summary

The source relates Nyström approximation error to the eigenvalue tail of a positive semidefinite matrix.

\mathbb E\|A-\widehat A_k\|\le\lambda_{k+1}+\frac{k}{\ell-k-1}\sum_{j>k}\lambda_j

Assumptions & context

A is real or complex positive semidefinite, 1 ≤ k < ℓ ≤ n, and Ω is standard normal. The output is a best rank-k Frobenius truncation of the Nyström matrix.

Source

Martinsson & Tropp. Randomized numerical linear algebra: Foundations and algorithms.

Source label: Theorem rand-nys

02 / LEAN REPRESENTATION

Formal statement

Statement with omitted proof. Expand the complete file below to read imports, local definitions and surrounding context.

theorem expected_spectral_error_random_nystrom
    {𝕜 : Type} {Ω : Type*} [RCLike 𝕜] [MeasurableSpace Ω]
    (hF : 𝕜 = ℝ ∨ 𝕜 = ℂ)
    (n : ℕ) (A : Matrix (Fin n) (Fin n) 𝕜) (hPSD : IsPSD A)
    (k ℓ : ℕ) (hk : 1 ≤ k) (hkℓ : k < ℓ) (hℓn : ℓ ≤ n)
    (P : Measure Ω) (Omega : Ω → Matrix (Fin n) (Fin ℓ) 𝕜)
    (hOmega : StandardNormalTestMatrix P Omega)
    (AhatK : Ω → Matrix (Fin n) (Fin n) 𝕜)
    (hAhatK : ∀ ω,
      let Y : Matrix (Fin n) (Fin ℓ) 𝕜 := A * Omega ω
      ∃ G : Matrix (Fin ℓ) (Fin ℓ) 𝕜,
        IsMoorePenroseInverse ((Omega ω)ᴴ * Y) G ∧
          BestRankKApproximation k (Y * G * Yᴴ) (AhatK ω)) :
    (∫ ω, ‖A - AhatK ω‖ ∂P) ≤
      orderedEigenvalue A ⟨k, lt_of_lt_of_le hkℓ hℓn⟩ +
        ((k : ℝ) / ((ℓ : ℝ) - (k : ℝ) - 1)) *
          (∑ j : Fin n,
            if k ≤ j.val then orderedEigenvalue A j else 0) := by
  sorry

Complete Lean file and local definitions

import RNLAPhaseB.B3Base

open MeasureTheory
open scoped Matrix
open scoped Matrix.Norms.L2Operator
open scoped BigOperators
open scoped ENNReal

namespace RNLAPhaseB.RandomNystrom

/-- Positive semidefiniteness for a real or complex square matrix. -/
def IsPSD {𝕜 : Type*} [RCLike 𝕜] {n : ℕ}
    (A : Matrix (Fin n) (Fin n) 𝕜) : Prop :=
  Aᴴ = A ∧
    ∀ v : Fin n → 𝕜,
      0 ≤ RCLike.re
        (∑ i : Fin n, star (v i) * (∑ j : Fin n, A i j * v j))

/-- The Frobenius distance, used to specify the rank truncation. -/
noncomputable def frobeniusDistance {𝕜 : Type*} [RCLike 𝕜] {n : ℕ}
    (X Y : Matrix (Fin n) (Fin n) 𝕜) : ℝ :=
  Real.sqrt (∑ i : Fin n, ∑ j : Fin n, ‖X i j - Y i j‖ ^ (2 : ℕ))

/-- A best approximation of rank at most `k` in Frobenius norm. -/
def BestRankKApproximation {𝕜 : Type*} [RCLike 𝕜] {n : ℕ}
    (k : ℕ) (X Z : Matrix (Fin n) (Fin n) 𝕜) : Prop :=
  Matrix.rank Z ≤ k ∧
    ∀ C : Matrix (Fin n) (Fin n) 𝕜,
      Matrix.rank C ≤ k →
        frobeniusDistance X Z ≤ frobeniusDistance X C

/-- The Moore–Penrose conditions specifying the pseudoinverse in the Nyström formula. -/
def IsMoorePenroseInverse {𝕜 : Type*} [RCLike 𝕜] {ℓ : ℕ}
    (M G : Matrix (Fin ℓ) (Fin ℓ) 𝕜) : Prop :=
  M * G * M = M ∧ G * M * G = G ∧
    (M * G)ᴴ = M * G ∧ (G * M)ᴴ = G * M

/-- Standard normal entries: real standard Gaussians over `ℝ`, and independent
real and imaginary Gaussians of variance `1/2` over `ℂ`. -/
noncomputable def StandardNormalTestMatrix {Ω : Type*} {𝕜 : Type} [MeasurableSpace Ω]
    [RCLike 𝕜] {n ℓ : ℕ} (P : Measure Ω)
    (Omega : Ω → Matrix (Fin n) (Fin ℓ) 𝕜) : Prop := by
  classical
  exact if hR : 𝕜 = ℝ then
    RNLAPhaseB.StandardGaussianTestMatrix P (fun ω => hR ▸ Omega ω)
  else
    IsProbabilityMeasure P ∧
      (∀ i : Fin n, ∀ j : Fin ℓ,
        ProbabilityTheory.HasLaw (fun ω => RCLike.re (Omega ω i j))
          (ProbabilityTheory.gaussianReal 0 (1 / 2)) P ∧
        ProbabilityTheory.HasLaw (fun ω => RCLike.im (Omega ω i j))
          (ProbabilityTheory.gaussianReal 0 (1 / 2)) P) ∧
      ProbabilityTheory.iIndepFun
        (fun p : (Fin n × Fin ℓ) × Bool =>
          if p.2 then fun ω => RCLike.re (Omega ω p.1.1 p.1.2)
          else fun ω => RCLike.im (Omega ω p.1.1 p.1.2)) P

/-- The `(j + 1)`st eigenvalue in decreasing order, expressed by the
Courant–Fischer variational characterization. -/
noncomputable def orderedEigenvalue {𝕜 : Type} [RCLike 𝕜] {n : ℕ}
    (A : Matrix (Fin n) (Fin n) 𝕜) (j : Fin n) : ℝ :=
  sSup {r : ℝ | ∃ V : Submodule 𝕜 (Fin n → 𝕜),
    Module.finrank 𝕜 V = j.val + 1 ∧
      ∀ v : Fin n → 𝕜, v ∈ V →
        r * (∑ i : Fin n, ‖v i‖ ^ (2 : ℕ)) ≤
          RCLike.re
            (∑ i : Fin n, star (v i) * (∑ h : Fin n, A i h * v h))}

/-- SOURCE WARNING sw1: The source permits `ℓ = k + 1`, making its denominator
`ℓ − k − 1` zero. Lean's real division assigns the resulting `k / 0` the
value zero; no restriction on `ℓ` has been added.
SOURCE WARNING sw2: The stated range `1 ≤ k < ℓ ≤ n` likewise includes
`ℓ = k + 1`, where the displayed fraction is undefined in ordinary arithmetic. -/
theorem expected_spectral_error_random_nystrom
    {𝕜 : Type} {Ω : Type*} [RCLike 𝕜] [MeasurableSpace Ω]
    (hF : 𝕜 = ℝ ∨ 𝕜 = ℂ)
    (n : ℕ) (A : Matrix (Fin n) (Fin n) 𝕜) (hPSD : IsPSD A)
    (k ℓ : ℕ) (hk : 1 ≤ k) (hkℓ : k < ℓ) (hℓn : ℓ ≤ n)
    (P : Measure Ω) (Omega : Ω → Matrix (Fin n) (Fin ℓ) 𝕜)
    (hOmega : StandardNormalTestMatrix P Omega)
    (AhatK : Ω → Matrix (Fin n) (Fin n) 𝕜)
    (hAhatK : ∀ ω,
      let Y : Matrix (Fin n) (Fin ℓ) 𝕜 := A * Omega ω
      ∃ G : Matrix (Fin ℓ) (Fin ℓ) 𝕜,
        IsMoorePenroseInverse ((Omega ω)ᴴ * Y) G ∧
          BestRankKApproximation k (Y * G * Yᴴ) (AhatK ω)) :
    (∫ ω, ‖A - AhatK ω‖ ∂P) ≤
      orderedEigenvalue A ⟨k, lt_of_lt_of_le hkℓ hℓn⟩ +
        ((k : ℝ) / ((ℓ : ℝ) - (k : ℝ) - 1)) *
          (∑ j : Fin n,
            if k ≤ j.val then orderedEigenvalue A j else 0) := by
  sorry

end RNLAPhaseB.RandomNystrom

← Back to all statements