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 $\mathbb{R}$.
• 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 $|\operatorname{ReLU}(x)-\operatorname{ReLU}(y)|\le|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 : TorchLean.Tensor ℝ [m, n]) : 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 : TorchLean.Tensor ℝ s) : t ≠ TorchLean.Tensor.full s 0 → 0 < Proofs.tensorL2Norm t

A non-zero tensor has positive L2 norm

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

Frobenius-norm Lipschitz bound for a linear layer's weight matrix.

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

Linear layers are Lipschitz continuous with the Frobenius norm as a valid, possibly loose, bound.

theorem NN.MLTheory.Proofs.relu_activation_lipschitz {n : ℕ} (x y : TorchLean.Tensor ℝ [n]) : Proofs.tensorL2Dist (Activation.reluSpec x) (Activation.reluSpec y) ≤ Proofs.tensorL2Dist x y

ReLU is 1-Lipschitz in the L2 distance, so activations never amplify an input perturbation.

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 ≠ TorchLean.Tensor.full [hidDim, inDim] 0) (h2_nonzero : l2.weights ≠ TorchLean.Tensor.full [outDim, hidDim] 0) : ∃ lipschitzConstant > 0, ∀ (x y : TorchLean.Tensor ℝ [inDim]), Proofs.tensorL2Dist (Examples.mlpForward l1 l2 x) (Examples.mlpForward l1 l2 y) ≤ lipschitzConstant * Proofs.tensorL2Dist x y

A two-layer MLP is Lipschitz, with a positive constant obtained as the product of the layer constants.

The constant here is the naive product of operator norms, which is what makes it cheap: it needs no information about the input region. That is also why it is loose compared to the CROWN bounds in NN.MLTheory.CROWN, and the contrast is the reason both developments are kept.

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 ≠ TorchLean.Tensor.full [hidDim, inDim] 0) (h2_nonzero : l2.weights ≠ TorchLean.Tensor.full [outDim, hidDim] 0) : ∃ L > 0, Robustness.Spec.isLipschitzContinuous (fun (x : TorchLean.Tensor ℝ [inDim]) => 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 isLipschitzContinuous fact.

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

theorem NN.MLTheory.Proofs.mlp_output_drift_bound_on_ball {inDim hidDim outDim : ℕ} (l1 : Spec.LinearSpec ℝ inDim hidDim) (l2 : Spec.LinearSpec ℝ hidDim outDim) (h1_nonzero : l1.weights ≠ TorchLean.Tensor.full [hidDim, inDim] 0) (h2_nonzero : l2.weights ≠ TorchLean.Tensor.full [outDim, hidDim] 0) (x₀ : TorchLean.Tensor ℝ [inDim]) (perturbationRadius : ℝ) : perturbationRadius > 0 → ∃ robustnessGuarantee > 0, ∀ (x : TorchLean.Tensor ℝ [inDim]), Proofs.tensorL2Dist x₀ x ≤ perturbationRadius → Proofs.tensorL2Dist (Examples.mlpForward l1 l2 x₀) (Examples.mlpForward l1 l2 x) ≤ robustnessGuarantee * perturbationRadius

Bound output drift on an input ball. This theorem does not by itself preserve a class label.

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.