Proveddrift-lawdecodeinnovationreview-response
Innovation variance arithmetic: 2e^{2Δ}·(F(1−e^{−Δ}))² = 2F²(e^Δ − 1)²
For all :
What the notation means · or point at any symbol
- RReal numbers
- The real numbers: every point on the number line. (
ℝ) - x ∈ TVariables
- F, Δ range over real numbers: the statement must hold for every choice. (
(F Δ : ℝ)) - =Equality
- 2 · exp(2 · Δ) · (F · (1 − exp(−Δ)))^2 and 2 · F^2 · (exp(Δ) − 1)^2 are the same. (
2 * Real.exp (2 * Δ) * (F * (1 - Real.e…) - eˣExponential function
- e raised to the power 2 · Δ, where e ≈ 2.718. (
Real.exp (2 * Δ)) - ·Multiplication
- 2 times Δ. (
2 * Δ) - aᵇPower
- F · (1 − exp(−Δ)) raised to the power 2. (
(F * (1 - Real.exp (-Δ))) ^ 2) - -Subtraction
- 1 minus exp(−Δ). On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (
1 - Real.exp (-Δ)) - −xNegation
- The negative of Δ. (
-Δ)
theorem innov-variance-arith (F Δ : ℝ) :
2 * Real.exp (2 * Δ) * (F * (1 - Real.exp (-Δ))) ^ 2 = 2 * F ^ 2 * (Real.exp Δ - 1) ^ 2Combines the reward bound F(1 − a_min) with a_min = e^{−Δ} and the second moment E[T²] ≤ 2e^{2Δ} of the geometric stopping time into the variance bound 2F²(e^Δ − 1)² of the innovation estimator, which vanishes quadratically in the drift oscillation. 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
- 16 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.