Vectorization

Shared Euclidean-space vectorization utilities for analytic autograd proofs.

This module centralizes the Vec alias (EuclideanSpace ℝ (Fin n)) and the basic Tensor ℝ (.dim n .scalar) ↔ Vec n conversions used across multiple proof files.

PyTorch correspondence / citations

This plays the same role as treating a length-n tensor as an element of ℝ^n when using standard analysis results (mean value theorem, operator norms, etc.). https://pytorch.org/docs/stable/linalg.html

@[reducible, inline]

abbrev Proofs.Autograd.Vec (n : ℕ) : Type

Euclidean vectors over ℝ.

noncomputable def Proofs.Autograd.toVecE {n : ℕ} (t : Spec.Tensor ℝ (Spec.Shape.dim n Spec.Shape.scalar)) : Vec n

Convert a 1D scalar tensor (Tensor ℝ (.dim n .scalar)) into a Euclidean vector Vec n.

This is the “analysis-friendly” view of a length-n tensor as an element of ℝ^n.

noncomputable def Proofs.Autograd.ofVecE {n : ℕ} (v : Vec n) : Spec.Tensor ℝ (Spec.Shape.dim n Spec.Shape.scalar)

Convert a Euclidean vector Vec n back into a 1D scalar tensor (Tensor ℝ (.dim n .scalar)).

This is the inverse direction of toVecE.

@[simp]

theorem Proofs.Autograd.toVecE_ofVecE {n : ℕ} (v : Vec n) : toVecE (ofVecE v) = v

toVecE is a left inverse of ofVecE.

@[simp]

theorem Proofs.Autograd.ofVecE_toVecE {n : ℕ} (t : Spec.Tensor ℝ (Spec.Shape.dim n Spec.Shape.scalar)) : ofVecE (toVecE t) = t

ofVecE is a left inverse of toVecE.

theorem Proofs.Autograd.inner_eq_sum_mul {n : ℕ} (x y : Vec n) : inner ℝ x y = ∑ i : Fin n, x.ofLp i * y.ofLp i

Coordinate formula for the Euclidean inner product on Vec n.

This is the statement “⟪x,y⟫ = ∑ᵢ xᵢ*yᵢ” specialized to EuclideanSpace ℝ (Fin n).