Provedalphabaguettebaguette-zoptimizer

Σ_{k<t} rᵏ ≤ 1/(1−r) for 0 ≤ r < 1

For all $\htmlData{mx=1}{r \in \htmlData{mx=0}{\mathbb{R}}}$ and $\htmlData{mx=1}{t \in \htmlData{mx=0}{\mathbb{N}}}$ , if $0 \mathrel{\htmlData{mx=1}{\leq}} \htmlData{mx=0}{r}$ and $\htmlData{mx=0}{r} \mathrel{\htmlData{mx=1}{<}} 1$ , then

\htmlData{mx=4}{\sum_{k=0}^{\htmlData{mx=0}{t} - 1} \htmlData{mx=3}{\htmlData{mx=1}{r}^{\htmlData{mx=2}{k}}}} \mathrel{\htmlData{mx=8}{\leq}} \htmlData{mx=7}{\frac{1}{\htmlData{mx=6}{1 - \htmlData{mx=5}{r}}}}

What the notation means · or point at any symbol

RReal numbers: The real numbers: every point on the number line. (ℝ)
≤At most: 0 is less than or equal to r. (0 ≤ r)
<Less than: r is strictly smaller than 1. (r < 1)
NNatural numbers: The natural numbers 0, 1, 2, …. In Lean they start at 0. (ℕ)
∑Summation: Add up r^k for k = 0, 1, …, t − 1. (∑ k ∈ Finset.range t, r ^ k)
aᵇPower: r raised to the power k. (r ^ k)
a/bDivision: 1 divided by 1 − r. In Lean, dividing by 0 gives 0. (1 / (1 - r))
-Subtraction: 1 minus r. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (1 - r)

theorem bz-geometric-sum-bound (r : ℝ) (h0 : 0 ≤ r) (h1 : r < 1) (t : ℕ) :
    ∑ k ∈ Finset.range t, r ^ k ≤ 1 / (1 - r)

Bounds the weighted Cauchy–Schwarz factor uniformly in the window length t. 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: 18 lines of Lean

Σ_{k<t} rᵏ ≤ 1/(1−r) for 0 ≤ r < 1

How it was proved

More proved statements