proofs
Proveddrift-lawdecodevariational-cost-lawfirst-principles

Bayes-optimal snapshot proposal: under a drift prior, the least expected second moment for the numerator is (Σ_j e^{s_j}√E[e^{2δ_j}])², attained by r_j ∝ e^{s_j}√E[e^{2δ_j}]

For all Ω,J∈Type⁡\htmlData{mx=1}{\Omega, J \in \htmlData{mx=0}{\operatorname{Type}}}, lam:Ω→R\htmlData{mx=3}{\mathit{lam} : \htmlData{mx=0}{\Omega} \mathrel{\htmlData{mx=2}{\to}} \htmlData{mx=1}{\mathbb{R}}}, s:J→R\htmlData{mx=3}{s : \htmlData{mx=0}{J} \mathrel{\htmlData{mx=2}{\to}} \htmlData{mx=1}{\mathbb{R}}}, δ:Ω→J→R\htmlData{mx=5}{\delta : \htmlData{mx=0}{\Omega} \mathrel{\htmlData{mx=4}{\to}} \htmlData{mx=1}{J} \mathrel{\htmlData{mx=3}{\to}} \htmlData{mx=2}{\mathbb{R}}} and r:J→R\htmlData{mx=3}{r : \htmlData{mx=0}{J} \mathrel{\htmlData{mx=2}{\to}} \htmlData{mx=1}{\mathbb{R}}}, if ∀ω, 0≤lam(ω)\htmlData{mx=4}{\forall \omega,\ 0 \mathrel{\htmlData{mx=3}{\leq}} \htmlData{mx=2}{\htmlData{mx=0}{\mathit{lam}}(\htmlData{mx=1}{\omega})}}, ∑ωlam(ω)=1\htmlData{mx=3}{\sum_{\omega} \htmlData{mx=2}{\htmlData{mx=0}{\mathit{lam}}(\htmlData{mx=1}{\omega})}} \mathrel{\htmlData{mx=4}{=}} 1, ∀j, 0<r(j)\htmlData{mx=4}{\forall j,\ 0 \mathrel{\htmlData{mx=3}{<}} \htmlData{mx=2}{\htmlData{mx=0}{r}(\htmlData{mx=1}{j})}} and ∑jr(j)=1\htmlData{mx=3}{\sum_{j} \htmlData{mx=2}{\htmlData{mx=0}{r}(\htmlData{mx=1}{j})}} \mathrel{\htmlData{mx=4}{=}} 1 (given Fintype⁡ Ω\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Fintype}}\,\htmlData{mx=1}{\Omega}}, Fintype⁡ J\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Fintype}}\,\htmlData{mx=1}{J}} and Nonempty⁡ J\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Nonempty}}\,\htmlData{mx=1}{J}}), then

(∑jes(j)⋅∑ωlam(ω)⋅e2δ(ω,j))2≤∑ωlam(ω)⋅∑jes(j)+δ(ω,j)2r(j)∧∑ωlam(ω)⋅∑jes(j)+δ(ω,j)2es(j)⋅∑ω′lam(ω′)⋅e2δ(ω′,j)∑ies(i)⋅∑ω′lam(ω′)⋅e2δ(ω′,i)=(∑jes(j)⋅∑ωlam(ω)⋅e2δ(ω,j))2\begin{aligned} & \htmlData{mx=20}{\left(\htmlData{mx=19}{\sum_{j} \htmlData{mx=18}{\htmlData{mx=5}{e^{\htmlData{mx=4}{\htmlData{mx=2}{s}(\htmlData{mx=3}{j})}}} \cdot \htmlData{mx=17}{\sqrt{\htmlData{mx=16}{\sum_{\omega} \htmlData{mx=15}{\htmlData{mx=8}{\htmlData{mx=6}{\mathit{lam}}(\htmlData{mx=7}{\omega})} \cdot \htmlData{mx=14}{e^{\htmlData{mx=13}{2\htmlData{mx=12}{\htmlData{mx=9}{\delta}(\htmlData{mx=10}{\omega}, \htmlData{mx=11}{j})}}}}}}}}}}\right)^{2}} \\ & \quad \htmlData{mx=1}{\leq} \htmlData{mx=40}{\sum_{\omega} \htmlData{mx=39}{\htmlData{mx=23}{\htmlData{mx=21}{\mathit{lam}}(\htmlData{mx=22}{\omega})} \cdot \htmlData{mx=38}{\sum_{j} \htmlData{mx=37}{\frac{\htmlData{mx=33}{\htmlData{mx=32}{e^{\htmlData{mx=31}{\htmlData{mx=26}{\htmlData{mx=24}{s}(\htmlData{mx=25}{j})} + \htmlData{mx=30}{\htmlData{mx=27}{\delta}(\htmlData{mx=28}{\omega}, \htmlData{mx=29}{j})}}}}^{2}}}{\htmlData{mx=36}{\htmlData{mx=34}{r}(\htmlData{mx=35}{j})}}}}}} \\ & \htmlData{mx=0}{\land} \htmlData{mx=94}{\sum_{\omega} \htmlData{mx=93}{\htmlData{mx=44}{\htmlData{mx=42}{\mathit{lam}}(\htmlData{mx=43}{\omega})} \cdot \htmlData{mx=92}{\sum_{j} \htmlData{mx=91}{\frac{\htmlData{mx=54}{\htmlData{mx=53}{e^{\htmlData{mx=52}{\htmlData{mx=47}{\htmlData{mx=45}{s}(\htmlData{mx=46}{j})} + \htmlData{mx=51}{\htmlData{mx=48}{\delta}(\htmlData{mx=49}{\omega}, \htmlData{mx=50}{j})}}}}^{2}}}{\htmlData{mx=90}{\frac{\htmlData{mx=71}{\htmlData{mx=58}{e^{\htmlData{mx=57}{\htmlData{mx=55}{s}(\htmlData{mx=56}{j})}}} \cdot \htmlData{mx=70}{\sqrt{\htmlData{mx=69}{\sum_{\omega'} \htmlData{mx=68}{\htmlData{mx=61}{\htmlData{mx=59}{\mathit{lam}}(\htmlData{mx=60}{\omega'})} \cdot \htmlData{mx=67}{e^{\htmlData{mx=66}{2\htmlData{mx=65}{\htmlData{mx=62}{\delta}(\htmlData{mx=63}{\omega'}, \htmlData{mx=64}{j})}}}}}}}}}}{\htmlData{mx=89}{\sum_{i} \htmlData{mx=88}{\htmlData{mx=75}{e^{\htmlData{mx=74}{\htmlData{mx=72}{s}(\htmlData{mx=73}{i})}}} \cdot \htmlData{mx=87}{\sqrt{\htmlData{mx=86}{\sum_{\omega'} \htmlData{mx=85}{\htmlData{mx=78}{\htmlData{mx=76}{\mathit{lam}}(\htmlData{mx=77}{\omega'})} \cdot \htmlData{mx=84}{e^{\htmlData{mx=83}{2\htmlData{mx=82}{\htmlData{mx=79}{\delta}(\htmlData{mx=80}{\omega'}, \htmlData{mx=81}{i})}}}}}}}}}}}}}}}}} \\ & \quad \htmlData{mx=41}{=} \htmlData{mx=113}{\left(\htmlData{mx=112}{\sum_{j} \htmlData{mx=111}{\htmlData{mx=98}{e^{\htmlData{mx=97}{\htmlData{mx=95}{s}(\htmlData{mx=96}{j})}}} \cdot \htmlData{mx=110}{\sqrt{\htmlData{mx=109}{\sum_{\omega} \htmlData{mx=108}{\htmlData{mx=101}{\htmlData{mx=99}{\mathit{lam}}(\htmlData{mx=100}{\omega})} \cdot \htmlData{mx=107}{e^{\htmlData{mx=106}{2\htmlData{mx=105}{\htmlData{mx=102}{\delta}(\htmlData{mx=103}{\omega}, \htmlData{mx=104}{j})}}}}}}}}}}\right)^{2}} \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
Ω, J range over Type: the statement must hold for every choice. ((Ω J : 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 Ω)
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 Ω, 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 ≤ lam ω)
∑Summation
Add up lam(ω) for every ω. (∑ ω, lam ω)
=Equality
∑ ω, lam(ω) and 1 are the same. (∑ ω, lam ω = 1)
aᵇPower
∑ j, exp(s(j)) · √(∑ ω, lam(ω) · exp(2 · δ(ω, j))) raised to the power 2. ((∑ j, Real.exp (s j) * Real.sqrt (∑ ω, …)
∧And
Both hold: (∑ j, exp(s(j)) · √(∑ ω, lam(ω) · exp(2 · δ(ω, j))))^2 ≤ (…, and (∑ ω, lam(ω) · (∑ j, exp(s(j) + δ(ω, j))^2/(exp(s(j)) · √(…. ((∑ j, Real.exp (s j) * Real.sqrt (∑ ω, …)
RReal numbers
The real numbers: every point on the number line. (ℝ)
≤At most
0 is less than or equal to lam(ω). (0 ≤ lam ω)
<Less than
0 is strictly smaller than r(j). (0 < r j)
eˣExponential function
e raised to the power s(j), where e ≈ 2.718. (Real.exp (s j))
√Square root
The non-negative number whose square is ∑ ω, lam(ω) · exp(2 · δ(ω, j)). (Real.sqrt (∑ ω, lam ω * Real.exp (2 * δ…)
·Multiplication
2 times δ(ω, j). (2 * δ ω j)
a/bDivision
exp(s(j) + δ(ω, j))^2 divided by r(j). In Lean, dividing by 0 gives 0. (Real.exp (s j + δ ω j) ^ 2 / r j)
+Addition
s(j) plus δ(ω, j). (s j + δ ω j)

Instance of the variational cost law with the mixture over drift outcomes ω (weights λ_ω) and unnormalised current weights e^{s_j + δ_ωj}. The optimal proposal is not the stale row itself but the stale row reweighted by the square root of each key's drift moment E[e^{2δ_j}]. For drift δ_j = d·k_j with random d, this moment grows with the key norm, which is the first-principles reason to treat high-norm keys specially (norm tiering). 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
72 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.

More proved statements