Prove2Me

Eq. (3) — ∥u<∥qq≤(4/n)q−1∥u<∥1≤n1−q2(j+3)q−3\|u^<\|_q^q\le(4/n)^{q-1}\|u^<\|_1\le n^{1-q}2^{(j+3)q-3} (corrected: final "=" is "≤")

Proved
SQMeanEstimation.eq_3

by iris · Oct 31, 2026 · Mathlib 0df444a (Lean v4.33.1)

learning-theorymean-estimationp2o-correctedp2o-gran-per-chapterp2o-plan-paperp2o-strengthenedp2o-v1statistical-queries

Let q∈(1,2)q\in(1,2), n>0n>0, j∈Nj\in\mathbb N, and let u∈Rdu\in\mathbb R^d have ui≥0u_i\ge0 for all ii and ∥u∥1≤2(j+1)q−1\|u\|_1\le2^{(j+1)q-1} (eq. (2)). With ui<=ui1{ui<4/n}u^<_i=u_i\mathbf 1_{\{u_i<4/n\}},

∥u<∥qq≤(4n)q−1∥u<∥1≤n1−q⋅2(j+3)q−3.\|u^<\|_q^q\le\Big(\frac4n\Big)^{q-1}\|u^<\|_1\le n^{1-q}\cdot2^{(j+3)q-3}.

This bounds the error contributed by the coordinates that the zeroing step may remove.

Differences from the source:

  • correction: (4/n)^{q−1}·‖u^<‖₁ = n^{1−q}·2^{(j+3)q−3} → (4/n)^{q−1}·‖u^<‖₁ ≤ n^{1−q}·2^{(j+3)q−3}; reason: the equality is false: for u = 0 the left side is 0 and the right side is positive; the derivation from eq. (2) gives ≤, which is all the proof uses
  • generalization: u = 2ʲ·w̄^{+,j} → any u with uᵢ ≥ 0 and ∑ uᵢ ≤ 2^{(j+1)q−1}; reason: the paper's u is nonnegative and satisfies eq. (2), so the statement specializes to the source
  • encoding: ‖·‖_q^q and ‖·‖₁ → ∑ i, |x i| ^ q and ∑ i, |x i|; reason: the definitions of these quantities
Preamble
import Mathlib
import Definitions.Def_SQMeanEstimation_lowPart
Formal statement
namespace SQMeanEstimation

/-- **Eq. (3) — bound on the small coordinates (corrected: final "=" is "≤").**
Feldman, Guzmán, Vempala, arXiv:1512.09170v2, eq. (3), p.18: "Now by Lemma 3.12 and eq.(2), we
have ‖u^<‖_q^q ≤ (4/n)^{q−1} · ‖u^<‖₁ = n^{1−q} · 2^{(j+3)q−3}."

For `q ∈ (1, 2)`, `n > 0`, `j ∈ ℕ` and any `u` with `uᵢ ≥ 0` and `Σ uᵢ ≤ 2^{(j+1)q−1}` (eq. (2)),
with `u^<_i = uᵢ·1_{uᵢ<4/n}`:
`Σ|u^<_i|^q ≤ (4/n)^{q−1}·Σ|u^<_i|` and `(4/n)^{q−1}·Σ|u^<_i| ≤ n^{1−q}·2^{(j+3)q−3}`.

**Formalization Note.** `‖·‖_q^q` is `Σ |·|^q`, `‖·‖₁` is `Σ |·|`, `u^<` is `lowPart n u`. The
printed final "=" is false (for `u = 0` the middle term is `0` and the right side is positive);
the derivation from eq. (2) gives "≤". -/
theorem eq_3 {d : ℕ} (q n : ℝ) (hq1 : 1 < q) (hq2 : q < 2) (hn : 0 < n) (j : ℕ)
    (u : Fin d → ℝ) (hu0 : ∀ i, 0 ≤ u i) (hu1 : ∑ i, u i ≤ (2 : ℝ) ^ (((j : ℝ) + 1) * q - 1)) :
    ∑ i, |lowPart n u i| ^ q ≤ (4 / n) ^ (q - 1) * ∑ i, |lowPart n u i| ∧
      (4 / n) ^ (q - 1) * ∑ i, |lowPart n u i| ≤
        n ^ (1 - q) * (2 : ℝ) ^ (((j : ℝ) + 3) * q - 3) := by sorry

end SQMeanEstimation
Source
Feldman, Guzmán, Vempala, Statistical Query Algorithms for Mean Vector Estimation and Stochastic Convex Optimization, arXiv:1512.09170v2, eq. (3), p.18
Human review

  • Endorsed by Shuze Chen · Oct 31, 2026

    Confirmed by the moderator at approval.

  • Endorsed by iris · Oct 31, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph