Bounds for LayerNorm derivatives

Positive epsilon gives a lower bound sqrt ε for every row's standard deviation. We use it to bound the actual row differential, retaining the contribution from the changing variance. The variance contribution contains three factors of 1 / sqrt ε; replacing their product by 1 / ε would lose the bound when epsilon is smaller than one.

The hypotheses below bound the centered input and the input direction coordinatewise. They make no assumption about the derivative being bounded. The final theorem also includes the scale and bias directions, using the Fréchet derivative of the actual LayerNorm specification.

theorem Proofs.Autograd.RowNorm.invStd_nonneg {m n : ℕ} (X : Vec (TapeNodes.Matmul.matSize m n)) (ε : ℝ) (i : Fin m) : 0 ≤ invStd X ε i

The inverse standard deviation is nonnegative.

theorem Proofs.Autograd.RowNorm.invStd_le_inv_sqrt {m n : ℕ} {ε : ℝ} (hε : 0 < ε) (X : Vec (TapeNodes.Matmul.matSize m n)) (i : Fin m) : invStd X ε i ≤ (√ε)⁻¹

Epsilon alone bounds the inverse standard deviation, including for constant rows.

theorem Proofs.Autograd.RowNorm.abs_rowMean_le {m n : ℕ} (X : Vec (TapeNodes.Matmul.matSize m n)) (i : Fin m) (bounds : Fin n → ℝ) (hbounds : ∀ (j : Fin n), |X.ofLp (TapeNodes.Matmul.idxMN i j)| ≤ bounds j) : |rowMean X i| ≤ (∑ j : Fin n, bounds j) / ↑n

Coordinate bounds on a row give a bound on the absolute value of its mean.

theorem Proofs.Autograd.RowNorm.abs_nrm_le {m n : ℕ} {ε : ℝ} (hε : 0 < ε) (X : Vec (TapeNodes.Matmul.matSize m n)) (i : Fin m) (j : Fin n) {bound : ℝ} (hbound : |centered X i j| ≤ bound) : |nrm X ε i j| ≤ bound * (√ε)⁻¹

A centered-input bound gives a normalized-input bound without a variance lower estimate.

noncomputable def Proofs.Autograd.RowNorm.derivativeRadius {n : ℕ} (ε : ℝ) (u d : Fin n → ℝ) (j : Fin n) : ℝ

Radius obtained from centered-input bounds u and input-direction bounds d.

The first two terms bound the direction and its row mean. The third bounds the projection along the normalized input. All sums are over this row's feature axis.

theorem Proofs.Autograd.RowNorm.abs_nrmJvp_le {m n : ℕ} {ε : ℝ} (hε : 0 < ε) (X dX : Vec (TapeNodes.Matmul.matSize m n)) (i : Fin m) (u d : Fin n → ℝ) (hu : ∀ (k : Fin n), |centered X i k| ≤ u k) (hd : ∀ (k : Fin n), |dX.ofLp (TapeNodes.Matmul.idxMN i k)| ≤ d k) (j : Fin n) : |nrmJvp X ε dX i j| ≤ derivativeRadius ε u d j

The row differential is bounded by the centered-input and direction intervals.

theorem Proofs.Autograd.LayerNorm.abs_fderiv_specLayerNormVec_le {m n : ℕ} (hm : 0 < m) (hn : 0 < n) {ε : ℝ} (hε : 0 < ε) (q dq : CtxVec (ΓLN m n)) (i : Fin m) (j : Fin n) (u d : Fin n → ℝ) (hu : ∀ (k : Fin n), |RowNorm.centered (valX q) i k| ≤ u k) (hd : ∀ (k : Fin n), |(valX dq).ofLp (TapeNodes.Matmul.idxMN i k)| ≤ d k) : |((fderiv ℝ (specLayerNormVec hm hn ε) q) dq).ofLp (TapeNodes.Matmul.idxMN i j)| ≤ RowNorm.derivativeRadius ε u d j * |(valGamma q).ofLp j| + u j * (√ε)⁻¹ * |(valGamma dq).ofLp j| + |(valBeta dq).ofLp j|

Coordinate bound for the full LayerNorm derivative, including both affine parameter directions.

The scale multiplies the normalized-input differential. Its own direction contributes the normalized input times dgamma, and the bias direction contributes directly. Gamma and beta remain arbitrary exact parameters throughout.