TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

NN.Proofs.Analysis.Lipschitz.Network

Lipschitz bounds for neural-network operations #

This module owns Lipschitz estimates for ReLU, matrix-vector multiplication, linear layers, and composition. The underlying real-valued tensor norm API lives in NN.Proofs.Analysis.Lipschitz.Norm.

Import NN.Proofs.Analysis.Lipschitz for the complete norm and network-bound API.

Bridges between tensorL2Dist bounds and Mathlib's LipschitzWith #

source
theorem Proofs.lipschitzWith_of_tensorL2Dist_le {s t : Spec.Shape} {f : TorchLean.Tensor ℝ s → TorchLean.Tensor ℝ t} {L : ℝ} (hL : 0 ≤ L) (h : ∀ (x y : TorchLean.Tensor ℝ s), tensorL2Dist (f x) (f y) ≤ L * tensorL2Dist x y) :
LipschitzWith ⟨L, hL⟩ f

A tensorL2Dist bound with a nonnegative constant is a Mathlib Lipschitz bound.

source
theorem LipschitzWith.tensorL2Dist_le {s t : Spec.Shape} {f : TorchLean.Tensor ℝ s → TorchLean.Tensor ℝ t} {K : NNReal} (hf : LipschitzWith K f) (x y : TorchLean.Tensor ℝ s) :
Proofs.tensorL2Dist (f x) (f y) ≤ ↑K * Proofs.tensorL2Dist x y

A Mathlib Lipschitz bound on real tensors is a tensorL2Dist bound.

source
theorem Proofs.relu_scalar_lipschitz (x y : ℝ) :
|max 0 x - max 0 y| ≤ |x - y|

Pointwise ReLU is 1-Lipschitz for scalars. Foundation for tensor-level Lipschitz bounds.

source
theorem Proofs.relu_scalar_tensor_lipschitz (x y : TorchLean.Tensor ℝ Spec.Shape.scalar) :
tensorL2Dist (Activation.reluSpec x) (Activation.reluSpec y) ≤ tensorL2Dist x y

ReLU is 1-Lipschitz on scalar tensors.

source
theorem Proofs.relu_lipschitz_general {s : Spec.Shape} (x y : TorchLean.Tensor ℝ s) :
tensorL2Dist (Activation.reluSpec x) (Activation.reluSpec y) ≤ tensorL2Dist x y

ReLU is 1-Lipschitz in the L2 norm for tensors of every shape.

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

Rank-one ReLU is 1-Lipschitz in $\ell_2$.

This theorem is just the vector specialization of relu_lipschitz_general, but it is convenient for callers working with ordinary .dim n .scalar activations.

source
theorem Proofs.reluSpec_lipschitzWith {s : Spec.Shape} :
LipschitzWith 1 Activation.reluSpec

ReLU is 1-Lipschitz for the Euclidean metric on real tensors.

source
theorem Proofs.sub_spec_eq_add_scale_neg_one {s : Spec.Shape} (a b : TorchLean.Tensor ℝ s) :
a.subSpec b = a.addSpec (b.scaleSpec (-1))

Tensor subtraction can be rewritten as addition of a -1 scale.

This is a small algebraic normal form used by linear-operator proofs, where it is often easier to reuse additive and scaling lemmas than reason about subSpec directly.

source
theorem Proofs.sub_spec_zero_right {s : Spec.Shape} (t : TorchLean.Tensor ℝ s) :
t.subSpec (TorchLean.Tensor.full s 0) = t

Subtracting the zero tensor on the right leaves the tensor unchanged.

source
theorem Proofs.mat_vec_mul_spec_zero {m n : ℕ} (W : TorchLean.Tensor ℝ [m, n]) :
Spec.matVecMulSpec W (TorchLean.Tensor.full (Spec.Shape.dim n Spec.Shape.scalar) 0) = TorchLean.Tensor.full (Spec.Shape.dim m Spec.Shape.scalar) 0

Matrix-vector multiplication sends the zero vector to the zero vector.

The proof follows the spec definition: each output coordinate is a fold over scalar products, and every scalar product contains a zero input coordinate.

source
noncomputable def Proofs.matrixFrobeniusNorm {m n : ℕ} (W : TorchLean.Tensor ℝ [m, n]) :
ℝ

Frobenius norm of a matrix tensor.

We use the Frobenius-norm-style bound:

$$ \lVert W\rVert_F =\sqrt{\sum_i\lVert\operatorname{row}_i(W)\rVert_2^2}, $$

This is an upper bound for the induced Euclidean operator norm; it is not the spectral norm.

Instances For
    source
    theorem Proofs.matVec_norm_le_frobenius {m n : ℕ} (W : TorchLean.Tensor ℝ [m, n]) (x : TorchLean.Tensor ℝ [n]) :
    tensorL2Norm (Spec.matVecMulSpec W x) ≤ matrixFrobeniusNorm W * tensorL2Norm x

    The Frobenius norm bounds matrix-vector multiplication in the Euclidean norm.

    source
    theorem Proofs.linear_op_norm_bound {m n : ℕ} (W : TorchLean.Tensor ℝ [m, n]) (x y : TorchLean.Tensor ℝ [n]) :
    tensorL2Dist (Spec.matVecMulSpec W x) (Spec.matVecMulSpec W y) ≤ matrixFrobeniusNorm W * tensorL2Dist x y

    Linear transformations preserve $\ell_2$-norm bounds. Fundamental theorem for neural network stability analysis.

    source
    theorem Proofs.lipschitz_composition {s t u : Spec.Shape} (f : TorchLean.Tensor ℝ s → TorchLean.Tensor ℝ t) (g : TorchLean.Tensor ℝ t → TorchLean.Tensor ℝ u) (Lf Lg : ℝ) (hf : ∀ (x y : TorchLean.Tensor ℝ s), tensorL2Dist (f x) (f y) ≤ Lf * tensorL2Dist x y) (hg : ∀ (x y : TorchLean.Tensor ℝ t), tensorL2Dist (g x) (g y) ≤ Lg * tensorL2Dist x y) (hLg : 0 ≤ Lg) (x y : TorchLean.Tensor ℝ s) :
    tensorL2Dist (g (f x)) (g (f y)) ≤ Lg * Lf * tensorL2Dist x y

    Composition of Lipschitz functions preserves Lipschitz property. Essential for analyzing deep neural networks.

    This is LipschitzWith.comp read through tensorL2Dist_eq_dist. A negative Lf is degenerate: the hypothesis on f then forces x = y, and both sides vanish.

    source
    theorem Proofs.relu_linear_lipschitz {m n : ℕ} (W : TorchLean.Tensor ℝ [m, n]) (x y : TorchLean.Tensor ℝ [n]) :
    tensorL2Dist (Activation.reluSpec (Spec.matVecMulSpec W x)) (Activation.reluSpec (Spec.matVecMulSpec W y)) ≤ matrixFrobeniusNorm W * tensorL2Dist x y

    ReLU + Linear composition Lipschitz bound. Practical theorem for single neural network layer analysis.