Provedcertified-residual-attentionoptimal-proposalaccess-costcontrol-variates

Cost-aware residual proposal: sharp cost × second-moment lower bound and an explicit minimizer

For all $\htmlData{mx=1}{J \in \htmlData{mx=0}{\operatorname{Type}}}$ and $\htmlData{mx=3}{A, c, r : \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}{A}(\htmlData{mx=1}{j})}}$ , $\htmlData{mx=4}{\forall j,\ 0 \mathrel{\htmlData{mx=3}{<}} \htmlData{mx=2}{\htmlData{mx=0}{c}(\htmlData{mx=1}{j})}}$ , $\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}}$ and $\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Nonempty}}\,\htmlData{mx=1}{J}}$ ), then

\htmlData{mx=39}{\htmlData{mx=9}{\left(\htmlData{mx=8}{\sum_{j} \htmlData{mx=7}{\sqrt{\htmlData{mx=6}{\htmlData{mx=2}{\htmlData{mx=0}{A}(\htmlData{mx=1}{j})} \cdot \htmlData{mx=5}{\htmlData{mx=3}{c}(\htmlData{mx=4}{j})}}}}}\right)^{2}} \mathrel{\htmlData{mx=27}{\leq}} \htmlData{mx=26}{\left(\htmlData{mx=17}{\sum_{j} \htmlData{mx=16}{\htmlData{mx=12}{\htmlData{mx=10}{r}(\htmlData{mx=11}{j})} \cdot \htmlData{mx=15}{\htmlData{mx=13}{c}(\htmlData{mx=14}{j})}}}\right) \cdot \left(\htmlData{mx=25}{\sum_{j} \htmlData{mx=24}{\frac{\htmlData{mx=20}{\htmlData{mx=18}{A}(\htmlData{mx=19}{j})}}{\htmlData{mx=23}{\htmlData{mx=21}{r}(\htmlData{mx=22}{j})}}}}\right)} \mathbin{\htmlData{mx=38}{\land}} ((\htmlData{mx=32}{\forall j,\ 0 \mathrel{\htmlData{mx=31}{<}} \htmlData{mx=30}{\htmlData{mx=28}{A}(\htmlData{mx=29}{j})}}) \mathrel{\htmlData{mx=37}{\implies}} \htmlData{mx=36}{\htmlData{mx=35}{\htmlData{mx=33}{\operatorname{let}}(\htmlData{mx=34}{q})}})(\mathtt{:=\ fun\ j\ =>\ Real.sqrt\ (A\ j\ /\ c\ j)\ let\ rstar\ :\ J\ \to \ \text{ℝ}\ :=\ fun\ j\ =>\ q\ j\ /\ \Sigma \ k,\ q\ k\ (\forall \ j,\ 0\ <\ rstar\ j)\ \text{∧}\ (\Sigma \ j,\ rstar\ j\ =\ 1)\ \text{∧}\ ((\Sigma \ j,\ rstar\ j\ *\ c\ j)\ *\ (\Sigma \ j,\ A\ j\ /\ rstar\ j)\ =\ (\Sigma \ j,\ Real.sqrt\ (A\ j\ *\ c\ j))\ \^\ 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 J. Lean writes f x; papers write f(x). (Fintype J)
Nonempty: Nonempty: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Nonempty)
⟹Implies: If J, then ℝ. (Between types, A → B is the type of functions from A to B.) (J → ℝ)
x : TVariables: A, c, r range over J → ℝ: the statement must hold for every choice. ((A c r : J → ℝ))
∀For all: The statement after the comma holds for every j. (∀ j, 0 ≤ A j)
∑Summation: Add up r(j) for every j. (∑ j, r j)
=Equality: ∑ j, r(j) and 1 are the same. (∑ j, r j = 1)
∧And: Both hold: (∑ j, √(A(j) · c(j)))^2 ≤ (∑ j, r(j) · c(j)) · (∑ j, A(j)/…, and (∀ j, 0 < A(j)) → let(q). (((∑ j, Real.sqrt (A j * c j)) ^ 2 ≤ (∑ …)
aᵇPower: ∑ j, √(A(j) · c(j)) raised to the power 2. ((∑ j, Real.sqrt (A j * c j)) ^ 2)
RReal numbers: The real numbers: every point on the number line. (ℝ)
≤At most: 0 is less than or equal to A(j). (0 ≤ A j)
<Less than: 0 is strictly smaller than c(j). (0 < c j)
√Square root: The non-negative number whose square is A(j) · c(j). (Real.sqrt (A j * c j))
·Multiplication: A(j) times c(j). (A j * c j)
a/bDivision: A(j) divided by r(j). In Lean, dividing by 0 gives 0. (A j / r j)
(x : T)Type ascription: let(q) read as a J → ℝ. Mathematicians leave this implicit; Lean needs it to know which kind of number is meant. ((let q : J → ℝ)
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)

theorem cra-cost-aware-residual-optimal-proposal {J : Type} [Fintype J] [Nonempty J] (A c r : J → ℝ) (hA : ∀ j, 0 ≤ A j) (hc : ∀ j, 0 < c j) (hr : ∀ j, 0 < r j) (hrs : ∑ j, r j = 1) :
    ((∑ j, Real.sqrt (A j * c j)) ^ 2 ≤ (∑ j, r j * c j) * (∑ j, A j / r j)) ∧ ((∀ j, 0 < A j) → (let q : J → ℝ := fun j => Real.sqrt (A j / c j)
let rstar : J → ℝ := fun j => q j / ∑ k, q k
(∀ j, 0 < rstar j) ∧ (∑ j, rstar j = 1) ∧ ((∑ j, rstar j * c j) * (∑ j, A j / rstar j) = (∑ j, Real.sqrt (A j * c j)) ^ 2)))

For nonnegative residual energies A and positive additive access costs c, Cauchy–Schwarz proves (sum rc)(sum A/r) ≥ (sum sqrt(Ac))². When all residual energies are positive, the normalized proposal r* proportional to sqrt(A/c) attains equality. This optimizes an explicitly stated second-moment bound times additive expected access cost, not exact wall-clock time or generally the centered variance. Zero residuals are allowed in the lower bound; full-support attainment is asserted only for strictly positive energies.

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

Cost-aware residual proposal: sharp cost × second-moment lower bound and an explicit minimizer

How it was proved

More proved statements