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
L2norm here is proof-oriented: it is defined fromSpec.tensorNormSquared, the same dot-product/sum-of-squares object used throughout tensor algebra proofs. NN.MLTheory.Robustness.Specalso 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 #
- $\ell_2$/$\ell_1$/$\ell_\infty$ norms correspond to PyTorch’s
torch.linalg.*_norm/torch.linalg.normAPIs. 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(andtorch.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
Tensorencoding.
$\ell_2$ norm (Euclidean norm) for tensors. Fundamental for measuring tensor magnitudes and distances.
Instances For
$\ell_\infty$ norm (maximum norm) for tensors. Important for uniform convergence and pointwise bounds.
Instances For
$\ell_1$ norm (Manhattan norm) for tensors. Useful for sparsity-inducing regularization.
Instances For
Distance function based on the $\ell_2$ norm.
Instances For
Distance function based on the $\ell_\infty$ norm.
Instances For
Cross-library norm facts #
NN.MLTheory.Robustness.Spec defines a scalar-polymorphic tensor_linf_norm. In this file we work
over $\mathbb R$ and often use tensor_l2_norm. The key inequality
$\lVert v\rVert_\infty\le\lVert v\rVert_2$ is what lets $\ell_2$-based
Lipschitz proofs feed directly into the $\ell_\infty$-robustness lemmas.
For a real vector-valued tensor, the $\ell_\infty$ norm from
NN.MLTheory.Robustness.Spec is bounded by the $\ell_2$ norm from this file:
$\lVert v\rVert_\infty\le\lVert v\rVert_2$.
The $\ell_2$ norm is nonnegative.
The $\ell_2$ norm is zero if and only if the tensor is zero.
Basic lemma: dot product with zero tensor is zero.
Bilinearity of dot product over addition (distributive property).
Bilinearity of the dot product: $\operatorname{dot}(x+ty,x+ty)=\lVert x\rVert^2+2t\langle x,y\rangle+t^2\lVert y\rVert^2$.
Cauchy-Schwarz inequality for tensors. For any tensors $x$ and $y$, $|\langle x,y\rangle|\le\lVert x\rVert\,\lVert y\rVert$. This is a fundamental inequality in inner product spaces.
Triangle inequality for the $\ell_2$ norm.
Homogeneity of the $\ell_2$ norm.
ReLU is 1-Lipschitz on scalar tensors.
General ReLU Lipschitz theorem for arbitrary tensor shapes. Main result: ReLU is 1-Lipschitz in the $\ell_2$ norm for any tensor shape.
Vector-shaped 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.
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.
Subtracting the zero tensor on the right leaves the tensor unchanged.
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.
Upper bound on a matrix operator norm.
We use the Frobenius-norm-style bound:
$$ \operatorname{matrixOpNorm}(W) =\sqrt{\sum_i\lVert\operatorname{row}_i(W)\rVert_2^2}, $$
which satisfies $\lVert Wx\rVert_2\le\operatorname{matrixOpNorm}(W)\lVert x\rVert_2$.
Instances For
Frobenius-based operator norm bound: $\lVert Wx\rVert_2\le\operatorname{matrixOpNorm}(W)\lVert x\rVert_2$.
Linear transformations preserve $\ell_2$-norm bounds. Fundamental theorem for neural network stability analysis.
Composition of Lipschitz functions preserves Lipschitz property. Essential for analyzing deep neural networks.
ReLU + Linear composition Lipschitz bound. Practical theorem for single neural network layer analysis.