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_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.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.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

    Matrix-vector multiplication is Lipschitz with its matrix's Frobenius norm as a bound.

    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

    Composing the two distance bounds multiplies their constants.

    The nonnegative Lg preserves the inequality when multiplying the bound for f. No sign assumption on Lf is needed.

    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 after matrix-vector multiplication retains the matrix's Frobenius Lipschitz bound.