Mixed LayerNorm derivatives

We differentiate the actual row differential, allowing both the input and its left direction to vary. The latter variation supplies the upstream mixed derivative in the chain rule. Centered input and direction bounds then enclose the result using only positive epsilon. The affine scale is fixed; its absolute value multiplies the final radius.

noncomputable def Proofs.Autograd.RowNorm.varianceFirst {m n : ℕ} (X A : Vec (TapeNodes.Matmul.matSize m n)) (i : Fin m) : ℝ

Variance differential written entirely in centered coordinates.

noncomputable def Proofs.Autograd.RowNorm.varianceMixed {m n : ℕ} (X A B C : Vec (TapeNodes.Matmul.matSize m n)) (i : Fin m) : ℝ

Mixed variance differential, including the upstream mixed direction C.

noncomputable def Proofs.Autograd.RowNorm.inverseFirst {m n : ℕ} (X A : Vec (TapeNodes.Matmul.matSize m n)) (ε : ℝ) (i : Fin m) : ℝ

Inverse-standard-deviation differential in centered coordinates.

noncomputable def Proofs.Autograd.RowNorm.inverseMixed {m n : ℕ} (X A B C : Vec (TapeNodes.Matmul.matSize m n)) (ε : ℝ) (i : Fin m) : ℝ

Mixed inverse-standard-deviation differential.

noncomputable def Proofs.Autograd.RowNorm.normalizedMixed {m n : ℕ} (X A B C : Vec (TapeNodes.Matmul.matSize m n)) (ε : ℝ) (i : Fin m) (j : Fin n) : ℝ

The mixed row chain rule: the Hessian term and the input's mixed differential.

theorem Proofs.Autograd.RowNorm.varD_apply_centered {m n : ℕ} (X A : Vec (TapeNodes.Matmul.matSize m n)) (i : Fin m) : (varD X i) A = varianceFirst X A i

The variance differential, written in centered coordinates.

theorem Proofs.Autograd.RowNorm.invD_apply_centered {m n : ℕ} {ε : ℝ} (hε : 0 < ε) (X A : Vec (TapeNodes.Matmul.matSize m n)) (i : Fin m) : (invD X ε i) A = inverseFirst X A ε i

The inverse-standard-deviation differential, written in centered coordinates.

theorem Proofs.Autograd.RowNorm.nrmD_apply_centered {m n : ℕ} {ε : ℝ} (hε : 0 < ε) (X A : Vec (TapeNodes.Matmul.matSize m n)) (i : Fin m) (j : Fin n) : (nrmD X ε i j) A = centered A i j * invStd X ε i + centered X i j * inverseFirst X A ε i

The existing Fréchet differential agrees with the centered product-rule formula.

theorem Proofs.Autograd.RowNorm.fderiv_nrmD_comp {m n : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {ε : ℝ} (hε : 0 < ε) (X A : E → Vec (TapeNodes.Matmul.matSize m n)) (p : E) (DX DA : E →L[ℝ] Vec (TapeNodes.Matmul.matSize m n)) (hX : HasFDerivAt X DX p) (hA : HasFDerivAt A DA p) (i : Fin m) (j : Fin n) (v : E) : (fderiv ℝ (fun (q : E) => (nrmD (X q) ε i j) (A q)) p) v = normalizedMixed (X p) (A p) (DX v) (DA v) ε i j

Differentiating the actual row differential gives the full mixed chain formula.

theorem Proofs.Autograd.RowNorm.fderiv_fderiv_nrm {m n : ℕ} {ε : ℝ} (hε : 0 < ε) (X A B : Vec (TapeNodes.Matmul.matSize m n)) (i : Fin m) (j : Fin n) : (fderiv ℝ (fun (Y : Vec (TapeNodes.Matmul.matSize m n)) => (fderiv ℝ (fun (Z : Vec (TapeNodes.Matmul.matSize m n)) => nrm Z ε i j) Y) A) X) B = normalizedMixed X A B 0 ε i j

The Hessian of a normalized row entry is the mixed formula with zero upstream term.

theorem Proofs.Autograd.RowNorm.fderiv_fderiv_affine_nrm_comp {m n : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {ε : ℝ} (hε : 0 < ε) (X : E → Vec (TapeNodes.Matmul.matSize m n)) (p left right : E) (hX : ∀ (q : E), DifferentiableAt ℝ X q) (DA : E →L[ℝ] Vec (TapeNodes.Matmul.matSize m n)) (hA : HasFDerivAt (fun (q : E) => (fderiv ℝ X q) left) DA p) (i : Fin m) (j : Fin n) (gamma beta : ℝ) : (fderiv ℝ (fun (q : E) => (fderiv ℝ (fun (y : E) => gamma * nrm (X y) ε i j + beta) q) left) p) right = gamma * normalizedMixed (X p) ((fderiv ℝ X p) left) ((fderiv ℝ X p) right) (DA right) ε i j

The actual affine row output has the same mixed derivative, multiplied by its fixed scale.

theorem Proofs.Autograd.RowNorm.fderiv_fderiv_nrm_comp {m n : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {ε : ℝ} (hε : 0 < ε) (X : E → Vec (TapeNodes.Matmul.matSize m n)) (p u v : E) (hX : ∀ (q : E), DifferentiableAt ℝ X q) (DA : E →L[ℝ] Vec (TapeNodes.Matmul.matSize m n)) (hA : HasFDerivAt (fun (q : E) => (fderiv ℝ X q) u) DA p) (i : Fin m) (j : Fin n) : (fderiv ℝ (fun (q : E) => (fderiv ℝ (fun (y : E) => nrm (X y) ε i j) q) u) p) v = normalizedMixed (X p) ((fderiv ℝ X p) u) ((fderiv ℝ X p) v) (DA v) ε i j

Mixed chain rule for an actual composed row, with fixed left direction u: the case gamma = 1, beta = 0 of fderiv_fderiv_affine_nrm_comp.

noncomputable def Proofs.Autograd.RowNorm.varianceFirstRadius {n : ℕ} (u a : Fin n → ℝ) : ℝ

A bound for qL = 2 mean(z*a) from centered magnitudes.

noncomputable def Proofs.Autograd.RowNorm.varianceMixedRadius {n : ℕ} (u a b c : Fin n → ℝ) : ℝ

A bound for qLR = 2 mean(a*b + z*c) from centered magnitudes.

noncomputable def Proofs.Autograd.RowNorm.inverseFirstRadius {n : ℕ} (ε : ℝ) (u a : Fin n → ℝ) : ℝ

Radius for the inverse-standard-deviation differential, using only epsilon.

noncomputable def Proofs.Autograd.RowNorm.inverseMixedRadius {n : ℕ} (ε : ℝ) (u a b c : Fin n → ℝ) : ℝ

Radius for the mixed inverse-standard-deviation differential.

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

First row radius for bounds on already centered input and direction.

noncomputable def Proofs.Autograd.RowNorm.centeredMixedRadius {n : ℕ} (ε : ℝ) (u a b c : Fin n → ℝ) (j : Fin n) : ℝ

Mixed row radius for centered input, two first directions, and one mixed direction.

theorem Proofs.Autograd.RowNorm.abs_varianceFirst_le {m n : ℕ} (X A : Vec (TapeNodes.Matmul.matSize m n)) (i : Fin m) (u a : Fin n → ℝ) (hu : ∀ (k : Fin n), |centered X i k| ≤ u k) (ha : ∀ (k : Fin n), |centered A i k| ≤ a k) : |varianceFirst X A i| ≤ varianceFirstRadius u a

Centered bounds on the input and one direction enclose the variance differential.

theorem Proofs.Autograd.RowNorm.abs_varianceMixed_le {m n : ℕ} (X A B C : Vec (TapeNodes.Matmul.matSize m n)) (i : Fin m) (u a b c : Fin n → ℝ) (hu : ∀ (k : Fin n), |centered X i k| ≤ u k) (ha : ∀ (k : Fin n), |centered A i k| ≤ a k) (hb : ∀ (k : Fin n), |centered B i k| ≤ b k) (hc : ∀ (k : Fin n), |centered C i k| ≤ c k) : |varianceMixed X A B C i| ≤ varianceMixedRadius u a b c

Centered bounds enclose the mixed variance differential.

theorem Proofs.Autograd.RowNorm.abs_inverseFirst_le {m n : ℕ} {ε : ℝ} (hε : 0 < ε) (X A : Vec (TapeNodes.Matmul.matSize m n)) (i : Fin m) (u a : Fin n → ℝ) (hu : ∀ (k : Fin n), |centered X i k| ≤ u k) (ha : ∀ (k : Fin n), |centered A i k| ≤ a k) : |inverseFirst X A ε i| ≤ inverseFirstRadius ε u a

Centered bounds enclose the inverse-standard-deviation differential, using only ε for the standard deviation.

theorem Proofs.Autograd.RowNorm.abs_inverseMixed_le {m n : ℕ} {ε : ℝ} (hε : 0 < ε) (X A B C : Vec (TapeNodes.Matmul.matSize m n)) (i : Fin m) (u a b c : Fin n → ℝ) (hu : ∀ (k : Fin n), |centered X i k| ≤ u k) (ha : ∀ (k : Fin n), |centered A i k| ≤ a k) (hb : ∀ (k : Fin n), |centered B i k| ≤ b k) (hc : ∀ (k : Fin n), |centered C i k| ≤ c k) : |inverseMixed X A B C ε i| ≤ inverseMixedRadius ε u a b c

Centered bounds enclose the mixed inverse-standard-deviation differential.

theorem Proofs.Autograd.RowNorm.abs_nrmD_le_centered {m n : ℕ} {ε : ℝ} (hε : 0 < ε) (X A : Vec (TapeNodes.Matmul.matSize m n)) (i : Fin m) (j : Fin n) (u a : Fin n → ℝ) (hu : ∀ (k : Fin n), |centered X i k| ≤ u k) (ha : ∀ (k : Fin n), |centered A i k| ≤ a k) : |(nrmD X ε i j) A| ≤ centeredFirstRadius ε u a j

The first differential is bounded from centered data, without a derivative-bound premise.

theorem Proofs.Autograd.RowNorm.abs_normalizedMixed_le {m n : ℕ} {ε : ℝ} (hε : 0 < ε) (X A B C : Vec (TapeNodes.Matmul.matSize m n)) (i : Fin m) (j : Fin n) (u a b c : Fin n → ℝ) (hu : ∀ (k : Fin n), |centered X i k| ≤ u k) (ha : ∀ (k : Fin n), |centered A i k| ≤ a k) (hb : ∀ (k : Fin n), |centered B i k| ≤ b k) (hc : ∀ (k : Fin n), |centered C i k| ≤ c k) : |normalizedMixed X A B C ε i j| ≤ centeredMixedRadius ε u a b c j

Centered magnitudes enclose all four terms of the analytic mixed chain formula.

theorem Proofs.Autograd.RowNorm.fderiv_fderiv_affine_nrm_comp_mem_Icc {m n : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {ε : ℝ} (hε : 0 < ε) (X : E → Vec (TapeNodes.Matmul.matSize m n)) (p left right : E) (hX : ∀ (q : E), DifferentiableAt ℝ X q) (DA : E →L[ℝ] Vec (TapeNodes.Matmul.matSize m n)) (hA : HasFDerivAt (fun (q : E) => (fderiv ℝ X q) left) DA p) (i : Fin m) (j : Fin n) (gamma beta : ℝ) (u a b c : Fin n → ℝ) (hu : ∀ (k : Fin n), |centered (X p) i k| ≤ u k) (ha : ∀ (k : Fin n), |centered ((fderiv ℝ X p) left) i k| ≤ a k) (hb : ∀ (k : Fin n), |centered ((fderiv ℝ X p) right) i k| ≤ b k) (hc : ∀ (k : Fin n), |centered (DA right) i k| ≤ c k) : (fderiv ℝ (fun (q : E) => (fderiv ℝ (fun (y : E) => gamma * nrm (X y) ε i j + beta) q) left) p) right ∈ Set.Icc (-(|gamma| * centeredMixedRadius ε u a b c j)) (|gamma| * centeredMixedRadius ε u a b c j)

Enclosure of the actual mixed derivative of a composed row with fixed affine scale.