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 Spec.dot_eq_inner identify 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

• The $\ell_2$ norm corresponds to PyTorch's torch.linalg.vector_norm / torch.linalg.norm. 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

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.

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

Distance function based on the $\ell_2$ norm.

Bridges to the inner product space structure

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.

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.

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.

theorem Proofs.tensorNormSquared_eq_norm_sq {s : Spec.Shape} (t : TorchLean.Tensor ℝ s) : Spec.tensorNormSquared t = ‖t‖ ^ 2

tensorNormSquared is the squared Euclidean norm.

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

tensorL2Norm is the Euclidean norm.

theorem Proofs.sq_tensorL2Norm {s : Spec.Shape} (t : TorchLean.Tensor ℝ s) : tensorL2Norm t ^ 2 = Spec.tensorNormSquared t

Squaring the $\ell_2$ norm recovers the squared-norm spec.

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.

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

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

The $\ell_2$ norm is nonnegative.

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.

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.

theorem Proofs.tensor_l2_norm_triangle {s : Spec.Shape} (x y : TorchLean.Tensor ℝ s) : tensorL2Norm (x.addSpec y) ≤ tensorL2Norm x + tensorL2Norm y

Triangle inequality for the $\ell_2$ norm.

theorem Proofs.tensor_l2_norm_scale {s : Spec.Shape} (t : TorchLean.Tensor ℝ s) (c : ℝ) : tensorL2Norm (t.scaleSpec c) = |c| * tensorL2Norm t

Homogeneity of the $\ell_2$ norm.

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

tensorL2Dist is symmetric.

theorem Proofs.tensor_l2_dist_triangle {s : Spec.Shape} (x y z : TorchLean.Tensor ℝ s) : tensorL2Dist x z ≤ tensorL2Dist x y + tensorL2Dist y z

Triangle inequality for tensorL2Dist.