Provedrandomized-conversionconversion-theoremattention-compute-lawmedian-of-means

Chebyshev for the average of k iid draws on the exact product space: P(|avg − p| ≥ ε) ≤ σ²/(k ε²)

For all $\htmlData{mx=1}{\Omega \in \htmlData{mx=0}{\operatorname{Type}}}$ , $\htmlData{mx=1}{k \in \htmlData{mx=0}{\mathbb{N}}}$ , $\htmlData{mx=3}{w, X : \htmlData{mx=0}{\Omega} \mathrel{\htmlData{mx=2}{\to}} \htmlData{mx=1}{\mathbb{R}}}$ and $\htmlData{mx=1}{p, \sigma_{2}, \varepsilon \in \htmlData{mx=0}{\mathbb{R}}}$ , if $0 \mathrel{\htmlData{mx=1}{<}} \htmlData{mx=0}{k}$ , $0 \mathrel{\htmlData{mx=1}{<}} \htmlData{mx=0}{\varepsilon}$ , $\htmlData{mx=4}{\forall \omega,\ 0 \mathrel{\htmlData{mx=3}{\leq}} \htmlData{mx=2}{\htmlData{mx=0}{w}(\htmlData{mx=1}{\omega})}}$ , $\htmlData{mx=3}{\sum_{\omega} \htmlData{mx=2}{\htmlData{mx=0}{w}(\htmlData{mx=1}{\omega})}} \mathrel{\htmlData{mx=4}{=}} 1$ , $\htmlData{mx=7}{\sum_{\omega} \htmlData{mx=6}{\htmlData{mx=2}{\htmlData{mx=0}{w}(\htmlData{mx=1}{\omega})} \cdot \htmlData{mx=5}{\htmlData{mx=3}{X}(\htmlData{mx=4}{\omega})}}} \mathrel{\htmlData{mx=9}{=}} \htmlData{mx=8}{p}$ and $\htmlData{mx=10}{\sum_{\omega} \htmlData{mx=9}{\htmlData{mx=2}{\htmlData{mx=0}{w}(\htmlData{mx=1}{\omega})} \cdot \htmlData{mx=8}{(\htmlData{mx=7}{\htmlData{mx=5}{\htmlData{mx=3}{X}(\htmlData{mx=4}{\omega})} - \htmlData{mx=6}{p}})^{2}}}} \mathrel{\htmlData{mx=12}{\leq}} \htmlData{mx=11}{\sigma_{2}}$ (given $\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Fintype}}\,\htmlData{mx=1}{\Omega}}$ ), then

\htmlData{mx=27}{\sum_{f \in \htmlData{mx=20}{\htmlData{mx=0}{\operatorname{filter}}\left(\htmlData{mx=19}{f \mapsto \htmlData{mx=1}{\varepsilon} \mathrel{\htmlData{mx=13}{\leq}} \htmlData{mx=12}{\left\lvert \htmlData{mx=11}{\htmlData{mx=9}{\frac{\htmlData{mx=7}{\sum_{i} \htmlData{mx=6}{\htmlData{mx=2}{X}(\htmlData{mx=5}{\htmlData{mx=3}{f}(\htmlData{mx=4}{i})})}}}{\htmlData{mx=8}{k}}} - \htmlData{mx=10}{p}} \right\rvert}}\right)}} \htmlData{mx=26}{\prod_{i} \htmlData{mx=25}{\htmlData{mx=21}{w}(\htmlData{mx=24}{\htmlData{mx=22}{f}(\htmlData{mx=23}{i})})}}} \mathrel{\htmlData{mx=34}{\leq}} \htmlData{mx=33}{\frac{\htmlData{mx=28}{\sigma_{2}}}{\htmlData{mx=32}{\htmlData{mx=29}{k} \cdot \htmlData{mx=31}{\htmlData{mx=30}{\varepsilon}^{2}}}}}

What the notation means · or point at any symbol

Type: Type: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Type)
Fintype: Fintype: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Fintype)
f(x)Function application: Fintype applied to Ω. Lean writes f x; papers write f(x). (Fintype Ω)
NNatural numbers: The natural numbers 0, 1, 2, …. In Lean they start at 0. (ℕ)
⟹Implies: If Ω, then ℝ. (Between types, A → B is the type of functions from A to B.) (Ω → ℝ)
x : TVariables: w, X range over Ω → ℝ: the statement must hold for every choice. ((w X : Ω → ℝ))
x ∈ TVariables: p, σ2, ε range over real numbers: the statement must hold for every choice. ((p σ2 ε : ℝ))
<Less than: 0 is strictly smaller than k. (0 < k)
∀For all: The statement after the comma holds for every ω. (∀ ω, 0 ≤ w ω)
∑Summation: Add up w(ω) for every ω. (∑ ω, w ω)
=Equality: ∑ ω, w(ω) and 1 are the same. (∑ ω, w ω = 1)
RReal numbers: The real numbers: every point on the number line. (ℝ)
≤At most: 0 is less than or equal to w(ω). (0 ≤ w ω)
·Multiplication: w(ω) times X(ω). (w ω * X ω)
filter: Finset.univ.filter: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Finset.univ.filter)
aᵇPower: X(ω) − p raised to the power 2. ((X ω - p) ^ 2)
-Subtraction: X(ω) minus p. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (X ω - p)
x ↦ f(x)Function (λ-abstraction): The function sending f to ε ≤ |(∑ i, X(f(i)))/k − p|. Lean writes fun x => …; papers write x ↦ …. (fun f : Fin k → Ω => ε ≤ |(∑ i, X (f i)…)
Fin: Fin: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Fin)
|x|Absolute value: The size of (∑ i, X(f(i)))/k − p without its sign. (|(∑ i, X (f i)) / k - p|)
a/bDivision: ∑ i, X(f(i)) divided by k. In Lean, dividing by 0 gives 0. ((∑ i, X (f i)) / k)
∏Product: Multiply together w(f(i)) for every i. (∏ i, w (f i))

theorem rc-average-chebyshev {Ω : Type} [Fintype Ω] {k : ℕ} (w X : Ω → ℝ) (p σ2 ε : ℝ) (hk : 0 < k) (hε : 0 < ε) (hw : ∀ ω, 0 ≤ w ω) (hsum : ∑ ω, w ω = 1) (hmean : ∑ ω, w ω * X ω = p) (hvar : ∑ ω, w ω * (X ω - p) ^ 2 ≤ σ2) :
    ∑ f ∈ Finset.univ.filter (fun f : Fin k → Ω => ε ≤ |(∑ i, X (f i)) / k - p|), ∏ i, w (f i) ≤ σ2 / (k * ε ^ 2)

A bounded-variance randomized oracle averaged over k = 4σ²/ε² independent runs is ε-accurate with probability ≥ 3/4, giving the base step of the median-of-means boost. Proven on the finite product space with the iid second-moment identity inlined. Part of the Randomized Conversion Theorem: the Conversion Theorem (counting ⇒ sampling descent) extended to every randomized bounded-variance attention algorithm via median-of-means boosting, a union bound over the 2n descent nodes, and ε-smoothing of each node; closes the residual scalability crux of the Attention Compute Law.

How it was proved

Proved: 4 October 2026
By: Ajax, with the agent “Baguette math & proofs (Claude Code, 2026-10-03)”
Checked by: Lean's kernel (Lean 4.33.1, with Mathlib); the proof is signed and replays offline
Axioms: Classical.choice, Quot.sound, propext
Proof: 95 lines of Lean

Chebyshev for the average of k iid draws on the exact product space: P(|avg − p| ≥ ε) ≤ σ²/(k ε²)

How it was proved

More proved statements