Vectorization

Shared Euclidean-space vectorization utilities for analytic autograd proofs.

This module centralizes the Vec alias (EuclideanSpace ℝ (Fin n)) and the basic Tensor ℝ [n] ↔ 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 $\mathbb R^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.getScalarE {n : ℕ} (t : TorchLean.Tensor ℝ [n]) : Vec n

Convert a rank-one tensor (Tensor ℝ [n]) into a Euclidean vector Vec n.

This is the “analysis-friendly” view of a length-n tensor as an element of $\mathbb R^n$.

@[simp]

theorem Proofs.Autograd.getScalarE_ofLp {n : ℕ} (t : TorchLean.Tensor ℝ [n]) (i : Fin n) : (getScalarE t).ofLp i = t.getScalar i

Coordinate evaluation of the Euclidean view of a rank-one tensor.

noncomputable def Proofs.Autograd.ofFnE {n : ℕ} (v : Vec n) : TorchLean.Tensor ℝ [n]

Convert a Euclidean vector Vec n back into a rank-one tensor (Tensor ℝ [n]).

This is the inverse direction of getScalarE.

@[simp]

theorem Proofs.Autograd.getScalarE_ofFnE {n : ℕ} (v : Vec n) : getScalarE (ofFnE v) = v

getScalarE is a left inverse of ofFnE.

@[simp]

theorem Proofs.Autograd.getScalar_ofFnE {n : ℕ} (v : Vec n) (i : Fin n) : (ofFnE v).getScalar i = v.ofLp i

Coordinate evaluation commutes with conversion from a Euclidean vector.

@[simp]

theorem Proofs.Autograd.ofFnE_getScalarE {n : ℕ} (t : TorchLean.Tensor ℝ [n]) : ofFnE (getScalarE t) = t

ofFnE is a left inverse of getScalarE.

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 $\langle x,y\rangle=\sum_i x_i y_i$ specialized to EuclideanSpace ℝ (Fin n).