MLP robustness: basic analytic lemmas

This file collects small real-analysis facts used by robustness statements for spec-level MLPs.

Contents:

• ReLU (written as max 0 x) is 1-Lipschitz on ℝ.
• Lipschitz bounds compose under function composition.
• A few tensor-norm helper lemmas that connect to the more general library in NN.Proofs.Analysis.Lipschitz.

References

• PyTorch ReLU: https://pytorch.org/docs/stable/generated/torch.nn.functional.relu.html

Basic Lipschitz lemmas

theorem NN.MLTheory.Proofs.relu_lipschitz_bound (x y : ℝ) : |max 0 x - max 0 y| ≤ |x - y|

Fundamental property: ReLU satisfies |ReLU(x) - ReLU(y)| ≤ |x - y|

theorem NN.MLTheory.Proofs.comp_lipschitz (f g : ℝ → ℝ) (h_f : ∀ (x y : ℝ), |f x - f y| ≤ |x - y|) (h_g : ∀ (x y : ℝ), |g x - g y| ≤ |x - y|) (x y : ℝ) : |(g ∘ f) x - (g ∘ f) y| ≤ |x - y|

Composition property for Lipschitz functions

theorem NN.MLTheory.Proofs.relu_comp_preserves (f : ℝ → ℝ) (h : ∀ (x y : ℝ), |f x - f y| ≤ |x - y|) (x y : ℝ) : |max 0 (f x) - max 0 (f y)| ≤ |x - y|

Main result: ReLU composition preserves unit Lipschitz property

Tensor helpers

def NN.MLTheory.Proofs.tensorNonzeroHasNonzeroEntry {m n : ℕ} (W : Spec.Tensor ℝ (Spec.Shape.dim m (Spec.Shape.dim n Spec.Shape.scalar))) : Prop

Definition: A non-zero tensor has at least one non-zero entry

theorem NN.MLTheory.Proofs.tensor_l2_norm_pos_of_ne_zero {s : Spec.Shape} (t : Spec.Tensor ℝ s) : t ≠ Spec.fill 0 s → 0 < Proofs.tensorL2Norm t

A non-zero tensor has positive L2 norm

noncomputable def NN.MLTheory.Proofs.linearLayerOperatorNorm {inDim outDim : ℕ} (layer : Spec.LinearSpec ℝ inDim outDim) : ℝ

Get the operator norm of the weight matrix in a linear layer

theorem NN.MLTheory.Proofs.linear_layer_lipschitz_bound {inDim outDim : ℕ} (layer : Spec.LinearSpec ℝ inDim outDim) (h_weights_nonzero : layer.weights ≠ Spec.fill 0 (Spec.Shape.dim outDim (Spec.Shape.dim inDim Spec.Shape.scalar))) : ∃ L > 0, ∀ (x y : Spec.Tensor ℝ (Spec.Shape.dim inDim Spec.Shape.scalar)), Proofs.tensorL2Dist (Spec.linearSpec layer x) (Spec.linearSpec layer y) ≤ L * Proofs.tensorL2Dist x y

Theorem: Linear layers are Lipschitz continuous with constant matrix_op_norm.

theorem NN.MLTheory.Proofs.relu_activation_lipschitz {n : ℕ} (x y : Spec.Tensor ℝ (Spec.Shape.dim n Spec.Shape.scalar)) : Proofs.tensorL2Dist (Activation.reluSpec x) (Activation.reluSpec y) ≤ Proofs.tensorL2Dist x y

theorem NN.MLTheory.Proofs.mlp_lipschitz_complete_analysis {inDim hidDim outDim : ℕ} (l1 : Spec.LinearSpec ℝ inDim hidDim) (l2 : Spec.LinearSpec ℝ hidDim outDim) (h1_nonzero : l1.weights ≠ Spec.fill 0 (Spec.Shape.dim hidDim (Spec.Shape.dim inDim Spec.Shape.scalar))) (h2_nonzero : l2.weights ≠ Spec.fill 0 (Spec.Shape.dim outDim (Spec.Shape.dim hidDim Spec.Shape.scalar))) : ∃ lipschitz_constant > 0, ∀ (x y : Spec.Tensor ℝ (Spec.Shape.dim inDim Spec.Shape.scalar)), Proofs.tensorL2Dist (Examples.mlpForward l1 l2 x) (Examples.mlpForward l1 l2 y) ≤ lipschitz_constant * Proofs.tensorL2Dist x y

theorem NN.MLTheory.Proofs.mlp_is_lipschitz_continuous_l2 {inDim hidDim outDim : ℕ} (l1 : Spec.LinearSpec ℝ inDim hidDim) (l2 : Spec.LinearSpec ℝ hidDim outDim) (h1_nonzero : l1.weights ≠ Spec.fill 0 (Spec.Shape.dim hidDim (Spec.Shape.dim inDim Spec.Shape.scalar))) (h2_nonzero : l2.weights ≠ Spec.fill 0 (Spec.Shape.dim outDim (Spec.Shape.dim hidDim Spec.Shape.scalar))) : ∃ L > 0, Robustness.Spec.isLipschitzContinuous (fun (x : Spec.Tensor ℝ (Spec.Shape.dim inDim Spec.Shape.scalar)) => Examples.mlpForward l1 l2 x) (fun {s : Spec.Shape} => Proofs.tensorL2Norm) (fun {s : Spec.Shape} => Proofs.tensorL2Norm) L

Repackage mlp_lipschitz_complete_analysis as a robustness-spec is_lipschitz_continuous fact.

This is the form expected by the certified-robustness lemmas in NN.MLTheory.Proofs.Verification.Robustness.LipschitzCertified.

theorem NN.MLTheory.Proofs.adversarial_robustness_certificate {inDim hidDim outDim : ℕ} (l1 : Spec.LinearSpec ℝ inDim hidDim) (l2 : Spec.LinearSpec ℝ hidDim outDim) (h1_nonzero : l1.weights ≠ Spec.fill 0 (Spec.Shape.dim hidDim (Spec.Shape.dim inDim Spec.Shape.scalar))) (h2_nonzero : l2.weights ≠ Spec.fill 0 (Spec.Shape.dim outDim (Spec.Shape.dim hidDim Spec.Shape.scalar))) (x₀ : Spec.Tensor ℝ (Spec.Shape.dim inDim Spec.Shape.scalar)) (perturbation_radius : ℝ) : perturbation_radius > 0 → ∃ robustness_guarantee > 0, ∀ (x : Spec.Tensor ℝ (Spec.Shape.dim inDim Spec.Shape.scalar)), Proofs.tensorL2Dist x₀ x ≤ perturbation_radius → Proofs.tensorL2Dist (Examples.mlpForward l1 l2 x₀) (Examples.mlpForward l1 l2 x) ≤ robustness_guarantee * perturbation_radius

Robustness statements for MLPs (ML theory layer).

This file collects robustness definitions and theorems specialized to multi-layer perceptrons, used as a bridge between learning-theory specifications and concrete model classes.