Bounds and norm facts for dependent tensors.

The proofs use coordinate extensionality and finite sums. They therefore describe the mathematical tensor independently of its packed physical storage.

theorem Spec.sum_spec_add_distrib {s : Shape} (a b : TorchLean.Tensor ℝ s) : (a.addSpec b).sumSpec = a.sumSpec + b.sumSpec

Sum distributes over elementwise addition.

theorem Spec.dot_comm {s : Shape} (a b : TorchLean.Tensor ℝ s) : dot a b = dot b a

The dot product is symmetric.

theorem Spec.dot_add_left {s : Shape} (a b c : TorchLean.Tensor ℝ s) : dot (a.addSpec b) c = dot a c + dot b c

Dot-product distributes over addition in the left argument.

theorem Spec.dot_scale_left {s : Shape} (a b : TorchLean.Tensor ℝ s) (k : ℝ) : dot (a.scaleSpec k) b = k * dot a b

Scaling a tensor scales its dot-product.

Squared norm

noncomputable def Spec.tensorNormSquared {s : Shape} (tensor : TorchLean.Tensor ℝ s) : ℝ

The squared Euclidean norm of all coordinates of a tensor.

theorem Spec.tensor_norm_squared_nonneg {s : Shape} (tensor : TorchLean.Tensor ℝ s) : 0 ≤ tensorNormSquared tensor

A tensor squared norm is nonnegative.

theorem Spec.tensor_norm_squared_zero_iff {s : Shape} (tensor : TorchLean.Tensor ℝ s) : tensorNormSquared tensor = 0 ↔ tensor = TorchLean.Tensor.full s 0

A tensor has zero squared norm exactly when every coordinate is zero.

theorem Spec.normalizeL2Regularized_eq {n : ℕ} (x : TorchLean.Tensor ℝ [n]) (epsilon : ℝ) (hepsilon : 0 < epsilon) (mean : Bool := false) : normalizeL2RegularizedSpec x epsilon mean = TorchLean.Tensor.map (fun (value : ℝ) => value / √((if mean = true then x.squareSpec.meanSpec else x.squareSpec.sumSpec) + epsilon)) x

Scaling the vector and epsilon together preserves the regularized real normalization. The same identity covers RMS normalization when mean is true.