Derivatives of tensor coordinate maps

Slicing, gathering, and broadcasting all read input coordinates through a fixed map. The map need not be injective: repeated reads are precisely why the reverse pass must sum contributions.

These statements use Rep.pull, the coordinate kernel underlying the tensor representation, and the existing Euclidean topology on real tensors. A derivative is therefore stated on the actual tensor type. The coordinate formulas also apply to empty shapes; there is no chosen first element or hidden positivity assumption.

def Proofs.Autograd.Reindex.pullCLM {source target : Spec.Shape} (index : target.Coord → source.Coord) : TorchLean.Tensor ℝ source →L[ℝ] TorchLean.Tensor ℝ target

The native coordinate pullback, bundled as a continuous linear map.

@[simp]

theorem Proofs.Autograd.Reindex.pullCLM_apply {source target : Spec.Shape} (index : target.Coord → source.Coord) (x : TorchLean.Tensor ℝ source) : (pullCLM index) x = TorchLean.Tensor.Internal.Rep.pull index x

The bundled map reads exactly the coordinates selected by the native kernel.

theorem Proofs.Autograd.Reindex.hasFDerivAt_pull {source target : Spec.Shape} (index : target.Coord → source.Coord) (x : TorchLean.Tensor ℝ source) : HasFDerivAt (TorchLean.Tensor.Internal.Rep.pull index) (pullCLM index) x

Reindexing is linear, so the same coordinate map acts on every input tangent.

def Proofs.Autograd.Reindex.sumFibers {source target : Spec.Shape} (index : target.Coord → source.Coord) (gradient : TorchLean.Tensor ℝ target) : TorchLean.Tensor ℝ source

A source coordinate receives the sum over all output coordinates which read it.

There is deliberately no distinctness hypothesis on index. For a gather with repeated indices, every occurrence contributes; for a broadcast, every replicated batch contributes.

theorem Proofs.Autograd.Reindex.inner_pull_sumFibers {source target : Spec.Shape} (index : target.Coord → source.Coord) (x : TorchLean.Tensor ℝ source) (gradient : TorchLean.Tensor ℝ target) : inner ℝ (TorchLean.Tensor.Internal.Rep.pull index x) gradient = inner ℝ x (sumFibers index gradient)

Coordinate pullback and summation over its fibers are adjoint.

theorem Proofs.Autograd.Reindex.pullCLM_adjoint {source target : Spec.Shape} (index : target.Coord → source.Coord) (gradient : TorchLean.Tensor ℝ target) : (ContinuousLinearMap.adjoint (pullCLM index)) gradient = sumFibers index gradient

The analytic adjoint is the concrete accumulation formula, not an unspecified reduction.

theorem Proofs.Autograd.Reindex.dot_eq_inner {shape : Spec.Shape} (x y : TorchLean.Tensor ℝ shape) : Spec.dot x y = inner ℝ x y

The real spec dot product uses the same inner product as tensor Fréchet derivatives.

theorem Proofs.Autograd.Reindex.inner_eq_sum_unstack {n : ℕ} {shape : Spec.Shape} (x y : TorchLean.Tensor ℝ (Spec.Shape.dim n shape)) : inner ℝ x y = ∑ i : Fin n, inner ℝ (x.unstack i) (y.unstack i)

The Euclidean inner product separates over the leading tensor axis.