Exactly unbiased Lipschitz functionals of the dense computation: finite-terminal MLMC with E‖X_ℓ − x⋆‖² ≤ c/2^ℓ and X_L = x⋆ gives E[Z] = Φ(x⋆), MSE ≤ (2+12L)Lip²c, work ≤ 3L
For all , , , , , , , , and , if , , , , , , , , , and (given ), then
What the notation means · or point at any symbol
- NNatural numbers
- The natural numbers 0, 1, 2, …. In Lean they start at 0. (
ℕ) - x ∈ TVariables
- L, dim range over natural numbers: the statement must hold for every choice. (
(L dim : ℕ)) - 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 Ω) - ≤At most
- 1 is less than or equal to L. (
1 ≤ L) - ⟹Implies
- If Ω, then ℝ. (Between types, A → B is the type of functions from A to B.) (
Ω → ℝ) - ∀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) - x : TVariables
- p, cost range over ℕ → ℝ: the statement must hold for every choice. (
(p cost : ℕ → ℝ)) - RReal numbers
- The real numbers: every point on the number line. (
ℝ) - <Less than
- l is strictly smaller than L. (
l < L) - 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) - ·Multiplication
- w(ω) times ∑ i, (X(l, ω, i) − xstar(i))^2. (
w ω * ∑ i, (X l ω i - xstar i) ^ 2) - (x : T)As real numbers
- 1/2 read as an element of real numbers. Mathematicians leave this implicit; Lean needs it to know which kind of number is meant. (
(1 / 2 : ℝ)) - aᵇPower
- X(l, ω, i) − xstar(i) raised to the power 2. (
(X l ω i - xstar i) ^ 2) - -Subtraction
- X(l, ω, i) minus xstar(i). On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (
X l ω i - xstar i) - +Addition
- l plus 1. (
l + 1) - a/bDivision
- c divided by 2^l. In Lean, dividing by 0 gives 0. (
c / 2 ^ l) - ∧And
- Both hold: (∑ l, ∑ ω, p(l) · w(ω) · (Y(0, ω) + (Y(l + 1, ω) − Y(l, ω)…, and (∑ l, p(l) · (cost(l) + cost(l + 1))) ≤ 3 · L. (
(∑ l ∈ Finset.range L, ∑ ω, p l * w ω *…)
theorem ua-mlmc-lipschitz-functional {L dim : ℕ} {Ω : Type} [Fintype Ω] (hL : 1 ≤ L) (w : Ω → ℝ) (hw : ∀ ω, 0 ≤ w ω) (hsum : ∑ ω, w ω = 1) (X : ℕ → Ω → (Fin dim → ℝ)) (xstar : Fin dim → ℝ) (Φ : (Fin dim → ℝ) → ℝ) (Lip c S : ℝ) (p cost : ℕ → ℝ) (hterm : ∀ ω, X L ω = xstar) (hlev : ∀ l, l < L → ∑ ω, w ω * ∑ i, (X l ω i - xstar i) ^ 2 ≤ c / 2 ^ l) (hLip : ∀ x y, (Φ x - Φ y) ^ 2 ≤ Lip ^ 2 * ∑ i, (x i - y i) ^ 2) (hS : S = ∑ k ∈ Finset.range L, (1 / 2 : ℝ) ^ k) (hp : ∀ l, p l = (1 / 2 : ℝ) ^ l / S) (hcost : ∀ l, l ≤ L → cost l ≤ 2 ^ l) (Y : ℕ → Ω → ℝ) (hY : ∀ l ω, Y l ω = Φ (X l ω)) (o : ℝ) (ho : o = Φ xstar) :
(∑ l ∈ Finset.range L, ∑ ω, p l * w ω * (Y 0 ω + (Y (l + 1) ω - Y l ω) / p l) = o) ∧ (∑ l ∈ Finset.range L, ∑ ω, p l * w ω * (Y 0 ω + (Y (l + 1) ω - Y l ω) / p l - o) ^ 2 ≤ (2 + 12 * L) * (Lip ^ 2 * c)) ∧ (∑ l ∈ Finset.range L, p l * (cost l + cost (l + 1)) ≤ 3 * L)The positive training theorem. Let X_ℓ be vector-valued level estimates of a dense quantity x⋆ (the vector of all attention outputs of a network at sample budget 2^ℓ per head), coupled on one probability space, with the exact dense computation as the last level, and let Φ be any Lip-Lipschitz functional (a coordinate of the dense loss gradient, as a function of the attention outputs, on a bounded domain). The randomised telescope over Φ(X_ℓ) is exactly unbiased for Φ(x⋆), with mean squared error ≤ (2+12L)·Lip²c and expected cost of the sampled level pair ≤ 3L. So exactly unbiased gradients of the DENSE objective are possible with sampled attention, at an expected overhead of O(log n) samples per head and a dense pass with probability Θ(1/n), with a variance price Lip²·(2+12L). Counterpart to the sample-reuse counterexample, which shows the naive route is biased. First-principles reformulation, 2026-10-05.
How it was proved
- Proved
- 5 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
- 127 lines of Lean