Bounds and norm facts for dependent tensors.

The lemmas here support proof developments that need componentwise bounds, norm estimates, and simple inequalities over tensor-shaped data.

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

Sum distributes over elementwise addition.

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

Dot product properties. Essential for gradient computations and neural network training.

theorem Spec.dot_add_left {s : Shape} (a b c : 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 : Tensor ℝ s) (k : ℝ) : dot (a.scaleSpec k) b = k * dot a b

Scaling a tensor scales its dot-product: dot (scale_spec a k) b = k * dot a b.

Flatten / unflatten round-trips

The round-trip lemmas for the spec definitions live with the definitions themselves: NN/Spec/Core/TensorReductionShape.lean provides

• Spec.Tensor.flatten_unflatten_inverse
• Spec.Tensor.unflatten_flatten_inverse

so downstream proof files do not need to re-prove the index arithmetic here.

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

Size preservation under operations. Essential for proving tensor operations maintain expected dimensions.

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

Size preservation for mul_spec: elementwise multiplication does not change shape size.

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

Existence of a uniform bound for safediv_spec, expressed via an idempotent min-clamp.

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

Tensor norm properties. Essential for regularization and optimization proofs.

theorem Spec.tensor_norm_squared_nonneg {s : Shape} (t : Tensor ℝ s) : tensorNormSquared t ≥ 0

tensor_norm_squared t is nonnegative, since it is a sum of squares.

theorem Spec.tensor_norm_squared_nonneg2 {s : Shape} (t : Tensor ℝ s) : 0 ≤ tensorNormSquared t

Convenience orientation of tensor_norm_squared_nonneg.

Keep this untagged as a simp lemma: the canonical theorem above uses the existing >= spelling, while downstream analysis proofs often need the 0 ≤ ... spelling for Real.sq_sqrt.

theorem Spec.tensor_norm_squared_zero_iff {s : Shape} (t : Tensor ℝ s) : tensorNormSquared t = 0 ↔ t = fill 0 s

tensor_norm_squared t = 0 iff t is the all-zero tensor.

Extensionality and structural algebra