Provedunbiased-gradientstrainingfirst-principles

Depth variance price: if e_0 = 0 and e_{d+1} ≤ 2σ + 2Λ e_d, then e_D ≤ 2σ·Σ_{k<D}(2Λ)^k, so the whole-network level constant is exponential in depth when 2Λ > 1

For all $\htmlData{mx=3}{e : \htmlData{mx=0}{\mathbb{N}} \mathrel{\htmlData{mx=2}{\to}} \htmlData{mx=1}{\mathbb{R}}}$ and $\htmlData{mx=1}{\sigma, \Lambda \in \htmlData{mx=0}{\mathbb{R}}}$ , if $0 \mathrel{\htmlData{mx=1}{\leq}} \htmlData{mx=0}{\sigma}$ , $0 \mathrel{\htmlData{mx=1}{\leq}} \htmlData{mx=0}{\Lambda}$ , $\htmlData{mx=1}{\htmlData{mx=0}{e}(0)} \mathrel{\htmlData{mx=2}{=}} 0$ and $\htmlData{mx=14}{\forall d,\ \htmlData{mx=3}{\htmlData{mx=0}{e}(\htmlData{mx=2}{\htmlData{mx=1}{d} + 1})} \mathrel{\htmlData{mx=13}{\leq}} \htmlData{mx=12}{\htmlData{mx=5}{2\htmlData{mx=4}{\sigma}} + \htmlData{mx=11}{\htmlData{mx=7}{2\htmlData{mx=6}{\Lambda}} \cdot \htmlData{mx=10}{\htmlData{mx=8}{e}(\htmlData{mx=9}{d})}}}}$ , then

\htmlData{mx=13}{\forall D,\ \htmlData{mx=2}{\htmlData{mx=0}{e}(\htmlData{mx=1}{D})} \mathrel{\htmlData{mx=12}{\leq}} \htmlData{mx=11}{\htmlData{mx=4}{2\htmlData{mx=3}{\sigma}} \cdot \htmlData{mx=10}{\sum_{k=0}^{\htmlData{mx=5}{D} - 1} \htmlData{mx=9}{(\htmlData{mx=7}{2\htmlData{mx=6}{\Lambda}})^{\htmlData{mx=8}{k}}}}}}

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. ((σ Λ : ℝ))
≤At most: 0 is less than or equal to σ. (0 ≤ σ)
f(x)Function application: e applied to 0. Lean writes f x; papers write f(x). (e 0)
=Equality: e(0) and 0 are the same. (e 0 = 0)
∀For all: The statement after the comma holds for every d. (∀ d, e (d + 1) ≤ 2 * σ + 2 * Λ * e d)
RReal numbers: The real numbers: every point on the number line. (ℝ)
+Addition: d plus 1. (d + 1)
·Multiplication: 2 times σ. (2 * σ)
∑Summation: Add up (2 · Λ)^k for k = 0, 1, …, D − 1. (∑ k ∈ Finset.range D, (2 * Λ) ^ k)
aᵇPower: 2 · Λ raised to the power k. ((2 * Λ) ^ k)

theorem ua-depth-variance-price (e : ℕ → ℝ) (σ Λ : ℝ) (hσ : 0 ≤ σ) (hΛ : 0 ≤ Λ) (h0 : e 0 = 0) (hrec : ∀ d, e (d + 1) ≤ 2 * σ + 2 * Λ * e d) :
    ∀ D, e D ≤ 2 * σ * ∑ k ∈ Finset.range D, (2 * Λ) ^ k

Closed form of the induction behind the Lipschitz finite-terminal MLMC training theorem: iterating the level-error propagation inequality (own sampling error σ per stage, Lipschitz constant squared ≤ Λ) over D stages gives e_D ≤ 2σ(1 + 2Λ + … + (2Λ)^{D−1}). This is the honest variance price of exactly unbiased dense-objective gradients: linear in depth when 2Λ ≤ 1, exponential otherwise. First-principles reformulation, 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: 23 lines of Lean

Depth variance price: if e_0 = 0 and e_{d+1} ≤ 2σ + 2Λ e_d, then e_D ≤ 2σ·Σ_{k<D}(2Λ)^k, so the whole-network level constant is exponential in depth when 2Λ > 1

How it was proved

More proved statements