Provedcommons

Shifting the input leaves layer norm unchanged

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

\htmlData{mx=9}{\htmlData{mx=0}{\operatorname{layerNorm}}(\htmlData{mx=1}{\varepsilon}, \htmlData{mx=7}{j \mapsto \htmlData{mx=6}{\htmlData{mx=4}{\htmlData{mx=2}{x}(\htmlData{mx=3}{j})} + \htmlData{mx=5}{c}}}, \htmlData{mx=8}{i})} \mathrel{\htmlData{mx=15}{=}} \htmlData{mx=14}{\htmlData{mx=10}{\operatorname{layerNorm}}(\htmlData{mx=11}{\varepsilon}, \htmlData{mx=12}{x}, \htmlData{mx=13}{i})}

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 ι)
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)
RReal numbers: The real numbers: every point on the number line. (ℝ)
⟹Implies: If ι, then ℝ. (Between types, A → B is the type of functions from A to B.) (ι → ℝ)
layerNorm: Commons.layerNorm: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Commons.layerNorm)
=Equality: layerNorm(ε, j ↦ x(j) + c, i) and layerNorm(ε, x, i) are the same. (Commons.layerNorm ε (fun j => x j + c) …)
x ↦ f(x)Function (λ-abstraction): The function sending j to x(j) + c. Lean writes fun x => …; papers write x ↦ …. (fun j => x j + c)
+Addition: x(j) plus c. (x j + c)

theorem layer-norm-shift-invariant {ι : Type} [Fintype ι] [Nonempty ι] (ε : ℝ) (x : ι → ℝ) (c : ℝ) (i : ι) :
    Commons.layerNorm ε (fun j => x j + c) i = Commons.layerNorm ε x i

From our commons: Commons.layerNorm_add_const in the Commons.ML.LayerNorm 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

Shifting the input leaves layer norm unchanged

How it was proved

More proved statements