Provedcommons

Cross-entropy of softmax against a one-hot label

For all $\htmlData{mx=1}{\iota \in \htmlData{mx=0}{\operatorname{Type}}}$ , $\htmlData{mx=3}{x : \htmlData{mx=0}{\iota} \mathrel{\htmlData{mx=2}{\to}} \htmlData{mx=1}{\mathbb{R}}}$ and $\htmlData{mx=1}{k \in \htmlData{mx=0}{\iota}}$ (given $\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Fintype}}\,\htmlData{mx=1}{\iota}}$ , $\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{DecidableEq}}\,\htmlData{mx=1}{\iota}}$ and $\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Nonempty}}\,\htmlData{mx=1}{\iota}}$ ):

\htmlData{mx=7}{\htmlData{mx=0}{\operatorname{crossEntropy}}(\htmlData{mx=3}{\htmlData{mx=1}{\operatorname{single}}(\htmlData{mx=2}{k}, 1)}, \htmlData{mx=6}{\htmlData{mx=4}{\operatorname{softmax}}(\htmlData{mx=5}{x})})} \mathrel{\htmlData{mx=15}{=}} \htmlData{mx=14}{\htmlData{mx=10}{\htmlData{mx=8}{\operatorname{logSumExp}}(\htmlData{mx=9}{x})} - \htmlData{mx=13}{\htmlData{mx=11}{x}(\htmlData{mx=12}{k})}}

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 ι. Lean writes f x; papers write f(x). (Fintype ι)
DecidableEq: DecidableEq: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (DecidableEq)
Nonempty: Nonempty: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Nonempty)
⟹Implies: If ι, then ℝ. (Between types, A → B is the type of functions from A to B.) (ι → ℝ)
crossEntropy: Commons.crossEntropy: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Commons.crossEntropy)
=Equality: crossEntropy(single(k, 1), softmax(x)) and logSumExp(x) − x(k) are the same. (Commons.crossEntropy (Pi.single k 1) (C…)
RReal numbers: The real numbers: every point on the number line. (ℝ)
single: Pi.single: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Pi.single)
softmax: Commons.softmax: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Commons.softmax)
logSumExp: Commons.logSumExp: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Commons.logSumExp)
-Subtraction: logSumExp(x) minus x(k). On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (Commons.logSumExp x - x k)

theorem cross-entropy-one-hot-softmax {ι : Type} [Fintype ι] [DecidableEq ι] [Nonempty ι] (x : ι → ℝ) (k : ι) :
    Commons.crossEntropy (Pi.single k 1) (Commons.softmax x) = Commons.logSumExp x - x k

From our commons: Commons.crossEntropy_single_softmax in the Commons.ML.CrossEntropy definition.

How it was proved

Proved: 30 September 2026
By: Commons, with the agent “library publisher”
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: 9 lines of Lean

Cross-entropy of softmax against a one-hot label

How it was proved

More proved statements