Provedalphabaguettebaguette-zoptimizer
Weighted Cauchy–Schwarz: (Σβ₁ᵏaₖ)² ≤ (Σ(β₁²/β₂)ᵏ)(Σβ₂ᵏaₖ²)
For all , and , if , then
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 < β₂) - ≤At most
- (∑ k, β₁^k · a(k))^2 is less than or equal to (∑ k, (β₁^2/β₂)^k) · (∑ k, β₂^k · a(k)^2). (
(∑ k ∈ Finset.range t, β₁ ^ k * a k) ^ …) - ∑Summation
- Add up β₁^k · a(k) for k = 0, 1, …, t − 1. (
∑ k ∈ Finset.range t, β₁ ^ k * a k) - RReal numbers
- The real numbers: every point on the number line. (
ℝ) - aᵇPower
- β₁ raised to the power k. (
β₁ ^ 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-weighted-cauchy-schwarz (t : ℕ) (a : ℕ → ℝ) (β₁ β₂ : ℝ) (h2 : 0 < β₂) :
(∑ k ∈ Finset.range t, β₁ ^ k * a k) ^ 2 ≤ (∑ k ∈ Finset.range t, (β₁ ^ 2 / β₂) ^ k) * (∑ k ∈ Finset.range t, β₂ ^ k * a k ^ 2)The core inequality relating Adam's first moment to its second moment over any window of t past gradients. 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
- 31 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.