Convolution Specifications

This file defines channels-first convolution and transpose convolution over an arbitrary spatial rank. The core specification handles one sample; batched interfaces map it over their leading dimensions.

PyTorch analogy: the grouped, dilated core corresponds to torch.nn.Conv{d}d with:

• arbitrary positive groups,
• per-axis dilation and stride,
• independent zero padding before and after each spatial axis,
• and the usual output-size formula (floor division, like PyTorch):

For each axis a : Fin d:

out[a] = (in[a] + padBefore[a] + padAfter[a] - (dilation[a]*(kernel[a]-1) + 1)) / stride[a] + 1

(Shape.slidingWindowOutDimDilated), and 0 when the padded input is shorter than the dilated kernel extent. Unlike PyTorch, a dilation of 0 is accepted and gives kernel extent 1.

The weight tensor has shape (outC × inC × kernel[0] × ... × kernel[d-1]) and the bias has shape (outC).

Implementation notes:

• Convolution uses natural nested loops (outer axes first) and one foldl accumulator. This fixes an explicit evaluation order for executable scalar models.
• Padding semantics are implemented via getAtOrZero plus an explicit guard for the left/top/front padding region (to avoid negative indices, which Nat cannot represent).

Index helpers

def Spec.Conv.Internal.foldlIndices {β : Type} (dims : List ℕ) (init : β) (f : β → List ℕ → β) : β

Fold over every coordinate of the rectangular index box dims.

Convolution sums over a kernel whose rank is a variable, so the sum is a fold over a list of extents rather than nested Fin loops. Pooling windows use the same fold. Coordinates are visited in row-major order.

def Spec.Conv.Internal.mkInputIdx? (outIdx kIdx stride padding : List ℕ) : Option (List ℕ)

Given:

• an output index tuple outIdx,
• a kernel index tuple kIdx,
• per-axis stride and padding, compute the corresponding input index tuple (into the unpadded input), or return none if we are in the left/top/front padding region on some axis.

Right/bottom/back padding is handled by getAtOrZero when the computed index is out of bounds.

def Spec.Conv.Internal.mkDilatedInputIdx? (outIdx kIdx stride dilation paddingBefore : List ℕ) : Option (List ℕ)

Convolution input-index map with per-axis dilation.

theorem Spec.Conv.Internal.mkDilatedInputIdx?_replicate_one (outIdx kernelIdx stride padding : List ℕ) : mkDilatedInputIdx? outIdx kernelIdx stride (List.replicate stride.length 1) padding = mkInputIdx? outIdx kernelIdx stride padding

Unit dilation reduces the dilated convolution index map to the dense index map.

def Spec.Conv.Internal.mkTransposeInputIdx? (outIdx kIdx stride padding : List ℕ) : Option (List ℕ)

Given:

• an output index tuple outIdx,
• a kernel index tuple kIdx,
• per-axis stride and padding, compute the corresponding input index tuple for transpose convolution, or none if the equality out + padding = in * stride + k cannot be satisfied on some axis.

Implementation detail: for each axis we solve

in = (out + padding - k) / stride

and require divisibility (% stride = 0) plus out + padding ≥ k. Out-of-bounds input indices are handled by getAtOrZero at the call site.

Spec definition

structure Spec.ConvSpec (d inC outC : ℕ) (kernel stride padding : TorchLean.Tensor ℕ [d]) (α : Type) [TorchLean.Storage α] : Type

Parameters for an arbitrary-rank dense convolution, in channels-first layout.

• kernel : TorchLean.Tensor α (Shape.ofList (outC :: inC :: (TorchLean.Tensor.Internal.Rep.data kernel).toList))

  Kernel weights, shape (outC, inC, kernel[0], ..., kernel[d-1]).

• bias : TorchLean.Tensor α [outC]

  Bias, shape (outC).

def Spec.convOutSpatialDilated {d : ℕ} (inSpatial kernel stride dilation paddingBefore paddingAfter : TorchLean.Tensor ℕ [d]) : TorchLean.Tensor ℕ [d]

Output spatial sizes for grouped/dilated convolution with asymmetric zero padding.

def Spec.convOutSpatial {d : ℕ} (inSpatial kernel stride padding : TorchLean.Tensor ℕ [d]) : TorchLean.Tensor ℕ [d]

Output spatial sizes, one extent for each spatial axis.

@[simp]

theorem Spec.convOutSpatialDilated_one_symmetric {d : ℕ} (input kernel stride padding : TorchLean.Tensor ℕ [d]) : convOutSpatialDilated input kernel stride (TorchLean.Tensor.full [d] 1) padding padding = convOutSpatial input kernel stride padding

Dilated convolution geometry reduces to the symmetric, unit-dilation case.

theorem Spec.convOutSpatial_unit {d : ℕ} (spatial : TorchLean.Tensor ℕ [d]) : convOutSpatial spatial (TorchLean.Tensor.full [d] 1) (TorchLean.Tensor.full [d] 1) (TorchLean.Tensor.full [d] 0) = spatial

A unit kernel with unit stride and no padding preserves every spatial extent.

theorem Spec.convOutSpatial_same {d : ℕ} (spatial radius : TorchLean.Tensor ℕ [d]) : convOutSpatial spatial (TorchLean.Tensor.map (fun (p : ℕ) => 2 * p + 1) radius) (TorchLean.Tensor.full [d] 1) radius = spatial

Unit-stride convolution with an odd kernel and padding equal to the kernel radius preserves every spatial extent.

def Spec.convOutShape {d : ℕ} (inSpatial kernel stride padding : TorchLean.Tensor ℕ [d]) : Shape

Output spatial shape Shape.ofList [out0, ..., out(d-1)].

def Spec.Conv.Internal.convCoreWith {α : Type} [TorchLean.Storage α] [Context α] {d inC outC weightC : ℕ} {kernel inSpatial outSpatial : TorchLean.Tensor ℕ [d]} (channelsPerOutput : ℕ) (inputChannel : Fin outC → Fin channelsPerOutput → ℕ) (inputIndex? : List ℕ → List ℕ → Option (List ℕ)) (weights : TorchLean.Tensor α (Shape.ofList (outC :: weightC :: (TorchLean.Tensor.Internal.Rep.data kernel).toList))) (input : TorchLean.Tensor α (Shape.ofList (inC :: (TorchLean.Tensor.Internal.Rep.data inSpatial).toList))) (weightChannel : Fin outC → Fin channelsPerOutput → ℕ := inputChannel) : TorchLean.Tensor α (Shape.ofList (outC :: (TorchLean.Tensor.Internal.Rep.data outSpatial).toList))

The bilinear contraction shared by arbitrary-rank convolutions.

inputChannel selects the input channel. weightChannel selects the corresponding weight channel; it defaults to the input channel for dense weights, while packed grouped weights use the local channel index. Both layouts keep the same channel and spatial accumulation order.

def Spec.groupedConvCoreSpec {α : Type} [TorchLean.Storage α] [Context α] {d inC outC : ℕ} {kernel stride dilation paddingBefore paddingAfter inSpatial : TorchLean.Tensor ℕ [d]} (groups : ℕ) (weights : TorchLean.Tensor α (Shape.ofList (outC :: inC :: (TorchLean.Tensor.Internal.Rep.data kernel).toList))) (input : TorchLean.Tensor α (Shape.ofList (inC :: (TorchLean.Tensor.Internal.Rep.data inSpatial).toList))) : TorchLean.Tensor α (Shape.ofList (outC :: (TorchLean.Tensor.Internal.Rep.data (convOutSpatialDilated inSpatial kernel stride dilation paddingBefore paddingAfter)).toList))

The grouped, dilated contraction for an arbitrary-rank convolution, with weights in the block-diagonal dense layout (outC, inC, k...).

Output channel oc belongs to group oc / (outC / groups) and reads only the input channels of that group, so only the block-diagonal part of weights is ever consulted. PyTorch stores grouped weights packed as (outC, inC / groups, k...); use groupedConvPackedCoreSpec for that layout, or groupedConvDenseWeights to expand a packed tensor into this one.

The standard grouped-convolution interpretation requires groups > 0, groups ∣ inC, and groups ∣ outC. Outside those conditions the definition retains natural-number division and zero-filled out-of-range reads. Trailing channels can be read: with inC = outC = 5 and groups = 2, output channel 4 reads input channel 4. groups = 0 reads no channels.

def Spec.groupedConvPackedCoreSpec {α : Type} [TorchLean.Storage α] [Context α] {d inC outC : ℕ} {kernel stride dilation paddingBefore paddingAfter inSpatial : TorchLean.Tensor ℕ [d]} (groups : ℕ) (weights : TorchLean.Tensor α (Shape.ofList (outC :: inC / groups :: (TorchLean.Tensor.Internal.Rep.data kernel).toList))) (input : TorchLean.Tensor α (Shape.ofList (inC :: (TorchLean.Tensor.Internal.Rep.data inSpatial).toList))) : TorchLean.Tensor α (Shape.ofList (outC :: (TorchLean.Tensor.Internal.Rep.data (convOutSpatialDilated inSpatial kernel stride dilation paddingBefore paddingAfter)).toList))

The grouped, dilated contraction with weights in PyTorch's packed layout (outC, inC / groups, k...), which is how torch.nn.Conv{1,2,3}d(groups=g).weight is stored.

Output channel oc belongs to group g = oc / (outC / groups) and reads input channels g * (inC / groups) + j for j < inC / groups, weighting each by weights[oc, j, k...].

The standard grouped-convolution interpretation requires groups > 0 and divisibility of both channel counts. Other configurations retain natural-number division and zero-filled out-of-range reads; they need not omit the trailing channels (for example, inC = outC = 5, groups = 2). With groups = 0 the contraction is zero; the affine spec still performs its addition of the bias.

def Spec.groupedConvDenseWeights {α : Type} [TorchLean.Storage α] [Context α] {d inC outC : ℕ} {kernel : TorchLean.Tensor ℕ [d]} (groups : ℕ) (weights : TorchLean.Tensor α (Shape.ofList (outC :: inC / groups :: (TorchLean.Tensor.Internal.Rep.data kernel).toList))) : TorchLean.Tensor α (Shape.ofList (outC :: inC :: (TorchLean.Tensor.Internal.Rep.data kernel).toList))

Expand packed grouped weights (outC, inC / groups, k...) into the block-diagonal dense layout (outC, inC, k...) read by groupedConvCoreSpec and groupedConvSpec.

Entry [oc, ic, k...] is weights[oc, ic - g * (inC / groups), k...] when input channel ic lies in the group g of output channel oc, and 0 otherwise. This is the remap a PyTorch checkpoint needs before it can be fed to the dense-layout grouped convolution.

def Spec.convCoreSpec {α : Type} [TorchLean.Storage α] [Context α] {d inC outC : ℕ} {kernel stride padding inSpatial : TorchLean.Tensor ℕ [d]} (weights : TorchLean.Tensor α (Shape.ofList (outC :: inC :: (TorchLean.Tensor.Internal.Rep.data kernel).toList))) (input : TorchLean.Tensor α (Shape.ofList (inC :: (TorchLean.Tensor.Internal.Rep.data inSpatial).toList))) : TorchLean.Tensor α (Shape.ofList (outC :: (TorchLean.Tensor.Internal.Rep.data (convOutSpatial inSpatial kernel stride padding)).toList))

The bilinear kernel/input contraction underlying an arbitrary-rank dense convolution.

theorem Spec.castShape_groupedConvCoreSpec_one_symmetric {α : Type} [TorchLean.Storage α] [Context α] {d inC outC : ℕ} {kernel stride padding inSpatial : TorchLean.Tensor ℕ [d]} (weights : TorchLean.Tensor α (Shape.ofList (outC :: inC :: (TorchLean.Tensor.Internal.Rep.data kernel).toList))) (input : TorchLean.Tensor α (Shape.ofList (inC :: (TorchLean.Tensor.Internal.Rep.data inSpatial).toList))) : (groupedConvCoreSpec 1 weights input).castShape ⋯ = convCoreSpec weights input

The grouped convolution contraction reduces to dense convolution for one group, unit dilation, and symmetric padding. The explicit cast transports the dilated output shape across the geometric specialization theorem.

def Spec.Conv.Internal.convBiasBroadcastWith {α : Type} [TorchLean.Storage α] [Context α] {d outC : ℕ} (outSpatial : TorchLean.Tensor ℕ [d]) (bias : TorchLean.Tensor α [outC]) : TorchLean.Tensor α (Shape.ofList (outC :: (TorchLean.Tensor.Internal.Rep.data outSpatial).toList))

Broadcast one channel value over a supplied spatial shape.

def Spec.convBiasBroadcastSpec {α : Type} [TorchLean.Storage α] [Context α] {d outC : ℕ} {kernel stride padding inSpatial : TorchLean.Tensor ℕ [d]} (bias : TorchLean.Tensor α [outC]) : TorchLean.Tensor α (Shape.ofList (outC :: (TorchLean.Tensor.Internal.Rep.data (convOutSpatial inSpatial kernel stride padding)).toList))

Broadcast a convolution bias over every output spatial position.

def Spec.convBiasBroadcastDilatedSpec {α : Type} [TorchLean.Storage α] [Context α] {d outC : ℕ} {kernel stride dilation paddingBefore paddingAfter inSpatial : TorchLean.Tensor ℕ [d]} (bias : TorchLean.Tensor α [outC]) : TorchLean.Tensor α (Shape.ofList (outC :: (TorchLean.Tensor.Internal.Rep.data (convOutSpatialDilated inSpatial kernel stride dilation paddingBefore paddingAfter)).toList))

Add a channel bias to a dilated convolution output.

theorem Spec.castShape_convBiasBroadcastDilatedSpec_one_symmetric {α : Type} [TorchLean.Storage α] [Context α] {d outC : ℕ} {kernel stride padding inSpatial : TorchLean.Tensor ℕ [d]} (bias : TorchLean.Tensor α [outC]) : (convBiasBroadcastDilatedSpec bias).castShape ⋯ = convBiasBroadcastSpec bias

Dilated-output bias broadcasting reduces to dense bias broadcasting in the symmetric case.

def Spec.groupedConvSpec {α : Type} [TorchLean.Storage α] [Context α] {d inC outC : ℕ} {kernel stride dilation paddingBefore paddingAfter inSpatial : TorchLean.Tensor ℕ [d]} (groups : ℕ) (weights : TorchLean.Tensor α (Shape.ofList (outC :: inC :: (TorchLean.Tensor.Internal.Rep.data kernel).toList))) (bias : TorchLean.Tensor α [outC]) (input : TorchLean.Tensor α (Shape.ofList (inC :: (TorchLean.Tensor.Internal.Rep.data inSpatial).toList))) : TorchLean.Tensor α (Shape.ofList (outC :: (TorchLean.Tensor.Internal.Rep.data (convOutSpatialDilated inSpatial kernel stride dilation paddingBefore paddingAfter)).toList))

Numerical semantics for grouped, dilated convolution with asymmetric zero padding, with weights in the block-diagonal dense layout (outC, inC, k...).

This is the entry point used by the IR evaluator and the lowering passes, whose payloads carry a dense ConvSpec kernel. PyTorch checkpoints store grouped weights packed as (outC, inC / groups, k...); either expand them with groupedConvDenseWeights or use groupedConvPackedSpec directly. Both forms assume groups ∣ inC and groups ∣ outC.

def Spec.groupedConvPackedSpec {α : Type} [TorchLean.Storage α] [Context α] {d inC outC : ℕ} {kernel stride dilation paddingBefore paddingAfter inSpatial : TorchLean.Tensor ℕ [d]} (groups : ℕ) (weights : TorchLean.Tensor α (Shape.ofList (outC :: inC / groups :: (TorchLean.Tensor.Internal.Rep.data kernel).toList))) (bias : TorchLean.Tensor α [outC]) (input : TorchLean.Tensor α (Shape.ofList (inC :: (TorchLean.Tensor.Internal.Rep.data inSpatial).toList))) : TorchLean.Tensor α (Shape.ofList (outC :: (TorchLean.Tensor.Internal.Rep.data (convOutSpatialDilated inSpatial kernel stride dilation paddingBefore paddingAfter)).toList))

Grouped, dilated convolution with asymmetric zero padding and PyTorch's packed weight layout (outC, inC / groups, k...).

PyTorch analogue: torch.nn.functional.conv{1,2,3}d(input, weight, bias, stride, padding, dilation, groups) on one unbatched sample, with weight used as stored. The divisibility requirement groups ∣ inC ∧ groups ∣ outC is documented on groupedConvPackedCoreSpec.

def Spec.convSpec {α : Type} [TorchLean.Storage α] [Context α] {d inC outC : ℕ} {kernel stride padding inSpatial : TorchLean.Tensor ℕ [d]} (layer : ConvSpec d inC outC kernel stride padding α) (input : TorchLean.Tensor α (Shape.ofList (inC :: (TorchLean.Tensor.Internal.Rep.data inSpatial).toList))) : TorchLean.Tensor α (Shape.ofList (outC :: (TorchLean.Tensor.Internal.Rep.data (convOutSpatial inSpatial kernel stride padding)).toList))

Arbitrary-rank dense convolution on a single channels-first input (no batch dimension).

Mathematically, for output channel oc and output spatial index o : Tensor Nat [d]:

y[oc,o] = Σ_{ic, k} x_pad[ic, o*stride + k] * W[oc,ic,k] + b[oc]

where k ranges over the kernel window and x_pad is input with zero-padding.

theorem Spec.castShape_groupedConvSpec_one_symmetric {α : Type} [TorchLean.Storage α] [Context α] {d inC outC : ℕ} {kernel stride padding inSpatial : TorchLean.Tensor ℕ [d]} (weights : TorchLean.Tensor α (Shape.ofList (outC :: inC :: (TorchLean.Tensor.Internal.Rep.data kernel).toList))) (bias : TorchLean.Tensor α [outC]) (input : TorchLean.Tensor α (Shape.ofList (inC :: (TorchLean.Tensor.Internal.Rep.data inSpatial).toList))) : (groupedConvSpec 1 weights bias input).castShape ⋯ = convSpec { kernel := weights, bias := bias } input

Grouped convolution reduces to dense convolution for its canonical dense configuration.

def Spec.convJvpSpec {α : Type} [TorchLean.Storage α] [Context α] {d inC outC : ℕ} {kernel stride padding inSpatial : TorchLean.Tensor ℕ [d]} (layer tangentLayer : ConvSpec d inC outC kernel stride padding α) (input tangentInput : TorchLean.Tensor α (Shape.ofList (inC :: (TorchLean.Tensor.Internal.Rep.data inSpatial).toList))) : TorchLean.Tensor α (Shape.ofList (outC :: (TorchLean.Tensor.Internal.Rep.data (convOutSpatial inSpatial kernel stride padding)).toList))

Directional derivative formula for convolution in its kernel, bias, and input arguments.

def Spec.convKernelDerivSpec {α : Type} [TorchLean.Storage α] [Context α] {d inC outC : ℕ} {kernel stride padding inSpatial : TorchLean.Tensor ℕ [d]} (_layer : ConvSpec d inC outC kernel stride padding α) (input : TorchLean.Tensor α (Shape.ofList (inC :: (TorchLean.Tensor.Internal.Rep.data inSpatial).toList))) (gradOutput : TorchLean.Tensor α (Shape.ofList (outC :: (TorchLean.Tensor.Internal.Rep.data (convOutSpatial inSpatial kernel stride padding)).toList))) : TorchLean.Tensor α (Shape.ofList (outC :: inC :: (TorchLean.Tensor.Internal.Rep.data kernel).toList))

Gradient of convolution output w.r.t. the kernel weights (given gradOutput).

def Spec.convBiasDerivSpec {α : Type} [TorchLean.Storage α] [Context α] {d inC outC : ℕ} {kernel stride padding inSpatial : TorchLean.Tensor ℕ [d]} (_layer : ConvSpec d inC outC kernel stride padding α) (_input : TorchLean.Tensor α (Shape.ofList (inC :: (TorchLean.Tensor.Internal.Rep.data inSpatial).toList))) (gradOutput : TorchLean.Tensor α (Shape.ofList (outC :: (TorchLean.Tensor.Internal.Rep.data (convOutSpatial inSpatial kernel stride padding)).toList))) : TorchLean.Tensor α [outC]

Gradient of convolution output w.r.t. the bias (sum over spatial positions).

def Spec.convInputDerivSpec {α : Type} [TorchLean.Storage α] [Context α] {d inC outC : ℕ} {kernel stride padding inSpatial : TorchLean.Tensor ℕ [d]} (layer : ConvSpec d inC outC kernel stride padding α) (_input : TorchLean.Tensor α (Shape.ofList (inC :: (TorchLean.Tensor.Internal.Rep.data inSpatial).toList))) (gradOutput : TorchLean.Tensor α (Shape.ofList (outC :: (TorchLean.Tensor.Internal.Rep.data (convOutSpatial inSpatial kernel stride padding)).toList))) : TorchLean.Tensor α (Shape.ofList (inC :: (TorchLean.Tensor.Internal.Rep.data inSpatial).toList))

Gradient of convolution output w.r.t. the input (the "input-gradient" / transpose-convolution map).

This is stated once for arbitrary spatial rank d; there are no rank-specific variants.

structure Spec.ConvGradients (α : Type) [TorchLean.Storage α] (kernelShape biasShape inputShape : Shape) : Type

Named reverse-mode result of a convolution.

The kernel, bias, and input gradients retain their respective tensor shapes. Named fields identify the three contributions in the backward pass and its adjoint theorem.

• kernelGradient : TorchLean.Tensor α kernelShape

  Gradient with respect to the kernel weights.

• biasGradient : TorchLean.Tensor α biasShape

  Gradient with respect to the per-output-channel bias.

• inputGradient : TorchLean.Tensor α inputShape

  Gradient with respect to the layer input.

@[instance_reducible]

instance Spec.instReprConvGradients {α✝ : Type} {inst✝ : TorchLean.Storage α✝} {kernelShape✝ biasShape✝ inputShape✝ : Shape} [Repr α✝] : Repr (ConvGradients α✝ kernelShape✝ biasShape✝ inputShape✝)

def Spec.instReprConvGradients.repr {α✝ : Type} {inst✝ : TorchLean.Storage α✝} {kernelShape✝ biasShape✝ inputShape✝ : Shape} [Repr α✝] : ConvGradients α✝ kernelShape✝ biasShape✝ inputShape✝ → ℕ → Std.Format

def Spec.convBackwardSpec {α : Type} [TorchLean.Storage α] [Context α] {d inC outC : ℕ} {kernel stride padding inSpatial : TorchLean.Tensor ℕ [d]} (layer : ConvSpec d inC outC kernel stride padding α) (input : TorchLean.Tensor α (Shape.ofList (inC :: (TorchLean.Tensor.Internal.Rep.data inSpatial).toList))) (gradOutput : TorchLean.Tensor α (Shape.ofList (outC :: (TorchLean.Tensor.Internal.Rep.data (convOutSpatial inSpatial kernel stride padding)).toList))) : ConvGradients α (Shape.ofList (outC :: inC :: (TorchLean.Tensor.Internal.Rep.data kernel).toList)) [outC] (Shape.ofList (inC :: (TorchLean.Tensor.Internal.Rep.data inSpatial).toList))

Convolution backward pass: the kernel, bias, and input gradients under their own names.

Transpose convolution

structure Spec.ConvTransposeSpec (d inC outC : ℕ) (kernel stride padding : TorchLean.Tensor ℕ [d]) (α : Type) [TorchLean.Storage α] : Type

Parameters for an arbitrary-rank transpose convolution, in channels-first layout.

PyTorch analogy: this is torch.nn.ConvTranspose{d}d with:

• output_padding = 0,
• dilation = 1,
• groups = 1,
• per-axis stride and padding,
• and weight layout (inC, outC, k0, ..., k(d-1)).

• kernel : TorchLean.Tensor α (Shape.ofList (inC :: outC :: (TorchLean.Tensor.Internal.Rep.data kernel).toList))

  Kernel weights, shape (inC, outC, kernel[0], ..., kernel[d-1]).

• bias : TorchLean.Tensor α [outC]

  Bias, shape (outC).

def Spec.convTransposeOutDim (inDim kDim stride padding : ℕ) : ℕ

Output size along one transpose-convolution axis with output_padding = 0.

For positive input, kernel, and stride this is (input - 1) * stride + kernel - 2 * padding. A zero input, kernel, or stride is treated as an invalid axis and has size zero; excessive padding also saturates the final subtraction at zero. The addition precedes subtraction intentionally: Nat subtraction in (input - 1) * stride - 2 * padding + kernel does not represent the integer formula.

def Spec.convTransposeOutSpatial {d : ℕ} (inSpatial kernel stride padding : TorchLean.Tensor ℕ [d]) : TorchLean.Tensor ℕ [d]

Output spatial sizes (Tensor Nat [d]) for transpose convolution (output_padding = 0).

def Spec.convTransposeSpec {α : Type} [TorchLean.Storage α] [Context α] {d inC outC : ℕ} {kernel stride padding inSpatial : TorchLean.Tensor ℕ [d]} (layer : ConvTransposeSpec d inC outC kernel stride padding α) (input : TorchLean.Tensor α (Shape.ofList (inC :: (TorchLean.Tensor.Internal.Rep.data inSpatial).toList))) : TorchLean.Tensor α (Shape.ofList (outC :: (TorchLean.Tensor.Internal.Rep.data (convTransposeOutSpatial inSpatial kernel stride padding)).toList))

Arbitrary-rank transpose convolution on a single channels-first input (no batch dimension).

For output channel oc and output spatial index o : Tensor Nat [d] we define:

y[oc,o] = Σ_{ic, k} x[ic, (o + padding - k) / stride] * W[ic,oc,k] + b[oc]

where each axis must satisfy out + padding ≥ k and divisibility by stride (% stride = 0).

def Spec.convTransposeKernelDerivSpec {α : Type} [TorchLean.Storage α] [Context α] {d inC outC : ℕ} {kernel stride padding inSpatial : TorchLean.Tensor ℕ [d]} (input : TorchLean.Tensor α (Shape.ofList (inC :: (TorchLean.Tensor.Internal.Rep.data inSpatial).toList))) (gradOutput : TorchLean.Tensor α (Shape.ofList (outC :: (TorchLean.Tensor.Internal.Rep.data (convTransposeOutSpatial inSpatial kernel stride padding)).toList))) : TorchLean.Tensor α (Shape.ofList (inC :: outC :: (TorchLean.Tensor.Internal.Rep.data kernel).toList))

Gradient of transpose convolution output w.r.t. the kernel weights (given gradOutput).

def Spec.convTransposeBiasDerivSpec {α : Type} [TorchLean.Storage α] [Context α] {d outC : ℕ} {kernel stride padding inSpatial : TorchLean.Tensor ℕ [d]} (gradOutput : TorchLean.Tensor α (Shape.ofList (outC :: (TorchLean.Tensor.Internal.Rep.data (convTransposeOutSpatial inSpatial kernel stride padding)).toList))) : TorchLean.Tensor α [outC]

Gradient of transpose convolution output w.r.t. the bias (sum over spatial positions).

def Spec.convTransposeInputDerivSpec {α : Type} [TorchLean.Storage α] [Context α] {d inC outC : ℕ} {kernel stride padding inSpatial : TorchLean.Tensor ℕ [d]} (weights : TorchLean.Tensor α (Shape.ofList (inC :: outC :: (TorchLean.Tensor.Internal.Rep.data kernel).toList))) (gradOutput : TorchLean.Tensor α (Shape.ofList (outC :: (TorchLean.Tensor.Internal.Rep.data (convTransposeOutSpatial inSpatial kernel stride padding)).toList))) : TorchLean.Tensor α (Shape.ofList (inC :: (TorchLean.Tensor.Internal.Rep.data inSpatial).toList))

Gradient of transpose convolution output w.r.t. the input (given gradOutput).

def Spec.convTransposeBackwardSpec {α : Type} [TorchLean.Storage α] [Context α] {d inC outC : ℕ} {kernel stride padding inSpatial : TorchLean.Tensor ℕ [d]} (layer : ConvTransposeSpec d inC outC kernel stride padding α) (input : TorchLean.Tensor α (Shape.ofList (inC :: (TorchLean.Tensor.Internal.Rep.data inSpatial).toList))) (gradOutput : TorchLean.Tensor α (Shape.ofList (outC :: (TorchLean.Tensor.Internal.Rep.data (convTransposeOutSpatial inSpatial kernel stride padding)).toList))) : ConvGradients α (Shape.ofList (inC :: outC :: (TorchLean.Tensor.Internal.Rep.data kernel).toList)) [outC] (Shape.ofList (inC :: (TorchLean.Tensor.Internal.Rep.data inSpatial).toList))

Transpose convolution backward pass, reported with the same named fields as the forward convolution's ConvGradients. Only the kernel layout differs: transpose weights are stored (inC, outC, ...).