Provedunbiased-attentiongradient-hardnesssampler-lower-bound

Gradient in one statement: three independent unbiased estimators A, B, C give G = A − B·C unbiased for Cov = E[uk] − E[u]E[k], with Var G ≤ 2Va + 2(VbVc + b²Vc + c²Vb)

For all $\htmlData{mx=1}{\Omega_{1}, \Omega_{2}, \Omega_{3} \in \htmlData{mx=0}{\operatorname{Type}}}$ , $\htmlData{mx=3}{w_{1} : \htmlData{mx=0}{\Omega_{1}} \mathrel{\htmlData{mx=2}{\to}} \htmlData{mx=1}{\mathbb{R}}}$ , $\htmlData{mx=3}{w_{2} : \htmlData{mx=0}{\Omega_{2}} \mathrel{\htmlData{mx=2}{\to}} \htmlData{mx=1}{\mathbb{R}}}$ , $\htmlData{mx=3}{w_{3} : \htmlData{mx=0}{\Omega_{3}} \mathrel{\htmlData{mx=2}{\to}} \htmlData{mx=1}{\mathbb{R}}}$ , $\htmlData{mx=3}{A : \htmlData{mx=0}{\Omega_{1}} \mathrel{\htmlData{mx=2}{\to}} \htmlData{mx=1}{\mathbb{R}}}$ , $\htmlData{mx=3}{B : \htmlData{mx=0}{\Omega_{2}} \mathrel{\htmlData{mx=2}{\to}} \htmlData{mx=1}{\mathbb{R}}}$ , $\htmlData{mx=3}{C : \htmlData{mx=0}{\Omega_{3}} \mathrel{\htmlData{mx=2}{\to}} \htmlData{mx=1}{\mathbb{R}}}$ and $\htmlData{mx=1}{a, b, c, \mathit{Va}, \mathit{Vb}, \mathit{Vc} \in \htmlData{mx=0}{\mathbb{R}}}$ , if $\htmlData{mx=4}{\forall x,\ 0 \mathrel{\htmlData{mx=3}{\leq}} \htmlData{mx=2}{\htmlData{mx=0}{w_{1}}(\htmlData{mx=1}{x})}}$ , $\htmlData{mx=3}{\sum_{x} \htmlData{mx=2}{\htmlData{mx=0}{w_{1}}(\htmlData{mx=1}{x})}} \mathrel{\htmlData{mx=4}{=}} 1$ , $\htmlData{mx=3}{\sum_{y} \htmlData{mx=2}{\htmlData{mx=0}{w_{2}}(\htmlData{mx=1}{y})}} \mathrel{\htmlData{mx=4}{=}} 1$ , $\htmlData{mx=3}{\sum_{z} \htmlData{mx=2}{\htmlData{mx=0}{w_{3}}(\htmlData{mx=1}{z})}} \mathrel{\htmlData{mx=4}{=}} 1$ , $\htmlData{mx=7}{\sum_{x} \htmlData{mx=6}{\htmlData{mx=2}{\htmlData{mx=0}{w_{1}}(\htmlData{mx=1}{x})} \cdot \htmlData{mx=5}{\htmlData{mx=3}{A}(\htmlData{mx=4}{x})}}} \mathrel{\htmlData{mx=9}{=}} \htmlData{mx=8}{a}$ , $\htmlData{mx=7}{\sum_{y} \htmlData{mx=6}{\htmlData{mx=2}{\htmlData{mx=0}{w_{2}}(\htmlData{mx=1}{y})} \cdot \htmlData{mx=5}{\htmlData{mx=3}{B}(\htmlData{mx=4}{y})}}} \mathrel{\htmlData{mx=9}{=}} \htmlData{mx=8}{b}$ , $\htmlData{mx=7}{\sum_{z} \htmlData{mx=6}{\htmlData{mx=2}{\htmlData{mx=0}{w_{3}}(\htmlData{mx=1}{z})} \cdot \htmlData{mx=5}{\htmlData{mx=3}{C}(\htmlData{mx=4}{z})}}} \mathrel{\htmlData{mx=9}{=}} \htmlData{mx=8}{c}$ , $\htmlData{mx=10}{\sum_{x} \htmlData{mx=9}{\htmlData{mx=2}{\htmlData{mx=0}{w_{1}}(\htmlData{mx=1}{x})} \cdot \htmlData{mx=8}{(\htmlData{mx=7}{\htmlData{mx=5}{\htmlData{mx=3}{A}(\htmlData{mx=4}{x})} - \htmlData{mx=6}{a}})^{2}}}} \mathrel{\htmlData{mx=12}{=}} \htmlData{mx=11}{\mathit{Va}}$ , $\htmlData{mx=10}{\sum_{y} \htmlData{mx=9}{\htmlData{mx=2}{\htmlData{mx=0}{w_{2}}(\htmlData{mx=1}{y})} \cdot \htmlData{mx=8}{(\htmlData{mx=7}{\htmlData{mx=5}{\htmlData{mx=3}{B}(\htmlData{mx=4}{y})} - \htmlData{mx=6}{b}})^{2}}}} \mathrel{\htmlData{mx=12}{=}} \htmlData{mx=11}{\mathit{Vb}}$ , $\htmlData{mx=10}{\sum_{z} \htmlData{mx=9}{\htmlData{mx=2}{\htmlData{mx=0}{w_{3}}(\htmlData{mx=1}{z})} \cdot \htmlData{mx=8}{(\htmlData{mx=7}{\htmlData{mx=5}{\htmlData{mx=3}{C}(\htmlData{mx=4}{z})} - \htmlData{mx=6}{c}})^{2}}}} \mathrel{\htmlData{mx=12}{=}} \htmlData{mx=11}{\mathit{Vc}}$ , $\htmlData{mx=4}{\forall y,\ 0 \mathrel{\htmlData{mx=3}{\leq}} \htmlData{mx=2}{\htmlData{mx=0}{w_{2}}(\htmlData{mx=1}{y})}}$ and $\htmlData{mx=4}{\forall z,\ 0 \mathrel{\htmlData{mx=3}{\leq}} \htmlData{mx=2}{\htmlData{mx=0}{w_{3}}(\htmlData{mx=1}{z})}}$ (given $\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Fintype}}\,\htmlData{mx=1}{\Omega_{1}}}$ , $\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Fintype}}\,\htmlData{mx=1}{\Omega_{2}}}$ and $\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Fintype}}\,\htmlData{mx=1}{\Omega_{3}}}$ ), then

\begin{aligned} & \left(\right. \htmlData{mx=27}{\sum_{x} \htmlData{mx=26}{\sum_{y} \htmlData{mx=25}{\sum_{z} \htmlData{mx=24}{\htmlData{mx=12}{\htmlData{mx=8}{\htmlData{mx=4}{\htmlData{mx=2}{w_{1}}(\htmlData{mx=3}{x})} \cdot \htmlData{mx=7}{\htmlData{mx=5}{w_{2}}(\htmlData{mx=6}{y})}} \cdot \htmlData{mx=11}{\htmlData{mx=9}{w_{3}}(\htmlData{mx=10}{z})}} \cdot (\htmlData{mx=23}{\htmlData{mx=15}{\htmlData{mx=13}{A}(\htmlData{mx=14}{x})} - \htmlData{mx=22}{\htmlData{mx=18}{\htmlData{mx=16}{B}(\htmlData{mx=17}{y})} \cdot \htmlData{mx=21}{\htmlData{mx=19}{C}(\htmlData{mx=20}{z})}}})}}}} \\ & \quad \htmlData{mx=1}{=} \htmlData{mx=32}{\htmlData{mx=28}{a} - \htmlData{mx=31}{\htmlData{mx=29}{b} \cdot \htmlData{mx=30}{c}}} \left.\right) \\ & \htmlData{mx=0}{\land} \left(\right. \htmlData{mx=66}{\sum_{x} \htmlData{mx=65}{\sum_{y} \htmlData{mx=64}{\sum_{z} \htmlData{mx=63}{\htmlData{mx=44}{\htmlData{mx=40}{\htmlData{mx=36}{\htmlData{mx=34}{w_{1}}(\htmlData{mx=35}{x})} \cdot \htmlData{mx=39}{\htmlData{mx=37}{w_{2}}(\htmlData{mx=38}{y})}} \cdot \htmlData{mx=43}{\htmlData{mx=41}{w_{3}}(\htmlData{mx=42}{z})}} \cdot \htmlData{mx=62}{(\htmlData{mx=61}{\htmlData{mx=55}{\htmlData{mx=47}{\htmlData{mx=45}{A}(\htmlData{mx=46}{x})} - \htmlData{mx=54}{\htmlData{mx=50}{\htmlData{mx=48}{B}(\htmlData{mx=49}{y})} \cdot \htmlData{mx=53}{\htmlData{mx=51}{C}(\htmlData{mx=52}{z})}}} - (\htmlData{mx=60}{\htmlData{mx=56}{a} - \htmlData{mx=59}{\htmlData{mx=57}{b} \cdot \htmlData{mx=58}{c}}})})^{2}}}}}} \\ & \quad \htmlData{mx=33}{\leq} \htmlData{mx=83}{\htmlData{mx=68}{2\htmlData{mx=67}{\mathit{Va}}} + \htmlData{mx=82}{2(\htmlData{mx=81}{\htmlData{mx=76}{\htmlData{mx=71}{\htmlData{mx=69}{\mathit{Vb}} \cdot \htmlData{mx=70}{\mathit{Vc}}} + \htmlData{mx=75}{\htmlData{mx=73}{\htmlData{mx=72}{b}^{2}} \cdot \htmlData{mx=74}{\mathit{Vc}}}} + \htmlData{mx=80}{\htmlData{mx=78}{\htmlData{mx=77}{c}^{2}} \cdot \htmlData{mx=79}{\mathit{Vb}}}})}} \left.\right) \end{aligned}

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)
x ∈ TVariables: Ω₁, Ω₂, Ω₃ range over Type: the statement must hold for every choice. ((Ω₁ Ω₂ Ω₃ : 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 Ω₁)
⟹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 x. (∀ x, 0 ≤ w₁ x)
∑Summation: Add up w₁(x) for every x. (∑ x, w₁ x)
=Equality: ∑ x, w₁(x) and 1 are the same. (∑ x, w₁ x = 1)
∧And: Both hold: (∑ x, ∑ y, ∑ z, w₁(x) · w₂(y) · w₃(z) · (A(x) − B(y) · C(z…, and (∑ x, ∑ y, ∑ z, w₁(x) · w₂(y) · w₃(z) · (A(x) − B(y) · C(z…. ((∑ x, ∑ y, ∑ z, w₁ x * w₂ y * w₃ z * (A…)
RReal numbers: The real numbers: every point on the number line. (ℝ)
≤At most: 0 is less than or equal to w₁(x). (0 ≤ w₁ x)
·Multiplication: w₁(x) times A(x). (w₁ x * A x)
aᵇPower: A(x) − a raised to the power 2. ((A x - a) ^ 2)
-Subtraction: A(x) minus a. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (A x - a)
+Addition: Vb · Vc plus b^2 · Vc. (Vb * Vc + b ^ 2 * Vc)

theorem ug-covariance-estimator {Ω₁ Ω₂ Ω₃ : Type} [Fintype Ω₁] [Fintype Ω₂] [Fintype Ω₃] (w₁ : Ω₁ → ℝ) (w₂ : Ω₂ → ℝ) (w₃ : Ω₃ → ℝ) (A : Ω₁ → ℝ) (B : Ω₂ → ℝ) (C : Ω₃ → ℝ) (a b c Va Vb Vc : ℝ) (hw1 : ∀ x, 0 ≤ w₁ x) (hs1 : ∑ x, w₁ x = 1) (hs2 : ∑ y, w₂ y = 1) (hs3 : ∑ z, w₃ z = 1) (hA : ∑ x, w₁ x * A x = a) (hB : ∑ y, w₂ y * B y = b) (hC : ∑ z, w₃ z * C z = c) (hVa : ∑ x, w₁ x * (A x - a) ^ 2 = Va) (hVb : ∑ y, w₂ y * (B y - b) ^ 2 = Vb) (hVc : ∑ z, w₃ z * (C z - c) ^ 2 = Vc) (hw2 : ∀ y, 0 ≤ w₂ y) (hw3 : ∀ z, 0 ≤ w₃ z) :
    (∑ x, ∑ y, ∑ z, w₁ x * w₂ y * w₃ z * (A x - B y * C z) = a - b * c) ∧ (∑ x, ∑ y, ∑ z, w₁ x * w₂ y * w₃ z * (A x - B y * C z - (a - b * c)) ^ 2 ≤ 2 * Va + 2 * (Vb * Vc + b ^ 2 * Vc + c ^ 2 * Vb))

The conditional positive result for gradients as a single Lean statement on the product space: the query gradient is a covariance of three attention expectations, so three debiased forward calls through the same proposal give an unbiased gradient with variance a fixed polynomial of the forward variances. Gradient cost = O(forward cost) under any proposal; combined with the sampler lower bound (ug-planted-gradient-gap) the gradient side of the law is matched above and below on the unconditional axis. Part of 'Unbiased randomized attention: cost x variance thresholds', gradient-hardness round: the unconditional sampler lower bound transferred to the query gradient.

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: 63 lines of Lean

Gradient in one statement: three independent unbiased estimators A, B, C give G = A − B·C unbiased for Cov = E[uk] − E[u]E[k], with Var G ≤ 2Va + 2(VbVc + b²Vc + c²Vb)

How it was proved

More proved statements