Lipschitz continuity library for `Tensor`-level ops #

This file proves basic norm and distance facts for TorchLean tensors over ℝ, and uses them to derive Lipschitz-style bounds for common neural-network building blocks.

Scope and conventions #

Everything here is spec-level and real-valued (ℝ), so we can freely use Mathlib’s analysis and order theory.
The main L2 norm here is proof-oriented: it is defined from Spec.tensorNormSquared, the same dot-product/sum-of-squares object used throughout tensor algebra proofs.
NN.MLTheory.Robustness.Spec also has scalar-polymorphic norm definitions for runtime and verification statements. This file does not duplicate that API surface; it proves real-valued theorems and includes bridge lemmas where those polymorphic specs need theorem-level support.

PyTorch correspondence / citations #

L2/L1/L∞ norms correspond to PyTorch’s torch.linalg.*_norm / torch.linalg.norm APIs. https://pytorch.org/docs/stable/generated/torch.linalg.vector_norm.html https://pytorch.org/docs/stable/generated/torch.linalg.norm.html
ReLU corresponds to torch.nn.functional.relu (and torch.nn.ReLU). https://pytorch.org/docs/stable/generated/torch.nn.functional.relu.html

Typical downstream use #

These lemmas are intended to be imported by higher-level results that need quantitative smoothness statements, e.g.:

proving that a composed network is Lipschitz (by composing layer-wise constants),
justifying robustness bounds that depend on Lipschitz constants, or
providing assumptions for convergence/step-size arguments.

References #

The key analytic tool is the Mean Value Theorem / derivative bounds, as formalized in Mathlib: Mathlib.Analysis.Calculus.MeanValue.
The mathematics is standard (functional analysis / optimization folklore); this file’s value is aligning those facts with TorchLean’s Tensor encoding.

source

noncomputable def Proofs.tensorL2Norm {s : Spec.Shape} (t : Spec.Tensor ℝ s) :

ℝ

L2 norm (Euclidean norm) for tensors. Fundamental for measuring tensor magnitudes and distances.

Instances For

source

noncomputable def Proofs.tensorLInftyNorm {s : Spec.Shape} (t : Spec.Tensor ℝ s) :

ℝ

L∞ norm (maximum norm) for tensors. Important for uniform convergence and pointwise bounds.

Instances For

source

noncomputable def Proofs.tensorL1Norm {s : Spec.Shape} (t : Spec.Tensor ℝ s) :

ℝ

L1 norm (Manhattan norm) for tensors. Useful for sparsity-inducing regularization.

Instances For

source

noncomputable def Proofs.tensorL2Dist {s : Spec.Shape} (x y : Spec.Tensor ℝ s) :

ℝ

Distance function based on L2 norm.

Instances For

source

noncomputable def Proofs.tensorLInftyDist {s : Spec.Shape} (x y : Spec.Tensor ℝ s) :

ℝ

Distance function based on L∞ norm.

Instances For

Cross-library norm facts #

NN.MLTheory.Robustness.Spec defines a scalar-polymorphic tensor_linf_norm. In this file we work over ℝ and often use tensor_l2_norm. The key inequality ‖v‖∞ ≤ ‖v‖₂ is what lets L2-based Lipschitz proofs feed directly into the L∞-robustness lemmas.

source

theorem Proofs.tensor_linf_norm_le_tensor_l2_norm {n : ℕ} (y : Spec.Tensor ℝ (Spec.Shape.dim n Spec.Shape.scalar)) :

NN.MLTheory.Robustness.Spec.tensorLinfNorm y ≤ tensorL2Norm y

For a real vector-valued tensor, the L∞ norm from NN.MLTheory.Robustness.Spec is bounded by the L2 norm from this file:

‖v‖∞ ≤ ‖v‖₂.

source

theorem Proofs.tensor_l2_norm_nonneg {s : Spec.Shape} (t : Spec.Tensor ℝ s) :

tensorL2Norm t ≥ 0

L2 norm is non-negative.

source

theorem Proofs.tensor_l2_norm_zero_iff {s : Spec.Shape} (t : Spec.Tensor ℝ s) :

tensorL2Norm t = 0 ↔ t = Spec.fill 0 s

L2 norm is zero iff tensor is zero.

source

theorem Proofs.dot_zero_right {s : Spec.Shape} (x : Spec.Tensor ℝ s) :

Spec.dot x (Spec.fill 0 s) = 0

Basic lemma: dot product with zero tensor is zero.

source

theorem Proofs.dot_add_add {s : Spec.Shape} (x y : Spec.Tensor ℝ s) :

Spec.dot (x.addSpec y) (x.addSpec y) = Spec.dot x x + 2 * Spec.dot x y + Spec.dot y y

Bilinearity of dot product over addition (distributive property).

source

theorem Proofs.dot_quadratic_expand {s : Spec.Shape} (x y : Spec.Tensor ℝ s) (t : ℝ) :

Spec.dot (x.addSpec (y.scaleSpec t)) (x.addSpec (y.scaleSpec t)) = Spec.dot x x + 2 * t * Spec.dot x y + t ^ 2 * Spec.dot y y

Bilinearity of dot product: dot (x + ty) (x + ty) = ||x||² + 2t⟨x,y⟩ + t²||y||²

source

theorem Proofs.tensor_cauchy_schwarz {s : Spec.Shape} (x y : Spec.Tensor ℝ s) :

|Spec.dot x y| ≤ tensorL2Norm x * tensorL2Norm y

Cauchy-Schwarz inequality for tensors. For any tensors x, y: |⟨x,y⟩| ≤ ||x|| * ||y|| This is a fundamental inequality in inner product spaces.

source

theorem Proofs.tensor_l2_norm_triangle {s : Spec.Shape} (x y : Spec.Tensor ℝ s) :

tensorL2Norm (x.addSpec y) ≤ tensorL2Norm x + tensorL2Norm y

Triangle inequality for L2 norm.

source

theorem Proofs.tensor_l2_norm_scale {s : Spec.Shape} (t : Spec.Tensor ℝ s) (c : ℝ) :

tensorL2Norm (t.scaleSpec c) = |c| * tensorL2Norm t

Homogeneity of L2 norm.

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 : Spec.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 : Spec.Tensor ℝ s) :

tensorL2Dist (Activation.reluSpec x) (Activation.reluSpec y) ≤ tensorL2Dist x y

General ReLU Lipschitz theorem for arbitrary tensor shapes. Main result: ReLU is 1-Lipschitz in L2 norm for any tensor shape.

source

theorem Proofs.relu_vector_lipschitz {n : ℕ} (x y : Spec.Tensor ℝ (Spec.Shape.dim n Spec.Shape.scalar)) :

tensorL2Dist (Activation.reluSpec x) (Activation.reluSpec y) ≤ tensorL2Dist x y

Vector-shaped ReLU is 1-Lipschitz in L2.

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.sub_spec_eq_add_scale_neg_one {s : Spec.Shape} (a b : Spec.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 : Spec.Tensor ℝ s) :

t.subSpec (Spec.fill 0 s) = t

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

source

theorem Proofs.mat_vec_mul_spec_zero {m n : ℕ} (W : Spec.Tensor ℝ (Spec.Shape.dim m (Spec.Shape.dim n Spec.Shape.scalar))) :

Spec.matVecMulSpec W (Spec.fill 0 (Spec.Shape.dim n Spec.Shape.scalar)) = Spec.fill 0 (Spec.Shape.dim m Spec.Shape.scalar)

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