ML.Neural­Net

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.

structure DenseLayer reviewed
Causalean.ML

A dense affine layer bundles a weight matrix and a bias vector determining the map x↦Wx+bx \mapsto Wx + b from Fin m inputs to Fin n outputs.

Definition (Lean source)
parameters
m n :
ℕ
fields
The weight matrix.
W :
Matrix (Fin n) (Fin m) ℝ
The bias vector.
b :
Fin n → ℝ
Causalean.ML.DenseLayer · Causalean/ML/NeuralNet/Layer.lean:21
def eval reviewed
Causalean.ML.DenseLayer

The affine map computed by a dense layer.

Definition (Lean source)
def DenseLayer.eval {m n : ℕ} (L : DenseLayer m n) (x : Fin m → ℝ) : Fin n → ℝ := fun j => (L.W *ᵥ x) j + L.b j
Causalean.ML.DenseLayer.eval · Causalean/ML/NeuralNet/Layer.lean:29 · uses DenseLayer
structure Activation reviewed
Causalean.ML

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)
fields
The scalar activation.
act :
ℝ → ℝ
A Lipschitz constant for the activation.
lip :
NNReal
Proof that `act` is `lip`-Lipschitz.
isLipschitz :
LipschitzWith lip act
Causalean.ML.Activation · Causalean/ML/NeuralNet/Layer.lean:33
def applyVec reviewed
Causalean.ML.Activation

Apply an activation coordinatewise to a vector.

Definition (Lean source)
def Activation.applyVec {n : ℕ} (σ : Activation) (x : Fin n → ℝ) : Fin n → ℝ := fun j => σ.act (x j)
Causalean.ML.Activation.applyVec · Causalean/ML/NeuralNet/Layer.lean:44 · uses Activation
Feed­Forward 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.

def layerMap reviewed
Causalean.ML

One network layer: the affine map followed by coordinatewise activation.

Definition (Lean source)
def layerMap {n : ℕ} (σ : Activation) (L : DenseLayer n n) (x : Fin n → ℝ) : Fin n → ℝ := σ.applyVec (L.eval x)
Causalean.ML.layerMap · Causalean/ML/NeuralNet/FeedForward.lean:21 · uses Activation , DenseLayer
def evalLayers reviewed
Causalean.ML

Evaluate a uniform-width feedforward network (a list of layers), folding left-to-right.

Definition (Lean source)
def evalLayers {n : ℕ} (σ : Activation) : List (DenseLayer n n) → (Fin n → ℝ) → (Fin n → ℝ) | [], x => x | L :: Ls, x => evalLayers σ Ls (layerMap σ L x)
Causalean.ML.evalLayers · Causalean/ML/NeuralNet/FeedForward.lean:25 · uses Activation , DenseLayer
theorem evalLayers_lipschitz reviewed
Causalean.ML

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
hypotheses
n :
ℕ
σ :
Activation
Ls :
List (DenseLayer n n)
k :
DenseLayer n n → NNReal
hk :
∀ L ∈ Ls, LipschitzWith (k L) (layerMap σ L)
conclusion
LipschitzWith (Ls.map k).prod (evalLayers σ Ls)
Proof (Lean source)
theorem evalLayers_lipschitz {n : ℕ} (σ : Activation) (Ls : List (DenseLayer n n)) (k : DenseLayer n n → NNReal) (hk : ∀ L ∈ Ls, LipschitzWith (k L) (layerMap σ L)) : LipschitzWith (Ls.map k).prod (evalLayers σ Ls) := by induction Ls with | nil => -- `simp` no longer unfolds `id`, so state the identity bound in the -- lambda form the goal uses. have hid : LipschitzWith (1 : NNReal) (fun x : Fin n → ℝ => x) := LipschitzWith.id simpa [evalLayers] using hid | cons L Ls ih => have hL : LipschitzWith (k L) (layerMap σ L) := hk L (by simp) have hLs : ∀ L' ∈ Ls, LipschitzWith (k L') (layerMap σ L') := by intro L' hL' exact hk L' (by simp [hL']) simpa [evalLayers, map_cons, List.prod_cons, mul_comm, Function.comp_def] using (ih hLs).comp hL
Causalean.ML.evalLayers_lipschitz · Causalean/ML/NeuralNet/FeedForward.lean:40 · uses Activation , DenseLayer , evalLayers , layerMap
1 supporting declaration (lemmas, instances)