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.vecOfFun {n : ℕ} (f : Fin n → ℝ) : Vec n

Build a Euclidean vector from its coordinate function.

Used by analytic derivatives and by vector reindexing across context concatenation and shape casts.

@[simp]

theorem Proofs.Autograd.vecOfFun_apply {n : ℕ} (f : Fin n → ℝ) (i : Fin n) : (vecOfFun f).ofLp i = f i

Coordinates of vecOfFun f are the values of f.

@[simp]

theorem Proofs.Autograd.vecOfFun_ofLp {n : ℕ} (f : Fin n → ℝ) (i : Fin n) : (vecOfFun f).ofLp i = f i

The same statement through the WithLp wrapper, which is the form simp meets in practice.

theorem Proofs.Autograd.vecOfFun_ofLp_eq {n : ℕ} (f : Fin n → ℝ) : (vecOfFun f).ofLp = f

Removing the WithLp wrapper from vecOfFun recovers its coordinate function.

@[simp]

theorem Proofs.Autograd.vecOfFun_eta {n : ℕ} (v : Vec n) : (vecOfFun fun (i : Fin n) => v.ofLp i) = v

Rebuilding a vector from its own coordinates changes nothing.

@[simp]

theorem Proofs.Autograd.vecOfFun_eta_ofLp {n : ℕ} (v : Vec n) : (vecOfFun fun (i : Fin n) => v.ofLp i) = v

The ofLp variant of eta. Both directions are needed because reindexing lemmas sometimes produce a bare coordinate function and sometimes an unwrapped one.

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).