Real-valued tensor norm facts #

This module owns the proof-oriented Tensor norm and distance definitions over ℝ, together with their algebraic properties. Neural-network Lipschitz bounds build on these facts in NN.Proofs.Analysis.Lipschitz.Network.

Scope and conventions #

Everything here is spec-level and real-valued (ℝ), so we can freely use Mathlib's analysis and order theory.
Tensor ℝ s is an InnerProductSpace ℝ (see NN.Proofs.Tensor.Euclidean). The bridge lemmas tensorL2Norm_eq_norm, tensorL2Dist_eq_dist, and dot_eq_inner identify the historical tensorL2Norm, tensorL2Dist, and Spec.dot with ‖·‖, dist, and ⟪·, ·⟫_ℝ; every norm inequality below is then a direct instance of the Mathlib theorem.
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 #

$\ell_2$/$\ell_1$/$\ell_\infty$ 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

Import NN.Proofs.Analysis.Lipschitz for both the norm foundation and network bounds, or this module when only the norm theory is needed.

Tensor norms and distance functions #

source

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

ℝ

$\ell_2$ norm (Euclidean norm) for tensors. Fundamental for measuring tensor magnitudes and distances.

Instances For

source

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

ℝ

$\ell_\infty$ norm (maximum norm) for tensors. Important for uniform convergence and pointwise bounds.

Instances For

source

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

ℝ

$\ell_1$ norm (Manhattan norm) for tensors. Useful for sparsity-inducing regularization.

Instances For

source

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

ℝ

Distance function based on the $\ell_2$ norm.

Instances For

source

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

ℝ

Distance function based on the $\ell_\infty$ norm.

Instances For

Bridges to the inner product space structure #

source

theorem Proofs.full_zero_eq_zero (s : Spec.Shape) :

TorchLean.Tensor.full s 0 = 0

The zero-filled tensor is the zero of the additive group.

source

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

t.scaleSpec c = c • t

Scaling by a scalar is the module action.

source

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

Spec.tensorNormSquared t = ∑ i : TorchLean.Tensor.Internal.Coord s, TorchLean.Tensor.Internal.Rep.get t i ^ 2

The squared norm is the coordinate sum of squares.

source

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

Spec.dot x y = inner ℝ x y

Spec.dot is the Euclidean inner product.

source

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

Spec.tensorNormSquared t = ‖t‖ ^ 2

tensorNormSquared is the squared Euclidean norm.

source

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

tensorL2Norm t = ‖t‖

tensorL2Norm is the Euclidean norm.

source

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

tensorL2Dist x y = dist x y

tensorL2Dist is the Euclidean distance.

Cross-library norm facts #

NN.MLTheory.Robustness.Spec defines a scalar-polymorphic tensorLinfNorm. In this file we work over $\mathbb R$ and often use tensorL2Norm. 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.

source

theorem Proofs.tensor_linf_norm_le_tensor_l2_norm {n : ℕ} (y : TorchLean.Tensor ℝ [n]) :

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

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

Basic norm properties used throughout the Lipschitz development #

source

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

tensorL2Norm t ≥ 0

The $\ell_2$ norm is nonnegative.

source

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

tensorL2Norm t = 0 ↔ t = TorchLean.Tensor.full s 0

The $\ell_2$ norm is zero if and only if the tensor is zero.

source

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

Spec.dot x (TorchLean.Tensor.full s 0) = 0

Basic lemma: dot product with zero tensor is zero.

source

theorem Proofs.dot_add_add {s : Spec.Shape} (x y : TorchLean.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 : TorchLean.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 the dot product: $\operatorname{dot}(x+ty,x+ty)=\lVert x\rVert^2+2t\langle x,y\rangle+t^2\lVert y\rVert^2$.

source

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

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

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.

source