Provedunbiased-gradientstrainingfirst-principles

Randomised objective: for samples drawn from a θ-independent proposal, the derivative of the expected loss equals the expected pathwise derivative

For all $\htmlData{mx=1}{J \in \htmlData{mx=0}{\operatorname{Type}}}$ , $\htmlData{mx=3}{r : \htmlData{mx=0}{J} \mathrel{\htmlData{mx=2}{\to}} \htmlData{mx=1}{\mathbb{R}}}$ , $\htmlData{mx=5}{f : \htmlData{mx=0}{J} \mathrel{\htmlData{mx=4}{\to}} \htmlData{mx=1}{\mathbb{R}} \mathrel{\htmlData{mx=3}{\to}} \htmlData{mx=2}{\mathbb{R}}}$ , $\htmlData{mx=3}{f' : \htmlData{mx=0}{J} \mathrel{\htmlData{mx=2}{\to}} \htmlData{mx=1}{\mathbb{R}}}$ , $\htmlData{mx=1}{\theta \in \htmlData{mx=0}{\mathbb{R}}}$ and $\htmlData{mx=12}{\mathit{hd} : \htmlData{mx=11}{\forall j,\ \htmlData{mx=10}{\htmlData{mx=0}{\operatorname{HasDerivAt}}\,\htmlData{mx=5}{t \mapsto \htmlData{mx=4}{\htmlData{mx=1}{f}(\htmlData{mx=2}{j}, \htmlData{mx=3}{t})}}\,\htmlData{mx=8}{\htmlData{mx=6}{f'}(\htmlData{mx=7}{j})}\,\htmlData{mx=9}{\theta}}}}$ (given $\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Fintype}}\,\htmlData{mx=1}{J}}$ ):

\htmlData{mx=20}{\htmlData{mx=0}{\operatorname{HasDerivAt}}\,\htmlData{mx=10}{t \mapsto \htmlData{mx=9}{\sum_{j} \htmlData{mx=8}{\htmlData{mx=3}{\htmlData{mx=1}{r}(\htmlData{mx=2}{j})} \cdot \htmlData{mx=7}{\htmlData{mx=4}{f}(\htmlData{mx=5}{j}, \htmlData{mx=6}{t})}}}}\,\htmlData{mx=18}{\sum_{j} \htmlData{mx=17}{\htmlData{mx=13}{\htmlData{mx=11}{r}(\htmlData{mx=12}{j})} \cdot \htmlData{mx=16}{\htmlData{mx=14}{f'}(\htmlData{mx=15}{j})}}}\,\htmlData{mx=19}{\theta}}

What the notation means · or point at any symbol

Type: Type: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Type)
Fintype: Fintype: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Fintype)
f(x)Function application: Fintype applied to J. Lean writes f x; papers write f(x). (Fintype J)
⟹Implies: If J, then ℝ. (Between types, A → B is the type of functions from A to B.) (J → ℝ)
∀For all: The statement after the comma holds for every j. (∀ j, HasDerivAt (fun t => f j t) (f' j)…)
RReal numbers: The real numbers: every point on the number line. (ℝ)
HasDerivAt: HasDerivAt: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (HasDerivAt)
x ↦ f(x)Function (λ-abstraction): The function sending t to f(j, t). Lean writes fun x => …; papers write x ↦ …. (fun t => f j t)
∑Summation: Add up r(j) · f(j, t) for every j. (∑ j, r j * f j t)
·Multiplication: r(j) times f(j, t). (r j * f j t)

theorem ug-pathwise-gradient-fixed-proposal {J : Type} [Fintype J] (r : J → ℝ) (f : J → ℝ → ℝ) (f' : J → ℝ) (θ : ℝ) (hd : ∀ j, HasDerivAt (fun t => f j t) (f' j) θ) :
    HasDerivAt (fun t => ∑ j, r j * f j t) (∑ j, r j * f' j) θ

The other half of the gradient contract. If the proposal does not depend on the parameters, d/dθ E_{J∼r}[f_θ(J)] = E_{J∼r}[d/dθ f_θ(J)], so ordinary backpropagation through the sampled network is exactly unbiased for the gradient of the randomised network's expected loss. That objective, not the dense one, is the natural target when inference also samples. Proposals that depend on θ need the score-function term (the covariance form of the attention gradient). 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: 13 lines of Lean

Randomised objective: for samples drawn from a θ-independent proposal, the derivative of the expected loss equals the expected pathwise derivative

How it was proved

More proved statements