Provedcertified-residual-attentioncontrol-variatesvariance

Residual attention estimator: exact expectation, variance identity, and zero-residual exactness

For all $\htmlData{mx=1}{J \in \htmlData{mx=0}{\operatorname{Type}}}$ and $\htmlData{mx=3}{\pi, r, v, g : \htmlData{mx=0}{J} \mathrel{\htmlData{mx=2}{\to}} \htmlData{mx=1}{\mathbb{R}}}$ , if $\htmlData{mx=4}{\forall j,\ 0 \mathrel{\htmlData{mx=3}{\leq}} \htmlData{mx=2}{\htmlData{mx=0}{\pi}(\htmlData{mx=1}{j})}}$ , $\htmlData{mx=3}{\sum_{j} \htmlData{mx=2}{\htmlData{mx=0}{\pi}(\htmlData{mx=1}{j})}} \mathrel{\htmlData{mx=4}{=}} 1$ , $\htmlData{mx=4}{\forall j,\ 0 \mathrel{\htmlData{mx=3}{<}} \htmlData{mx=2}{\htmlData{mx=0}{r}(\htmlData{mx=1}{j})}}$ and $\htmlData{mx=3}{\sum_{j} \htmlData{mx=2}{\htmlData{mx=0}{r}(\htmlData{mx=1}{j})}} \mathrel{\htmlData{mx=4}{=}} 1$ (given $\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Fintype}}\,\htmlData{mx=1}{J}}$ ), then

\htmlData{mx=4}{\htmlData{mx=3}{\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{let}}(\htmlData{mx=1}{b})}}(\mathtt{:=\ \Sigma \ j,\ {\pi}\ j\ *\ g\ j\ let\ o\ :\ \text{ℝ}\ :=\ \Sigma \ j,\ {\pi}\ j\ *\ v\ j\ let\ E\ :\ J\ \to \ \text{ℝ}\ :=\ fun\ j\ =>\ b\ +\ ({\pi}\ j\ /\ r\ j)\ *\ (v\ j\ -\ g\ j)\ (\Sigma \ j,\ r\ j\ *\ E\ j\ =\ o)\ \text{∧}\ (\Sigma \ j,\ r\ j\ *\ (E\ j\ -\ o)\ \^\ 2\ =\ (\Sigma \ j,\ {\pi}\ j\ \^\ 2\ *\ (v\ j\ -\ g\ j)\ \^\ 2\ /\ r\ j)\ -\ (\Sigma \ j,\ {\pi}\ j\ *\ (v\ j\ -\ g\ j))\ \^\ 2)\ \text{∧}\ (\Sigma \ j,\ r\ j\ *\ (E\ j\ -\ o)\ \^\ 2\ \leq \ \Sigma \ j,\ {\pi}\ j\ \^\ 2\ *\ (v\ j\ -\ g\ j)\ \^\ 2\ /\ r\ j)\ \text{∧}\ ((\forall \ j,\ v\ j\ =\ g\ j)\ \to \ \forall \ j,\ E\ j\ =\ o))})}

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 J. Lean writes f x; papers write f(x). (Fintype J)
⟹Implies: If J, then ℝ. (Between types, A → B is the type of functions from A to B.) (J → ℝ)
x : TVariables: π, r, v, g range over J → ℝ: the statement must hold for every choice. ((π r v g : J → ℝ))
∀For all: The statement after the comma holds for every j. (∀ j, 0 ≤ π j)
∑Summation: Add up π(j) for every j. (∑ j, π j)
=Equality: ∑ j, π(j) and 1 are the same. (∑ j, π j = 1)
(x : T)As real numbers: let(b) read as an element of real numbers. Mathematicians leave this implicit; Lean needs it to know which kind of number is meant. ((let b : ℝ)
let: let: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (let)
RReal numbers: The real numbers: every point on the number line. (ℝ)
≤At most: 0 is less than or equal to π(j). (0 ≤ π j)
<Less than: 0 is strictly smaller than r(j). (0 < r j)
πPi: The ratio of a circle's circumference to its diameter, ≈ 3.14159. (π)

theorem cra-residual-estimator-exact-moments {J : Type} [Fintype J] (π r v g : J → ℝ) (hπ : ∀ j, 0 ≤ π j) (hπs : ∑ j, π j = 1) (hr : ∀ j, 0 < r j) (hrs : ∑ j, r j = 1) :
    (let b : ℝ := ∑ j, π j * g j
let o : ℝ := ∑ j, π j * v j
let E : J → ℝ := fun j => b + (π j / r j) * (v j - g j)
(∑ j, r j * E j = o) ∧
(∑ j, r j * (E j - o) ^ 2 = (∑ j, π j ^ 2 * (v j - g j) ^ 2 / r j) - (∑ j, π j * (v j - g j)) ^ 2) ∧
(∑ j, r j * (E j - o) ^ 2 ≤ ∑ j, π j ^ 2 * (v j - g j) ^ 2 / r j) ∧
((∀ j, v j = g j) → ∀ j, E j = o))

On a finite probability space, a supplied exact control-variate mean plus importance-weighted residuals has the exact target mean. Its variance is sum pi²(v-g)²/r minus the squared residual mean. This theorem assumes normalized weights are supplied; it does not hide their computation or the control-variate mean inside a speed claim. Scalar values; vector and multi-head aggregation are separate results.

How it was proved

Proved: 5 October 2026
By: Ajax
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: 62 lines of Lean

Residual attention estimator: exact expectation, variance identity, and zero-residual exactness

How it was proved

More proved statements