AcceptedTheorem · Statement with omitted proof

Exponential bounds for Gaussian trace estimation

Intrinsic dimension controls upper and lower deviations of a Gaussian trace estimator.

Martinsson & Tropp ↗
Source label: Theorem trace-est-exp

Download Lean file ↓

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

01 / MATHEMATICAL STATEMENT

Meaning & conditions

Mathematical summary

Intrinsic dimension controls upper and lower deviations of a Gaussian trace estimator.

\begin{aligned}\Pr\{\overline X_k\ge\tau\operatorname{tr}(A)\}&\le e^{-\frac12 k\,\operatorname{intdim}(A)(\sqrt\tau-1)^2},\\ \Pr\{\overline X_k\le\tau^{-1}\operatorname{tr}(A)\}&\le e^{-\frac14 k\,\operatorname{intdim}(A)(\tau^{-1}-1)^2}.\end{aligned}

Assumptions & context

A is nonzero positive semidefinite, τ > 1, k ≤ n, and the probes are independent standard normal. The intrinsic dimension is tr(A)/‖A‖.

Source

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

Source label: Theorem trace-est-exp

02 / LEAN REPRESENTATION

Formal statement

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

theorem trace_estimator_exp (n : ℕ) :
    (∀ (A : Matrix (Fin n) (Fin n) ℝ), PsdSymMatrix A → A ≠ 0 →
      ∀ (τ : ℝ), 1 < τ → ∀ (k : ℕ), k ≤ n →
      ∀ (Ω : Type*) [MeasurableSpace Ω] (P : Measure Ω)
        (W : Ω → Matrix (Fin k) (Fin n) ℝ),
        StandardGaussianTestMatrix P W →
          (P {ω | averageTraceSample A (W ω) ≥
                τ * Matrix.trace A} ≤
              ENNReal.ofReal (Real.exp
                (-(1 / 2 : ℝ) * (k : ℝ) * intrinsicDimension A *
                  (Real.sqrt τ - 1) ^ 2)) ∧
           P {ω | averageTraceSample A (W ω) ≤
                τ⁻¹ * Matrix.trace A} ≤
              ENNReal.ofReal (Real.exp
                (-(1 / 4 : ℝ) * (k : ℝ) * intrinsicDimension A *
                  (τ⁻¹ - 1) ^ 2)))) ∧
    (∀ (A : Matrix (Fin n) (Fin n) ℂ), PsdSymMatrix A → A ≠ 0 →
      ∀ (τ : ℝ), 1 < τ → ∀ (k : ℕ), k ≤ n →
      ∀ (Ω : Type*) [MeasurableSpace Ω] (P : Measure Ω)
        (G : Ω → Matrix (Fin k) (Fin n × Fin 2) ℝ),
        StandardGaussianTestMatrix P G →
          (P {ω | averageTraceSample A (complexStandardNormalSamples (G ω)) ≥
                τ * RCLike.re (Matrix.trace A)} ≤
              ENNReal.ofReal (Real.exp
                (-(2 : ℝ) * ((1 / 2 : ℝ) * (k : ℝ) *
                  intrinsicDimension A * (Real.sqrt τ - 1) ^ 2))) ∧
           P {ω | averageTraceSample A (complexStandardNormalSamples (G ω)) ≤
                τ⁻¹ * RCLike.re (Matrix.trace A)} ≤
              ENNReal.ofReal (Real.exp
                (-(2 : ℝ) * ((1 / 4 : ℝ) * (k : ℝ) *
                  intrinsicDimension A * (τ⁻¹ - 1) ^ 2))))) := 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.TraceEstExp

/-- A self-adjoint positive semidefinite matrix. -/
def PsdSymMatrix {𝕜 : Type*} [RCLike 𝕜] {n : ℕ}
    (A : Matrix (Fin n) (Fin n) 𝕜) : Prop :=
  Aᴴ = A ∧
    ∀ v : Fin n → 𝕜,
      0 ≤ RCLike.re (∑ j : Fin n, star (v j) * (A *ᵥ v) j)

/-- The intrinsic dimension, with the matrix operator norm. -/
noncomputable def intrinsicDimension {𝕜 : Type*} [RCLike 𝕜] {n : ℕ}
    (A : Matrix (Fin n) (Fin n) 𝕜) : ℝ :=
  RCLike.re (Matrix.trace A) / ‖A‖

/-- The quadratic-form trace sample. It is real for a self-adjoint matrix. -/
def traceSample {𝕜 : Type*} [RCLike 𝕜] {n : ℕ}
    (A : Matrix (Fin n) (Fin n) 𝕜) (v : Fin n → 𝕜) : ℝ :=
  RCLike.re (∑ j : Fin n, star (v j) * (A *ᵥ v) j)

/-- The average of `k` trace samples, one from each row. -/
noncomputable def averageTraceSample {𝕜 : Type*} [RCLike 𝕜] {n k : ℕ}
    (A : Matrix (Fin n) (Fin n) 𝕜)
    (W : Matrix (Fin k) (Fin n) 𝕜) : ℝ :=
  (∑ i : Fin k, traceSample A (W i)) / (k : ℝ)

/-- Unit-variance complex standard normal entries, constructed from independent
standard real normal entries. -/
noncomputable def complexStandardNormalSamples {n k : ℕ}
    (G : Matrix (Fin k) (Fin n × Fin 2) ℝ) :
    Matrix (Fin k) (Fin n) ℂ :=
  fun i j =>
    ((G i (j, (0 : Fin 2)) : ℂ) +
      Complex.I * (G i (j, (1 : Fin 2)) : ℂ)) / (Real.sqrt 2 : ℂ)

/-- Exponential upper and lower tails for the averaged Gaussian trace
estimator, in the real and complex settings. The complex exponents carry the
source's extra factor of two. -/
theorem trace_estimator_exp (n : ℕ) :
    (∀ (A : Matrix (Fin n) (Fin n) ℝ), PsdSymMatrix A → A ≠ 0 →
      ∀ (τ : ℝ), 1 < τ → ∀ (k : ℕ), k ≤ n →
      ∀ (Ω : Type*) [MeasurableSpace Ω] (P : Measure Ω)
        (W : Ω → Matrix (Fin k) (Fin n) ℝ),
        StandardGaussianTestMatrix P W →
          (P {ω | averageTraceSample A (W ω) ≥
                τ * Matrix.trace A} ≤
              ENNReal.ofReal (Real.exp
                (-(1 / 2 : ℝ) * (k : ℝ) * intrinsicDimension A *
                  (Real.sqrt τ - 1) ^ 2)) ∧
           P {ω | averageTraceSample A (W ω) ≤
                τ⁻¹ * Matrix.trace A} ≤
              ENNReal.ofReal (Real.exp
                (-(1 / 4 : ℝ) * (k : ℝ) * intrinsicDimension A *
                  (τ⁻¹ - 1) ^ 2)))) ∧
    (∀ (A : Matrix (Fin n) (Fin n) ℂ), PsdSymMatrix A → A ≠ 0 →
      ∀ (τ : ℝ), 1 < τ → ∀ (k : ℕ), k ≤ n →
      ∀ (Ω : Type*) [MeasurableSpace Ω] (P : Measure Ω)
        (G : Ω → Matrix (Fin k) (Fin n × Fin 2) ℝ),
        StandardGaussianTestMatrix P G →
          (P {ω | averageTraceSample A (complexStandardNormalSamples (G ω)) ≥
                τ * RCLike.re (Matrix.trace A)} ≤
              ENNReal.ofReal (Real.exp
                (-(2 : ℝ) * ((1 / 2 : ℝ) * (k : ℝ) *
                  intrinsicDimension A * (Real.sqrt τ - 1) ^ 2))) ∧
           P {ω | averageTraceSample A (complexStandardNormalSamples (G ω)) ≤
                τ⁻¹ * RCLike.re (Matrix.trace A)} ≤
              ENNReal.ofReal (Real.exp
                (-(2 : ℝ) * ((1 / 4 : ℝ) * (k : ℝ) *
                  intrinsicDimension A * (τ⁻¹ - 1) ^ 2))))) := by
  sorry

end RNLAPhaseB.TraceEstExp

How to read the formalization

Real and complex cases are stated separately. In the complex case both exponents receive an additional factor of two.

← Back to all statements