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.
Dense-layer evaluation sends an input vector through an affine layer, producing one output coordinate as the weighted input sum plus its bias. The layer maps the stated input and output dimensions.
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)
Coordinatewise activation transforms an input vector by applying the scalar activation coordinatewise, using the activation bundle at the chosen finite dimension.
Definition (Lean source)
FeedForward 4 core · 6 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 activation Lipschitz constant and
the induced L∞ operator norm of each layer's weight matrix.
Universal approximation and training dynamics are out of scope.
A one-layer network map applies an affine layer then activates. It combines a square dense layer and activation function at the chosen finite width and acts on an input vector.
Definition (Lean source)
The weight Lipschitz constant extracts the induced L∞ weight norm from a square dense layer.
Definition (Lean source)
Uniform-width feedforward evaluation composes affine-then-activation maps using the chosen activation function at a fixed finite width. An empty network returns its input, while a nonempty network applies its head before its tail.
Definition (Lean source)
A feedforward network is Lipschitz with its product activation--weight bound. The full network evaluation has the product bound for the bundled activation function and the ordered square layers.
Formal statement
Proof (Lean source)
6 supporting declarations (lemmas, instances)
-
weightLip_eqtheorem — A dense layer's weight Lipschitz constant is the largest absolute row sum, giving an explicit induced L∞ operator norm for the square weight matrix.hypothesesn :ℕL :DenseLayer n nProof (Lean source)
theorem DenseLayer.weightLip_eq {n : ℕ} (L : DenseLayer n n) : L.weightLip = (Finset.univ : Finset (Fin n)).sup fun i => ∑ j : Fin n, ‖L.W i j‖₊ := by unfold DenseLayer.weightLip letI := linftyOpNormedAddCommGroup (m := Fin n) (n := Fin n) (α := ℝ) exact Matrix.linfty_opNNNorm_def L.W -
eval_lipschitztheorem — Affine evaluation is Lipschitz with the induced L∞ norm of the weight matrix for every square dense layer; the bias cancels when comparing two inputs.Proof (Lean source)
theorem DenseLayer.eval_lipschitz {n : ℕ} (L : DenseLayer n n) : LipschitzWith L.weightLip L.eval := by letI := linftyOpNormedAddCommGroup (m := Fin n) (n := Fin n) (α := ℝ) apply LipschitzWith.of_dist_le_mul intro x y rw [dist_eq_norm, dist_eq_norm] have heval : L.eval x - L.eval y = mulVec L.W (x - y) := by funext i simp [DenseLayer.eval, Matrix.mulVec_sub] rw [heval] simpa [DenseLayer.weightLip] using Matrix.linfty_opNorm_mulVec L.W (x - y) -
applyVec_lipschitztheorem — Coordinatewise activation preserves the bundled scalar Lipschitz constant on finite vectors for the chosen activation function.hypothesesn :ℕσ :conclusionProof (Lean source)
theorem Activation.applyVec_lipschitz {n : ℕ} (σ : Activation) : LipschitzWith σ.lip (σ.applyVec : (Fin n → ℝ) → (Fin n → ℝ)) := by apply LipschitzWith.of_dist_le_mul intro x y exact (dist_pi_le_iff (mul_nonneg σ.lip.2 dist_nonneg)).2 fun i => by change dist (σ.act (x i)) (σ.act (y i)) ≤ _ calc dist (σ.act (x i)) (σ.act (y i)) ≤ σ.lip * dist (x i) (y i) := σ.isLipschitz.dist_le_mul (x i) (y i) _ ≤ σ.lip * dist x y := mul_le_mul_of_nonneg_left (dist_le_pi_dist x y i) σ.lip.2 -
layerMap_lipschitztheorem — An affine-then-activation layer has the product Lipschitz bound, combining the activation function with a square dense layer.hypothesesconclusionLipschitzWith (σ.lip * L.weightLip) (layerMap σ L)Proof (Lean source)
theorem layerMap_lipschitz {n : ℕ} (σ : Activation) (L : DenseLayer n n) : LipschitzWith (σ.lip * L.weightLip) (layerMap σ L) := by change LipschitzWith (σ.lip * L.weightLip) (fun x => σ.applyVec (L.eval x)) exact σ.applyVec_lipschitz.comp L.eval_lipschitz -
evalLayers_appendtheorem — Network concatenation evaluates by function composition. Joined lists apply the first network and then the second, for the chosen activation function, the two layer lists, and the input vector.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] -
evalLayers_lipschitz_of_foralltheorem — Per-layer Lipschitz bounds multiply through a feedforward network. The whole network has the product bound for the activation function and ordered layer list, provided each layer has an assigned constant and every layer map obeys its assignment.hypothesesn :ℕσ :Ls :List (DenseLayer n n)K :DenseLayer n n → NNRealhK :∀ L ∈ Ls, LipschitzWith (K L) (layerMap σ L)conclusionProof (Lean source)
theorem evalLayers_lipschitz_of_forall {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 => have hid : LipschitzWith (1 : NNReal) (fun x : Fin n → ℝ => x) := LipschitzWith.id simpa [evalLayers] using hid | cons L Ls ih => have hhead : LipschitzWith (K L) (layerMap σ L) := hK L (by simp) have htail : ∀ M ∈ Ls, LipschitzWith (K M) (layerMap σ M) := by intro M hM exact hK M (by simp [hM]) simpa [evalLayers, Function.comp_def, mul_comm] using (ih htail).comp hhead