ML.NeuralNet
Roll-up for dense affine layers, activations carrying Lipschitz constants, and uniform-width feedforward network evaluation.
Layer 4 core · 0 supporting A dense (affine) layer x ↦ W x + b and an activation function carrying its Lipschitz constant. ★ DenseLayer★ Activation
Neural-network layers
A dense (affine) layer x ↦ W x + b and an activation function carrying its
Lipschitz constant. These are the building blocks composed in
NeuralNet/FeedForward.lean.
A dense affine layer bundles a weight matrix and a bias vector determining the map from Fin m inputs to Fin n outputs.
For an input dimension, an output dimension, a dense affine layer, and an input vector, the layer evaluation is the output vector whose th coordinate is the weighted sum of the input coordinates plus the th bias.
Definition (Lean source)
An activation function bundles a scalar map together with a Lipschitz constant and the certificate that the map is Lipschitz with that constant (e.g. ReLU, sigmoid, and tanh are all 1-Lipschitz).
Definition (Lean source)
For a vector dimension, an activation-function bundle, and an input vector, the coordinatewise activation is the vector obtained by applying the bundle's scalar activation to each coordinate of the input.
Definition (Lean source)
FeedForward 3 core · 1 supporting A uniform-width feedforward network is a list of dense layers evaluated left-to-right with an activation after each affine map. ★ evalLayers_lipschitz
Feedforward networks (uniform width)
A uniform-width feedforward network is a list of dense layers evaluated left-to-right with an activation after each affine map. Structural facts: the evaluation respects layer concatenation (composition), and the network is Lipschitz with constant the product of the per-layer Lipschitz constants. Universal approximation and training dynamics are out of scope.
For a nonnegative network width, an activation function, a dense layer with that finite input and output width, and an input vector of that width, the one-layer network map applies the layer's affine transformation and then applies the activation function to each coordinate.
Definition (Lean source)
For a nonnegative network width and an activation function, the evaluation of a uniform-width feedforward network maps a finite ordered list of equal-width dense layers and an input vector to its output vector. For an empty list, the output is the input itself; for a list whose first layer is followed by further layers, the output applies the first layer and then evaluates the remaining layers.
Definition (Lean source)
Structure — Lipschitz. For a uniform-width feedforward network with activation σ and layer list Ls, if each layer's affine-then-activation map is Lipschitz with the constant assigned to it by k, then the whole network evaluation is Lipschitz with constant equal to the product of the per-layer constants.
Formal statement
Proof (Lean source)
1 supporting declaration (lemmas, instances)
-
evalLayers_appendtheorem — Structure — composition. Evaluating concatenated layer lists is the composition of the two evaluations.hypothesesconclusionProof (Lean source)
theorem evalLayers_append {n : ℕ} (σ : Activation) (Ls Ms : List (DenseLayer n n)) (x : Fin n → ℝ) : evalLayers σ (Ls ++ Ms) x = evalLayers σ Ms (evalLayers σ Ls x) := by induction Ls generalizing x with | nil => rfl | cons L Ls ih => simp [evalLayers, ih]