Source defectFalse source claim · Explicit counterexample

Sampling optimality: a source defect

The source’s sampling-optimality claim is false on its stated probability domain. An explicit counterexample gives expected errors of 4 and 1.

Drineas & Mahoney ↗
RandMatrixMultiply · optimal sampling probabilities

Download Lean file ↓

Source defect. The sampling-optimality claim is false as stated. The counterexample below disproves it; the Lean declaration preserves the source claim with an omitted proof.

01 / MATHEMATICAL STATEMENT

Claim & counterexample

Mathematical summary

The source claims that norm-proportional sampling minimizes the exact expected squared Frobenius error over every nonnegative probability distribution summing to one. This claim is false as stated: the domain allows a zero sampling probability on a nonzero matrix contribution, and the counterexample below violates the asserted optimality.

A = [1, 1], B = [1, −1]ᵀ, c = 1
p* = (½, ½): E(p*) = 4
q = (1, 0): E(q) = 1

Assumptions & context

The source’s probability domain allows qᵢ = 0.
Sampling is independent and with replacement, with the stated rescaling.
The objective is the exact expectation, rather than only its upper bound.

Source

Drineas & Mahoney. Lectures on randomized numerical linear algebra.

RandMatrixMultiply · optimal sampling probabilities

02 / LEAN REPRESENTATION

Source claim in Lean

Target declaration, with proof omitted. The download includes imports and local definitions.

theorem lem_basicmult {m n d c : ℕ}
    (A : Matrix (Fin m) (Fin n) ℝ) (B : Matrix (Fin n) (Fin d) ℝ)
    (hc1 : 1 ≤ c) (hcn : c ≤ n)
    (p : Fin n → ℝ) (hp : ValidSamplingProbabilities p)
    {Ω : Type} [MeasurableSpace Ω] (P : Measure Ω) (idx : Ω → Fin c → Fin n)
    (hidx : IIDIndexSampling P p idx) :
    expectedSqError P A B p idx ≤
        ∑ k, ENNReal.ofReal (l2Norm (col A k) ^ 2 * l2Norm (row B k) ^ 2) /
          ((c : ℝ≥0∞) * ENNReal.ofReal (p k))
    ∧ ((∀ k, p k = optimalProbabilities A B k) →
        expectedSqError P A B p idx ≤
          ENNReal.ofReal ((1 / (c : ℝ)) *
            (∑ k, l2Norm (col A k) * l2Norm (row B k)) ^ 2))
    ∧ ((∀ k, p k = optimalProbabilities A B k) →
        ∀ q : Fin n → ℝ, ValidSamplingProbabilities q →
          ∀ (Ω' : Type) [MeasurableSpace Ω'] (P' : Measure Ω')
            (idx' : Ω' → Fin c → Fin n), IIDIndexSampling P' q idx' →
            expectedSqError P A B p idx ≤ expectedSqError P' A B q idx') := by
  sorry

03 / MATHEMATICAL NOTES

Why the claim fails

Here AB = 0. With p* = (½, ½), the sampled product is +2 or −2, giving squared error 4 in either case. With q = (1, 0), the sampled product is always 1, giving squared error 1.
Both distributions satisfy the stated constraints. Since 1 < 4, p* does not minimize the expected error on that domain.
The missing support condition is qᵢ > 0 whenever A[:,i] B[i,:] is nonzero. Adding it changes the claim’s domain; it is not part of the source statement shown here.
The Lean declaration preserves the false source claim with an omitted proof. It is a source-defect example and must not be used as an established computational guarantee.