Convolution Index Arithmetic

The forward and transpose convolution loops describe the same integer relation from opposite directions. This file proves that relation once for an arbitrary list of spatial axes. The only geometric hypothesis is the standard one that every stride is positive.

Finite spatial indices

@[reducible, inline]

abbrev Spec.Conv.Internal.MultiIndex : List ℕ → Type

A shape-indexed spatial coordinate, represented without partial list indexing.

@[instance_reducible]

instance Spec.Conv.Internal.instFintypeMultiIndex (dims : List ℕ) : Fintype (MultiIndex dims)

@[instance_reducible]

instance Spec.Conv.Internal.instDecidableEqMultiIndex (dims : List ℕ) : DecidableEq (MultiIndex dims)

def Spec.Conv.Internal.MultiIndex.toList {dims : List ℕ} : MultiIndex dims → List ℕ

Convert a bounded spatial coordinate to the runtime list representation.

def Spec.Conv.Internal.MultiIndex.get {α : Type} [TorchLean.Storage α] {dims : List ℕ} : TorchLean.Tensor α (Shape.ofList dims) → MultiIndex dims → α

Read a tensor at a bounded spatial coordinate.

@[simp]

theorem Spec.Conv.Internal.MultiIndex.get_dim {α : Type} [TorchLean.Storage α] (n : ℕ) (dims : List ℕ) (values : Fin n → TorchLean.Tensor α (Shape.ofList dims)) (head : Fin n) (tail : MultiIndex dims) : get (TorchLean.Tensor.dim values) (head, tail) = get (values head) tail

Reading a dim tensor peels the leading coordinate and recurses into that slice.

@[simp]

theorem Spec.Conv.Internal.MultiIndex.get_vector_eq_getScalar {α : Type} [TorchLean.Storage α] {n : ℕ} (values : TorchLean.Tensor α [n]) (i : Fin n) : get values (i, PUnit.unit) = values.getScalar i

Reading the sole scalar coordinate below a vector index agrees with the vector view.

@[simp]

theorem Spec.Conv.Internal.getAtOrZero_dim_nil {α : Type} [TorchLean.Storage α] [Zero α] (n : ℕ) (dims : List ℕ) (values : Fin n → TorchLean.Tensor α (Shape.ofList dims)) : getAtOrZero (TorchLean.Tensor.dim values) [] = 0

An index that runs out too early reads zero.

theorem Spec.Conv.Internal.getAtOrZero_dim_cons {α : Type} [TorchLean.Storage α] [Zero α] (n : ℕ) (dims : List ℕ) (values : Fin n → TorchLean.Tensor α (Shape.ofList dims)) (j : ℕ) (js : List ℕ) : getAtOrZero (TorchLean.Tensor.dim values) (j :: js) = if h : j < n then getAtOrZero (values ⟨j, h⟩) js else 0

Otherwise the leading coordinate is bounds-checked and the lookup recurses, reading zero when it falls outside. This total lookup is what lets padding be expressed without a separate case split at every use site: an out-of-range index simply contributes nothing.

theorem Spec.Conv.Internal.MultiIndex.sum_cons {α : Type} [AddCommMonoid α] (n : ℕ) (dims : List ℕ) (f : MultiIndex (n :: dims) → α) : ∑ i : MultiIndex (n :: dims), f i = ∑ head : Fin n, ∑ tail : MultiIndex dims, f (head, tail)

Split a finite sum over a nonempty multi-index into its leading coordinate and tail.

@[simp]

theorem Spec.Conv.Internal.MultiIndex.get_generate {α : Type} [TorchLean.Storage α] (dims : List ℕ) (f : List ℕ → α) (i : MultiIndex dims) : get (TorchLean.Tensor.generate dims f) i = f i.toList

Reading a generated tensor applies the generating function to the index's coordinate list.

theorem Spec.Conv.Internal.MultiIndex.get_addSpec {α : Type} [TorchLean.Storage α] [Context α] {dims : List ℕ} (x y : TorchLean.Tensor α (Shape.ofList dims)) (i : MultiIndex dims) : get (x.addSpec y) i = get x i + get y i

Bounded-coordinate lookup commutes with pointwise tensor addition.

@[simp]

theorem Spec.Conv.Internal.getAtOrZero_toList {α : Type} [TorchLean.Storage α] [Zero α] (dims : List ℕ) (x : TorchLean.Tensor α (Shape.ofList dims)) (i : MultiIndex dims) : getAtOrZero x i.toList = MultiIndex.get x i

On an in-range index the total lookup agrees with the bounded one.

This is the lemma that connects the two indexing styles in the file: implementations use unbounded List Nat coordinates, specifications use MultiIndex, and inside the bounds they coincide.

theorem Spec.Conv.Internal.getAtOrZero_eq_sum_indicator {α : Type} [TorchLean.Storage α] [AddCommMonoid α] (dims : List ℕ) (x : TorchLean.Tensor α (Shape.ofList dims)) (indices : List ℕ) : getAtOrZero x indices = ∑ i : MultiIndex dims, if indices = i.toList then MultiIndex.get x i else 0

A total lookup is the finite coordinate sum selected by equality of index lists.

This formulation handles valid indices, padding, and malformed or out-of-range lists uniformly.

theorem Spec.Conv.Internal.foldlIndices_add {α : Type} [AddCommMonoid α] (dims : List ℕ) (init : α) (f : List ℕ → α) : (foldlIndices dims init fun (acc : α) (i : List ℕ) => acc + f i) = init + ∑ i : MultiIndex dims, f i.toList

The executable nested index fold is the finite sum over bounded coordinates.

theorem Spec.Conv.Internal.dot_eq_sum_get {α : Type} [TorchLean.Storage α] [CommSemiring α] (dims : List ℕ) (x y : TorchLean.Tensor α (Shape.ofList dims)) : Proofs.TensorAlgebra.dot x y = ∑ i : MultiIndex dims, MultiIndex.get x i * MultiIndex.get y i

Recursive tensor dot product as a finite sum over bounded multi-indices.

def Spec.Conv.Internal.PositiveStrides (stride : List ℕ) : Prop

Every stride in a runtime list is positive.

theorem Spec.Conv.Internal.mkTransposeInputIdx?_of_mkInputIdx?_eq_some {outIdx kIdx stride padding inIdx : List ℕ} (hStride : PositiveStrides stride) (hForward : mkInputIdx? outIdx kIdx stride padding = some inIdx) : mkTransposeInputIdx? inIdx kIdx stride padding = some outIdx

Solving a forward convolution index and then solving backwards recovers the output index.

theorem Spec.Conv.Internal.mkInputIdx?_of_mkTransposeInputIdx?_eq_some {inIdx kIdx stride padding outIdx : List ℕ} (hStride : PositiveStrides stride) (hTranspose : mkTransposeInputIdx? inIdx kIdx stride padding = some outIdx) : mkInputIdx? outIdx kIdx stride padding = some inIdx

Solving a transpose convolution index and then solving forwards recovers the input index.

theorem Spec.Conv.Internal.mkInputIdx?_eq_some_iff {outIdx kIdx stride padding inIdx : List ℕ} (hStride : PositiveStrides stride) : mkInputIdx? outIdx kIdx stride padding = some inIdx ↔ mkTransposeInputIdx? inIdx kIdx stride padding = some outIdx

The two index solvers define the same relation when strides are positive.