Proveddrift-lawdecodeinnovationreview-response
Stopped-sum unbiasedness, geometric step: Σ'_{i≥0} (1−p)^i·(p·c) = c for 0 < p ≤ 1
For all , if and , then
What the notation means · or point at any symbol
- RReal numbers
- The real numbers: every point on the number line. (
ℝ) - x ∈ TVariables
- p, c range over real numbers: the statement must hold for every choice. (
(p c : ℝ)) - <Less than
- 0 is strictly smaller than p. (
0 < p) - ≤At most
- p is less than or equal to 1. (
p ≤ 1) - ∑'Infinite sum
- Add up (1 − p)^i · (p · c) for every i in ℕ. (
∑' i : ℕ, (1 - p) ^ i * (p * c)) - =Equality
- ∑' i, (1 − p)^i · (p · c) and c are the same. (
∑' i : ℕ, (1 - p) ^ i * (p * c) = c) - NNatural numbers
- The natural numbers 0, 1, 2, …. In Lean they start at 0. (
ℕ) - aᵇPower
- 1 − p raised to the power i. (
(1 - p) ^ i) - -Subtraction
- 1 minus p. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (
1 - p) - ·Multiplication
- p times c. (
p * c)
theorem innov-geometric-unbiased (p c : ℝ) (hp0 : 0 < p) (hp1 : p ≤ 1) :
∑' i : ℕ, (1 - p) ^ i * (p * c) = cThe series step of the innovation estimator's unbiasedness: trial i contributes with probability (1−p)^{i−1} (not yet accepted) and has reward mean p(o − m), so the expected total is (o − m). Suggested by an external reviewer (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
- 17 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.