Rowwise LayerNorm Derivative Bounds

Positive epsilon bounds the inverse standard deviation by 1 / sqrt epsilon. Centered input and direction bounds then control the first differential and the mixed second differential. Each row uses its own input box and the stored scale; the fixed bias has zero derivative.

def NN.MLTheory.CROWN.Graph.derivativeMagnitude {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] (bounds : α × α) : α

Upper bound on absolute value from a pair of interval endpoints.

def NN.MLTheory.CROWN.Graph.centeredDerivativeRadii? {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [NonlinearBoundOps α] {n : ℕ} (bounds : Fin n → α × α) : Option (Fin n → α)

Bound each coordinate after subtracting the same row's mean.

def NN.MLTheory.CROWN.Graph.meanDerivativeRadius? {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [NonlinearBoundOps α] {n : ℕ} (radius : Fin n → α) : Option α

Upper bound on the mean of nonnegative coordinate radii.

def NN.MLTheory.CROWN.Graph.layerNormDerivativeRow? {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [NonlinearBoundOps α] {n : ℕ} (input left right mixed : Fin n → α × α) (gamma : TorchLean.Tensor α [n]) (epsilon : α) : Option ((TorchLean.Tensor α [n] × TorchLean.Tensor α [n]) × TorchLean.Tensor α [n] × TorchLean.Tensor α [n])

Enclose one row's first and mixed-second differentials with fixed affine parameters.

For centered input z and centered directions a, b, c, the variance differentials are qL = 2 mean(z*a), qR = 2 mean(z*b), and qLR = 2 mean(a*b + z*c). The inverse-square-root differential contributes both r³ qLR / 2 and 3 r⁵ qL qR / 4. Keeping the latter term is essential for mixed directions.

def NN.MLTheory.CROWN.Graph.layerNormDerivativeMatrix? {α : Type} [TorchLean.Storage α] [Context α] (s : Spec.Shape) (rows width : ℕ) (box : FlatBox α) : Option (TorchLean.Tensor α [rows, width] × TorchLean.Tensor α [rows, width])

Restore the matrix view used by the LayerNorm semantics after validating a flat box.

def NN.MLTheory.CROWN.Graph.layerNormDerivativeBoxes? {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [NonlinearBoundOps α] (s : Spec.Shape) (axis : ℕ) (parameters : Option (IR.LayerNormParams α)) (input left right mixed : FlatBox α) : Option (FlatBox α × FlatBox α)

Enclose first and mixed-second LayerNorm differentials over any valid trailing shape.