AcceptedLemma · Statement with omitted proof

Sufficient sketch conditions for least squares

Two geometric sketch conditions control both residual error and solution error.

Drineas & Mahoney ↗
Source label: lem:suff_cond

Download Lean file ↓

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

01 / MATHEMATICAL STATEMENT

Meaning & conditions

Mathematical summary

Two geometric sketch conditions control both residual error and solution error.

\|A\widetilde x-b\|_2\le(1+\epsilon)\mathcal Z,\qquad \|x_{\rm opt}-\widetilde x\|_2\le\frac{\sqrt\epsilon\,\mathcal Z}{\sigma_{\min}(A)}

Assumptions & context

The sketch preserves a lower singular-value bound on the column basis and controls its interaction with b⊥; 0 < ε < 1.

Source

Drineas & Mahoney. Lectures on randomized numerical linear algebra.

Source label: lem:suff_cond

02 / LEAN REPRESENTATION

Formal statement

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

theorem lem_suff_cond {r n d : ℕ}
    (A : Matrix (Fin n) (Fin d) ℝ) (b : Fin n → ℝ)
    (U : Matrix (Fin n) (Fin d) ℝ)
    (hU : IsTopLeftSingularVectors A U)
    (hcol : matrixColumnSpace U = matrixColumnSpace A)
    (Ap : Matrix (Fin d) (Fin n) ℝ) (hAp : IsMoorePenroseInverse A Ap)
    (X : Matrix (Fin r) (Fin n) ℝ) (ε : ℝ) (hε0 : 0 < ε) (hε1 : ε < 1)
    (h1 : Condition1 X U) (h2 : Condition2 X A U b ε)
    (xt : Fin d → ℝ) (hxt : IsSketchedLSSolution X A b xt) :
    l2Norm (A *ᵥ xt - b) ≤ (1 + ε) * lsOptimalResidual A b ∧
    l2Norm (Ap *ᵥ b - xt) ≤
      1 / sigmaMin A * Real.sqrt ε * lsOptimalResidual A b := by
  sorry

Complete Lean file and local definitions

import RNLAPhaseB.B3Base
import RNLAPhaseB.Complexity

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

namespace RNLAPhaseB.DM2017SuffCond

/-- `Z = min_{x ∈ ℝ^d} ‖A x - b‖₂` (Eqn. eqn:orig_ls_prob). -/
noncomputable def lsOptimalResidual {n d : ℕ} (A : Matrix (Fin n) (Fin d) ℝ)
    (b : Fin n → ℝ) : ℝ :=
  ⨅ x : Fin d → ℝ, l2Norm (A *ᵥ x - b)

/-- Moore–Penrose conditions: `Ap` is the generalized inverse `A†` of `A`. -/
def IsMoorePenroseInverse {n d : ℕ} (A : Matrix (Fin n) (Fin d) ℝ)
    (Ap : Matrix (Fin d) (Fin n) ℝ) : Prop :=
  A * Ap * A = A ∧ Ap * A * Ap = Ap ∧ (A * Ap)ᵀ = A * Ap ∧ (Ap * A)ᵀ = Ap * A

/-- Smallest singular value of an `r × d` real matrix, via the variational
characterization `σ_min(M) = min_{‖z‖₂ = 1} ‖M z‖₂` (the least of its `d`
singular values). -/
noncomputable def sigmaMin {r d : ℕ} (M : Matrix (Fin r) (Fin d) ℝ) : ℝ :=
  ⨅ z : {z : Fin d → ℝ // l2Norm z = 1}, l2Norm (M *ᵥ z.1)

/-- `U` contains the top `d` left singular vectors of `A`: `U` has orthonormal
columns and `A = U Σ Vᵀ` with `Σ` diagonal with nonnegative nonincreasing
entries (the singular values) and `V` orthogonal. -/
def IsTopLeftSingularVectors {n d : ℕ} (A : Matrix (Fin n) (Fin d) ℝ)
    (U : Matrix (Fin n) (Fin d) ℝ) : Prop :=
  Uᵀ * U = 1 ∧
    ∃ (s : Fin d → ℝ) (V : Matrix (Fin d) (Fin d) ℝ),
      Vᵀ * V = 1 ∧ (∀ i, 0 ≤ s i) ∧ Antitone s ∧
      A = U * Matrix.diagonal s * Vᵀ

/-- `b^⊥ = U_A^⊥ (U_A^⊥)ᵀ b = (I - U_A U_Aᵀ) b`, the part of `b` outside the
column space of `A`. -/
noncomputable def bPerp {n d : ℕ} (U : Matrix (Fin n) (Fin d) ℝ) (b : Fin n → ℝ) :
    Fin n → ℝ :=
  b - U *ᵥ (Uᵀ *ᵥ b)

/-- Condition (eqn:lemma1_ass1): `σ_min²(X U_A) ≥ 1/√2`. -/
def Condition1 {r n d : ℕ} (X : Matrix (Fin r) (Fin n) ℝ)
    (U : Matrix (Fin n) (Fin d) ℝ) : Prop :=
  sigmaMin (X * U) ^ 2 ≥ 1 / Real.sqrt 2

/-- Condition (eqn:lemma1_ass2): `‖U_Aᵀ Xᵀ X b^⊥‖₂² ≤ ε Z² / 2`. -/
def Condition2 {r n d : ℕ} (X : Matrix (Fin r) (Fin n) ℝ)
    (A : Matrix (Fin n) (Fin d) ℝ) (U : Matrix (Fin n) (Fin d) ℝ)
    (b : Fin n → ℝ) (ε : ℝ) : Prop :=
  l2Norm ((Uᵀ * Xᵀ * X) *ᵥ bPerp U b) ^ 2 ≤ ε * lsOptimalResidual A b ^ 2 / 2

/-- `x̃` solves the down-scaled least-squares problem induced by `X`
(eqn:orig_ls_prob_Xrotated): it minimizes `‖X A x - X b‖₂` over `x ∈ ℝ^d`. -/
def IsSketchedLSSolution {r n d : ℕ} (X : Matrix (Fin r) (Fin n) ℝ)
    (A : Matrix (Fin n) (Fin d) ℝ) (b : Fin n → ℝ) (xt : Fin d → ℝ) : Prop :=
  ∀ x : Fin d → ℝ, l2Norm ((X * A) *ᵥ xt - X *ᵥ b) ≤ l2Norm ((X * A) *ᵥ x - X *ᵥ b)

/-- Lemma lem:suff_cond (Drineas–Mahoney 2017). -/
theorem lem_suff_cond {r n d : ℕ}
    (A : Matrix (Fin n) (Fin d) ℝ) (b : Fin n → ℝ)
    (U : Matrix (Fin n) (Fin d) ℝ)
    (hU : IsTopLeftSingularVectors A U)
    (hcol : matrixColumnSpace U = matrixColumnSpace A)
    (Ap : Matrix (Fin d) (Fin n) ℝ) (hAp : IsMoorePenroseInverse A Ap)
    (X : Matrix (Fin r) (Fin n) ℝ) (ε : ℝ) (hε0 : 0 < ε) (hε1 : ε < 1)
    (h1 : Condition1 X U) (h2 : Condition2 X A U b ε)
    (xt : Fin d → ℝ) (hxt : IsSketchedLSSolution X A b xt) :
    l2Norm (A *ᵥ xt - b) ≤ (1 + ε) * lsOptimalResidual A b ∧
    l2Norm (Ap *ᵥ b - xt) ≤
      1 / sigmaMin A * Real.sqrt ε * lsOptimalResidual A b := by
  sorry

end RNLAPhaseB.DM2017SuffCond

How to read the formalization

The optimal residual, least-squares solution and Moore–Penrose inverse are explicitly represented. Both conclusions refer to the original unsketched problem.

← Back to all statements