Provedalphabaguettebaguette-zv2

AdamW weights are an exponential moving average of updates (closed form)

For all $\htmlData{mx=3}{\theta, u : \htmlData{mx=0}{\mathbb{N}} \mathrel{\htmlData{mx=2}{\to}} \htmlData{mx=1}{\mathbb{R}}}$ and $\htmlData{mx=1}{a, \eta \in \htmlData{mx=0}{\mathbb{R}}}$ , if $\htmlData{mx=17}{\forall t,\ \htmlData{mx=3}{\htmlData{mx=0}{\theta}(\htmlData{mx=2}{\htmlData{mx=1}{t} + 1})} \mathrel{\htmlData{mx=16}{=}} \htmlData{mx=15}{\htmlData{mx=9}{(\htmlData{mx=5}{1 - \htmlData{mx=4}{a}}) \cdot \htmlData{mx=8}{\htmlData{mx=6}{\theta}(\htmlData{mx=7}{t})}} - \htmlData{mx=14}{\htmlData{mx=10}{\eta} \cdot \htmlData{mx=13}{\htmlData{mx=11}{u}(\htmlData{mx=12}{t})}}}}$ , then

\begin{aligned} & \htmlData{mx=0}{\forall} t, \\ & \quad \htmlData{mx=4}{\htmlData{mx=2}{\theta}(\htmlData{mx=3}{t})} \\ & \quad \quad \htmlData{mx=1}{=} \htmlData{mx=27}{\htmlData{mx=11}{\htmlData{mx=8}{(\htmlData{mx=6}{1 - \htmlData{mx=5}{a}})^{\htmlData{mx=7}{t}}} \cdot \htmlData{mx=10}{\htmlData{mx=9}{\theta}(0)}} - \htmlData{mx=26}{\htmlData{mx=12}{\eta} \cdot \htmlData{mx=25}{\sum_{s=0}^{\htmlData{mx=13}{t} - 1} \htmlData{mx=24}{\htmlData{mx=20}{(\htmlData{mx=15}{1 - \htmlData{mx=14}{a}})^{\htmlData{mx=19}{\htmlData{mx=17}{\htmlData{mx=16}{t} - 1} - \htmlData{mx=18}{s}}}} \cdot \htmlData{mx=23}{\htmlData{mx=21}{u}(\htmlData{mx=22}{s})}}}}} \end{aligned}

What the notation means · or point at any symbol

NNatural numbers: The natural numbers 0, 1, 2, …. In Lean they start at 0. (ℕ)
⟹Implies: If ℕ, then ℝ. (Between types, A → B is the type of functions from A to B.) (ℕ → ℝ)
x : TVariables: θ, u range over ℕ → ℝ: the statement must hold for every choice. ((θ u : ℕ → ℝ))
x ∈ TVariables: a, η range over real numbers: the statement must hold for every choice. ((a η : ℝ))
∀For all: The statement after the comma holds for every t. (∀ t, θ (t + 1) = (1 - a) * θ t - η * u t)
RReal numbers: The real numbers: every point on the number line. (ℝ)
f(x)Function application: θ applied to t + 1. Lean writes f x; papers write f(x). (θ (t + 1))
=Equality: θ(t + 1) and (1 − a) · θ(t) − η · u(t) are the same. (θ (t + 1) = (1 - a) * θ t - η * u t)
+Addition: t plus 1. (t + 1)
aᵇPower: 1 − a raised to the power t. ((1 - a) ^ t)
·Multiplication: 1 − a times θ(t). ((1 - a) * θ t)
-Subtraction: 1 minus a. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (1 - a)
∑Summation: Add up (1 − a)^(t − 1 − s) · u(s) for s = 0, 1, …, t − 1. (∑ s ∈ Finset.range t, (1 - a) ^ (t - 1 …)

theorem bz2-adamw-ema-closed-form (θ u : ℕ → ℝ) (a η : ℝ) (hθ : ∀ t, θ (t + 1) = (1 - a) * θ t - η * u t) :
    ∀ t, θ t = (1 - a) ^ t * θ 0 - η * ∑ s ∈ Finset.range t, (1 - a) ^ (t - 1 - s) * u s

θ(t) = (1−a)ᵗθ(0) − η·Σ_{s<t}(1−a)^(t−1−s)·u(s). This is the formal statement of the EMA view of AdamW (timescale 1/a = 1/(ηλ); Wang & Aitchison, ICML 2025), from which the box is immediate. We claim no novelty for the box. Part of 'Baguette-Z v2' (revision after the hostile review).

How it was proved

Proved: 3 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: 29 lines of Lean

AdamW weights are an exponential moving average of updates (closed form)

How it was proved

More proved statements