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.

Shape preservation

theorem Spec.shape_size_add {s : Shape} (a b : TorchLean.Tensor ℝ s) : (shapeOf (a.addSpec b)).size = s.size

Elementwise addition does not change the statically tracked shape size.

theorem Spec.shape_size_mul {s : Shape} (a b : TorchLean.Tensor ℝ s) : (shapeOf (a.mulSpec b)).size = s.size

Elementwise multiplication does not change the statically tracked shape size.

Uniform finite bounds

theorem Spec.safediv_bound {s : Shape} (a b : TorchLean.Tensor ℝ s) (_i : Fin s.size) : Context.defaultEpsilon > 0 → ∃ (bound : ℝ), (a.safedivSpec b).absSpec = TorchLean.Tensor.mapSpec (fun (value : ℝ) => min value bound) (a.safedivSpec b).absSpec

A finite tensor admits a uniform bound, expressed by an idempotent minimum clamp.

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.