Provedalphabaguettebaguette-zoptimizer

Adam's moments satisfy m² ≤ C²·v with C² = (1−β₁)²/((1−β₂)(1−β₁²/β₂))

For all $\htmlData{mx=1}{t \in \htmlData{mx=0}{\mathbb{N}}}$ , $\htmlData{mx=3}{a : \htmlData{mx=0}{\mathbb{N}} \mathrel{\htmlData{mx=2}{\to}} \htmlData{mx=1}{\mathbb{R}}}$ and $\htmlData{mx=1}{\beta_{1}, \beta_{2} \in \htmlData{mx=0}{\mathbb{R}}}$ , if $0 \mathrel{\htmlData{mx=1}{<}} \htmlData{mx=0}{\beta_{2}}$ , $\htmlData{mx=0}{\beta_{2}} \mathrel{\htmlData{mx=1}{<}} 1$ and $\htmlData{mx=1}{\htmlData{mx=0}{\beta_{1}}^{2}} \mathrel{\htmlData{mx=3}{<}} \htmlData{mx=2}{\beta_{2}}$ , then

\begin{aligned} & \htmlData{mx=13}{\left(\htmlData{mx=12}{(\htmlData{mx=2}{1 - \htmlData{mx=1}{\beta_{1}}}) \cdot \htmlData{mx=11}{\sum_{k=0}^{\htmlData{mx=3}{t} - 1} \htmlData{mx=10}{\htmlData{mx=6}{\htmlData{mx=4}{\beta_{1}}^{\htmlData{mx=5}{k}}} \cdot \htmlData{mx=9}{\htmlData{mx=7}{a}(\htmlData{mx=8}{k})}}}}\right)^{2}} \\ & \quad \htmlData{mx=0}{\leq} \htmlData{mx=39}{\htmlData{mx=25}{\frac{\htmlData{mx=16}{(\htmlData{mx=15}{1 - \htmlData{mx=14}{\beta_{1}}})^{2}}}{\htmlData{mx=24}{(\htmlData{mx=18}{1 - \htmlData{mx=17}{\beta_{2}}}) \cdot \left(\htmlData{mx=23}{1 - \htmlData{mx=22}{\frac{\htmlData{mx=20}{\htmlData{mx=19}{\beta_{1}}^{2}}}{\htmlData{mx=21}{\beta_{2}}}}}\right)}}} \cdot \left(\htmlData{mx=38}{(\htmlData{mx=27}{1 - \htmlData{mx=26}{\beta_{2}}}) \cdot \htmlData{mx=37}{\sum_{k=0}^{\htmlData{mx=28}{t} - 1} \htmlData{mx=36}{\htmlData{mx=31}{\htmlData{mx=29}{\beta_{2}}^{\htmlData{mx=30}{k}}} \cdot \htmlData{mx=35}{\htmlData{mx=34}{\htmlData{mx=32}{a}(\htmlData{mx=33}{k})}^{2}}}}}\right)} \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: β₁, β₂ range over real numbers: the statement must hold for every choice. ((β₁ β₂ : ℝ))
<Less than: 0 is strictly smaller than β₂. (0 < β₂)
aᵇPower: β₁ raised to the power 2. (β₁ ^ 2)
≤At most: ((1 − β₁) · (∑ k, β₁^k · a(k)))^2 is less than or equal to (1 − β₁)^2/((1 − β₂) · (1 − β₁^2/β₂)) · ((1 − β₂) · (∑ k, …. (((1 - β₁) * ∑ k ∈ Finset.range t, β₁ ^ …)
-Subtraction: 1 minus β₁. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (1 - β₁)
RReal numbers: The real numbers: every point on the number line. (ℝ)
∑Summation: Add up β₁^k · a(k) for k = 0, 1, …, t − 1. (∑ k ∈ Finset.range t, β₁ ^ k * a k)
·Multiplication: β₁^k times a(k). (β₁ ^ k * a k)
f(x)Function application: a applied to k. Lean writes f x; papers write f(x). (a k)
a/bDivision: β₁^2 divided by β₂. In Lean, dividing by 0 gives 0. (β₁ ^ 2 / β₂)

theorem bz-adam-moment-ratio (t : ℕ) (a : ℕ → ℝ) (β₁ β₂ : ℝ) (h2 : 0 < β₂) (h2' : β₂ < 1) (h12 : β₁ ^ 2 < β₂) :
    ((1 - β₁) * ∑ k ∈ Finset.range t, β₁ ^ k * a k) ^ 2 ≤ (1 - β₁) ^ 2 / ((1 - β₂) * (1 - β₁ ^ 2 / β₂)) * ((1 - β₂) * ∑ k ∈ Finset.range t, β₂ ^ k * a k ^ 2)

For any gradient history and any window length, the first moment m = (1−β₁)Σβ₁ᵏaₖ and second moment v = (1−β₂)Σβ₂ᵏaₖ² satisfy m² ≤ C²v whenever β₁² < β₂ < 1. Part of the plan 'Baguette-Z: closed-loop certified integer-state training'.

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

Adam's moments satisfy m² ≤ C²·v with C² = (1−β₁)²/((1−β₂)(1−β₁²/β₂))

How it was proved

More proved statements