Derivative of General Convolution

This file proves the derivative and reverse-mode formulas for channels-first convolution at an arbitrary spatial rank. All sums use bounded multi-indices; no axis count is fixed in a theorem. The forward coordinate map is bilinear in kernel and input. The input-gradient adjoint identity requires positive strides so the forward and transpose index relations agree. These are exact-real specification results; they do not establish correspondence with native LibTorch kernels.

def Proofs.Autograd.Conv.channelGet {α : Type} [TorchLean.Storage α] {channels : ℕ} {dims : List ℕ} (x : TorchLean.Tensor α (Spec.Shape.ofList (channels :: dims))) (channel : Fin channels) (i : Spec.Conv.Internal.MultiIndex dims) : α

Read a channel and bounded spatial coordinate from a channels-first tensor.

def Proofs.Autograd.Conv.channelPairGet {α : Type} [TorchLean.Storage α] {outer inner : ℕ} {dims : List ℕ} (x : TorchLean.Tensor α (Spec.Shape.ofList (outer :: inner :: dims))) (i : Fin outer) (j : Fin inner) (k : Spec.Conv.Internal.MultiIndex dims) : α

Read two leading channels followed by a bounded spatial coordinate.

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

Split a channels-first tensor dot product into channel and spatial sums.

theorem Proofs.Autograd.Conv.getAtOrZero_channel_eq_sum_indicator {α : Type} [TorchLean.Storage α] [AddCommMonoid α] {channels : ℕ} {dims : List ℕ} (x : TorchLean.Tensor α (Spec.Shape.ofList (channels :: dims))) (channel : Fin channels) (indices : List ℕ) : Spec.getAtOrZero x (↑channel :: indices) = ∑ i : Spec.Conv.Internal.MultiIndex dims, if indices = i.toList then channelGet x channel i else 0

Expand a channels-first lookup into the unique bounded spatial coordinate that it names.

def Proofs.Autograd.Conv.convCoefficient {d inC outC : ℕ} {kernel stride padding inSpatial : TorchLean.Tensor ℕ [d]} (weights : TorchLean.Tensor ℝ (Spec.Shape.ofList (outC :: inC :: kernel.to (List ℕ)))) (outCh : Fin outC) (outIdx : Spec.Conv.Internal.MultiIndex ((Spec.convOutSpatial inSpatial kernel stride padding).to (List ℕ))) (inCh : Fin inC) (inIdx : Spec.Conv.Internal.MultiIndex (inSpatial.to (List ℕ))) : ℝ

The scalar coefficient connecting one input coordinate to one output coordinate.

theorem Proofs.Autograd.Conv.channelGet_convCoreSpec {d inC outC : ℕ} {kernel stride padding inSpatial : TorchLean.Tensor ℕ [d]} (weights : TorchLean.Tensor ℝ (Spec.Shape.ofList (outC :: inC :: kernel.to (List ℕ)))) (input : TorchLean.Tensor ℝ (Spec.Shape.ofList (inC :: inSpatial.to (List ℕ)))) (outCh : Fin outC) (outIdx : Spec.Conv.Internal.MultiIndex ((Spec.convOutSpatial inSpatial kernel stride padding).to (List ℕ))) : channelGet (Spec.convCoreSpec weights input) outCh outIdx = ∑ inCh : Fin inC, ∑ kIdx : Spec.Conv.Internal.MultiIndex (kernel.to (List ℕ)), (match Spec.Conv.Internal.mkInputIdx? outIdx.toList kIdx.toList (stride.to (List ℕ)) (padding.to (List ℕ)) with | none => 0 | some inIdx => Spec.getAtOrZero input (↑inCh :: inIdx)) * channelPairGet weights outCh inCh kIdx

One coordinate of the generic convolution contraction, written as finite sums.

theorem Proofs.Autograd.Conv.channelGet_convCoreSpec_eq_coefficients {d inC outC : ℕ} {kernel stride padding inSpatial : TorchLean.Tensor ℕ [d]} (weights : TorchLean.Tensor ℝ (Spec.Shape.ofList (outC :: inC :: kernel.to (List ℕ)))) (input : TorchLean.Tensor ℝ (Spec.Shape.ofList (inC :: inSpatial.to (List ℕ)))) (outCh : Fin outC) (outIdx : Spec.Conv.Internal.MultiIndex ((Spec.convOutSpatial inSpatial kernel stride padding).to (List ℕ))) : channelGet (Spec.convCoreSpec weights input) outCh outIdx = ∑ inCh : Fin inC, ∑ inIdx : Spec.Conv.Internal.MultiIndex (inSpatial.to (List ℕ)), channelGet input inCh inIdx * convCoefficient weights outCh outIdx inCh inIdx

Convolution is the matrix represented by convCoefficient at every spatial rank.

theorem Proofs.Autograd.Conv.channelPairGet_convKernelDerivSpec {d inC outC : ℕ} {kernel stride padding inSpatial : TorchLean.Tensor ℕ [d]} (layer : Spec.ConvSpec d inC outC kernel stride padding ℝ) (input : TorchLean.Tensor ℝ (Spec.Shape.ofList (inC :: inSpatial.to (List ℕ)))) (gradOutput : TorchLean.Tensor ℝ (Spec.Shape.ofList (outC :: (Spec.convOutSpatial inSpatial kernel stride padding).to (List ℕ)))) (outCh : Fin outC) (inCh : Fin inC) (kIdx : Spec.Conv.Internal.MultiIndex (kernel.to (List ℕ))) : channelPairGet (Spec.convKernelDerivSpec layer input gradOutput) outCh inCh kIdx = ∑ outIdx : Spec.Conv.Internal.MultiIndex ((Spec.convOutSpatial inSpatial kernel stride padding).to (List ℕ)), (match Spec.Conv.Internal.mkInputIdx? outIdx.toList kIdx.toList (stride.to (List ℕ)) (padding.to (List ℕ)) with | none => 0 | some inIdx => Spec.getAtOrZero input (↑inCh :: inIdx)) * channelGet gradOutput outCh outIdx

One kernel-gradient coordinate is the contraction of input and output cotangent.

theorem Proofs.Autograd.Conv.getScalar_convBiasDerivSpec {d inC outC : ℕ} {kernel stride padding inSpatial : TorchLean.Tensor ℕ [d]} (layer : Spec.ConvSpec d inC outC kernel stride padding ℝ) (input : TorchLean.Tensor ℝ (Spec.Shape.ofList (inC :: inSpatial.to (List ℕ)))) (gradOutput : TorchLean.Tensor ℝ (Spec.Shape.ofList (outC :: (Spec.convOutSpatial inSpatial kernel stride padding).to (List ℕ)))) (outCh : Fin outC) : (Spec.convBiasDerivSpec layer input gradOutput).getScalar outCh = ∑ outIdx : Spec.Conv.Internal.MultiIndex ((Spec.convOutSpatial inSpatial kernel stride padding).to (List ℕ)), channelGet gradOutput outCh outIdx

One bias-gradient coordinate is the spatial sum of the output cotangent.

theorem Proofs.Autograd.Conv.channelGet_convBiasBroadcastSpec {d outC : ℕ} {kernel stride padding inSpatial : TorchLean.Tensor ℕ [d]} (bias : TorchLean.Tensor ℝ [outC]) (outCh : Fin outC) (outIdx : Spec.Conv.Internal.MultiIndex ((Spec.convOutSpatial inSpatial kernel stride padding).to (List ℕ))) : channelGet (Spec.convBiasBroadcastSpec bias) outCh outIdx = bias.getScalar outCh

Broadcasting a bias reads the same channel value at every spatial coordinate.

theorem Proofs.Autograd.Conv.channelGet_convInputDerivSpec {d inC outC : ℕ} {kernel stride padding inSpatial : TorchLean.Tensor ℕ [d]} (layer : Spec.ConvSpec d inC outC kernel stride padding ℝ) (input : TorchLean.Tensor ℝ (Spec.Shape.ofList (inC :: inSpatial.to (List ℕ)))) (gradOutput : TorchLean.Tensor ℝ (Spec.Shape.ofList (outC :: (Spec.convOutSpatial inSpatial kernel stride padding).to (List ℕ)))) (inCh : Fin inC) (inIdx : Spec.Conv.Internal.MultiIndex (inSpatial.to (List ℕ))) : channelGet (Spec.convInputDerivSpec layer input gradOutput) inCh inIdx = ∑ outCh : Fin outC, ∑ kIdx : Spec.Conv.Internal.MultiIndex (kernel.to (List ℕ)), match Spec.Conv.Internal.mkTransposeInputIdx? inIdx.toList kIdx.toList (stride.to (List ℕ)) (padding.to (List ℕ)) with | none => 0 | some outIdx => Spec.getAtOrZero gradOutput (↑outCh :: outIdx) * channelPairGet layer.kernel outCh inCh kIdx

One input-gradient coordinate is the specification's transpose-index contraction.

theorem Proofs.Autograd.Conv.channelGet_convInputDerivSpec_eq_coefficients {d inC outC : ℕ} {kernel stride padding inSpatial : TorchLean.Tensor ℕ [d]} (layer : Spec.ConvSpec d inC outC kernel stride padding ℝ) (input : TorchLean.Tensor ℝ (Spec.Shape.ofList (inC :: inSpatial.to (List ℕ)))) (gradOutput : TorchLean.Tensor ℝ (Spec.Shape.ofList (outC :: (Spec.convOutSpatial inSpatial kernel stride padding).to (List ℕ)))) (hStride : Spec.Conv.Internal.PositiveStrides (stride.to (List ℕ))) (inCh : Fin inC) (inIdx : Spec.Conv.Internal.MultiIndex (inSpatial.to (List ℕ))) : channelGet (Spec.convInputDerivSpec layer input gradOutput) inCh inIdx = ∑ outCh : Fin outC, ∑ outIdx : Spec.Conv.Internal.MultiIndex ((Spec.convOutSpatial inSpatial kernel stride padding).to (List ℕ)), convCoefficient layer.kernel outCh outIdx inCh inIdx * channelGet gradOutput outCh outIdx

The specification's input gradient multiplies by the transposed coefficient matrix.

Adjoint identities

theorem Proofs.Autograd.Conv.convCoreSpec_convInputDerivSpec_adjoint {d inC outC : ℕ} {kernel stride padding inSpatial : TorchLean.Tensor ℕ [d]} (layer : Spec.ConvSpec d inC outC kernel stride padding ℝ) (input deltaInput : TorchLean.Tensor ℝ (Spec.Shape.ofList (inC :: inSpatial.to (List ℕ)))) (gradOutput : TorchLean.Tensor ℝ (Spec.Shape.ofList (outC :: (Spec.convOutSpatial inSpatial kernel stride padding).to (List ℕ)))) (hStride : Spec.Conv.Internal.PositiveStrides (stride.to (List ℕ))) : TensorAlgebra.dot (Spec.convCoreSpec layer.kernel deltaInput) gradOutput = TensorAlgebra.dot deltaInput (Spec.convInputDerivSpec layer input gradOutput)

The forward input map and input-gradient specification are adjoint at every spatial rank.

theorem Proofs.Autograd.Conv.convCoreSpec_convKernelDerivSpec_adjoint {d inC outC : ℕ} {kernel stride padding inSpatial : TorchLean.Tensor ℕ [d]} (layer : Spec.ConvSpec d inC outC kernel stride padding ℝ) (input : TorchLean.Tensor ℝ (Spec.Shape.ofList (inC :: inSpatial.to (List ℕ)))) (deltaKernel : TorchLean.Tensor ℝ (Spec.Shape.ofList (outC :: inC :: kernel.to (List ℕ)))) (gradOutput : TorchLean.Tensor ℝ (Spec.Shape.ofList (outC :: (Spec.convOutSpatial inSpatial kernel stride padding).to (List ℕ)))) : TensorAlgebra.dot (Spec.convCoreSpec deltaKernel input) gradOutput = TensorAlgebra.dot deltaKernel (Spec.convKernelDerivSpec layer input gradOutput)

The kernel contraction and kernel-gradient specification are adjoint.

theorem Proofs.Autograd.Conv.convBiasBroadcastSpec_convBiasDerivSpec_adjoint {d inC outC : ℕ} {kernel stride padding inSpatial : TorchLean.Tensor ℕ [d]} (layer : Spec.ConvSpec d inC outC kernel stride padding ℝ) (input : TorchLean.Tensor ℝ (Spec.Shape.ofList (inC :: inSpatial.to (List ℕ)))) (deltaBias : TorchLean.Tensor ℝ [outC]) (gradOutput : TorchLean.Tensor ℝ (Spec.Shape.ofList (outC :: (Spec.convOutSpatial inSpatial kernel stride padding).to (List ℕ)))) : TensorAlgebra.dot (Spec.convBiasBroadcastSpec deltaBias) gradOutput = TensorAlgebra.dot deltaBias (Spec.convBiasDerivSpec layer input gradOutput)

Bias broadcasting and spatial reduction are adjoint.

Fréchet derivative

@[reducible, inline]

abbrev Proofs.Autograd.Conv.CoordVec (dims : List ℕ) : Type

Euclidean coordinates indexed by a tensor shape list.

noncomputable def Proofs.Autograd.Conv.coordVecOfFun {dims : List ℕ} (f : Spec.Conv.Internal.MultiIndex dims → ℝ) : CoordVec dims

Build shape-indexed Euclidean coordinates from a coordinate function.

@[simp]

theorem Proofs.Autograd.Conv.coordVecOfFun_apply {dims : List ℕ} (f : Spec.Conv.Internal.MultiIndex dims → ℝ) (i : Spec.Conv.Internal.MultiIndex dims) : (coordVecOfFun f).ofLp i = f i

Coordinates of coordVecOfFun f are the values of f.

noncomputable def Proofs.Autograd.Conv.tensorToCoordVec {dims : List ℕ} (x : TorchLean.Tensor ℝ (Spec.Shape.ofList dims)) : CoordVec dims

Vectorize a tensor using bounded multi-indices rather than flattened natural indices.

@[simp]

theorem Proofs.Autograd.Conv.tensorToCoordVec_apply {dims : List ℕ} (x : TorchLean.Tensor ℝ (Spec.Shape.ofList dims)) (i : Spec.Conv.Internal.MultiIndex dims) : (tensorToCoordVec x).ofLp i = Spec.Conv.Internal.MultiIndex.get x i

Coordinate i of a vectorized tensor is the tensor entry at i.

Convolution is indexed by bounded multi-indices rather than one flat Fin, because the stride and padding arithmetic is stated per axis; keeping the vectorization multi-indexed means no flattening appears in any of the derivative proofs.

noncomputable def Proofs.Autograd.Conv.convCoreVec {d inC outC : ℕ} {kernel stride padding inSpatial : TorchLean.Tensor ℕ [d]} (weights : CoordVec (outC :: inC :: kernel.to (List ℕ))) (input : CoordVec (inC :: inSpatial.to (List ℕ))) : CoordVec (outC :: (Spec.convOutSpatial inSpatial kernel stride padding).to (List ℕ))

The kernel/input contraction in Euclidean coordinates.

@[simp]

theorem Proofs.Autograd.Conv.convCoreVec_apply {d inC outC : ℕ} {kernel stride padding inSpatial : TorchLean.Tensor ℕ [d]} (weights : CoordVec (outC :: inC :: kernel.to (List ℕ))) (input : CoordVec (inC :: inSpatial.to (List ℕ))) (outCoord : Spec.Conv.Internal.MultiIndex (outC :: (Spec.convOutSpatial inSpatial kernel stride padding).to (List ℕ))) : (convCoreVec weights input).ofLp outCoord = ∑ inCh : Fin inC, ∑ inIdx : Spec.Conv.Internal.MultiIndex (inSpatial.to (List ℕ)), input.ofLp (inCh, inIdx) * ∑ kIdx : Spec.Conv.Internal.MultiIndex (kernel.to (List ℕ)), if Spec.Conv.Internal.mkInputIdx? outCoord.2.toList kIdx.toList (stride.to (List ℕ)) (padding.to (List ℕ)) = some inIdx.toList then weights.ofLp (outCoord.1, inCh, kIdx) else 0

Unfolds one output coordinate of the contraction into its double sum.

theorem Proofs.Autograd.Conv.tensorToCoordVec_convCoreSpec {d inC outC : ℕ} {kernel stride padding inSpatial : TorchLean.Tensor ℕ [d]} (weights : TorchLean.Tensor ℝ (Spec.Shape.ofList (outC :: inC :: kernel.to (List ℕ)))) (input : TorchLean.Tensor ℝ (Spec.Shape.ofList (inC :: inSpatial.to (List ℕ)))) : tensorToCoordVec (Spec.convCoreSpec weights input) = convCoreVec (tensorToCoordVec weights) (tensorToCoordVec input)

Tensor convolution and its Euclidean-coordinate contraction agree at every spatial rank.

@[reducible, inline]

abbrev Proofs.Autograd.Conv.ConvKernelCoords {d : ℕ} (outC inC : ℕ) (kernel : TorchLean.Tensor ℕ [d]) : Type

Euclidean kernel coordinates for a rank-general convolution.

@[reducible, inline]

abbrev Proofs.Autograd.Conv.ConvInputCoords {d : ℕ} (inC : ℕ) (inSpatial : TorchLean.Tensor ℕ [d]) : Type

Euclidean input coordinates for a rank-general convolution.

@[reducible, inline]

abbrev Proofs.Autograd.Conv.ConvOutputCoords {d : ℕ} (outC : ℕ) (inSpatial kernel stride padding : TorchLean.Tensor ℕ [d]) : Type

Euclidean output coordinates for a rank-general convolution.

theorem Proofs.Autograd.Conv.convCoreVec_add_input {d inC outC : ℕ} {kernel stride padding inSpatial : TorchLean.Tensor ℕ [d]} (weights : ConvKernelCoords outC inC kernel) (x y : ConvInputCoords inC inSpatial) : convCoreVec weights (x + y) = convCoreVec weights x + convCoreVec weights y

The convolution contraction is additive in its input coordinates.

theorem Proofs.Autograd.Conv.convCoreVec_smul_input {d inC outC : ℕ} {kernel stride padding inSpatial : TorchLean.Tensor ℕ [d]} (weights : ConvKernelCoords outC inC kernel) (c : ℝ) (input : ConvInputCoords inC inSpatial) : convCoreVec weights (c • input) = c • convCoreVec weights input

The convolution contraction respects scalar multiplication in its input coordinates.

theorem Proofs.Autograd.Conv.convCoreVec_add_kernel {d inC outC : ℕ} {kernel stride padding inSpatial : TorchLean.Tensor ℕ [d]} (w z : ConvKernelCoords outC inC kernel) (input : ConvInputCoords inC inSpatial) : convCoreVec (w + z) input = convCoreVec w input + convCoreVec z input

The convolution contraction is additive in its kernel coordinates.

theorem Proofs.Autograd.Conv.convCoreVec_smul_kernel {d inC outC : ℕ} {kernel stride padding inSpatial : TorchLean.Tensor ℕ [d]} (c : ℝ) (weights : ConvKernelCoords outC inC kernel) (input : ConvInputCoords inC inSpatial) : convCoreVec (c • weights) input = c • convCoreVec weights input

The convolution contraction respects scalar multiplication in its kernel coordinates.

noncomputable def Proofs.Autograd.Conv.convCoreBilin {d inC outC : ℕ} {kernel stride padding inSpatial : TorchLean.Tensor ℕ [d]} : ConvKernelCoords outC inC kernel →L[ℝ] ConvInputCoords inC inSpatial →L[ℝ] ConvOutputCoords outC inSpatial kernel stride padding

Continuous bilinear form of rank-general convolution.

@[simp]

theorem Proofs.Autograd.Conv.convCoreBilin_apply {d inC outC : ℕ} {kernel stride padding inSpatial : TorchLean.Tensor ℕ [d]} (weights : CoordVec (outC :: inC :: kernel.to (List ℕ))) (input : CoordVec (inC :: inSpatial.to (List ℕ))) : (convCoreBilin weights) input = convCoreVec weights input

The bundled bilinear map computes the same contraction as convCoreVec.

Bundling matters: once convolution is a continuous bilinear map, its derivative in each argument comes from mathlib rather than a separate difference-quotient argument.

noncomputable def Proofs.Autograd.Conv.convBiasBroadcastCLM {d outC : ℕ} {kernel stride padding inSpatial : TorchLean.Tensor ℕ [d]} : CoordVec [outC] →L[ℝ] CoordVec (outC :: (Spec.convOutSpatial inSpatial kernel stride padding).to (List ℕ))

Continuous linear bias broadcast in Euclidean coordinates.

@[simp]

theorem Proofs.Autograd.Conv.convBiasBroadcastCLM_apply {d outC : ℕ} {kernel stride padding inSpatial : TorchLean.Tensor ℕ [d]} (bias : CoordVec [outC]) (outCoord : Spec.Conv.Internal.MultiIndex (outC :: (Spec.convOutSpatial inSpatial kernel stride padding).to (List ℕ))) : (convBiasBroadcastCLM bias).ofLp outCoord = bias.ofLp (outCoord.1, PUnit.unit)

Bias broadcast copies the channel entry to every spatial position of that channel.

theorem Proofs.Autograd.Conv.tensorToCoordVec_addSpec {dims : List ℕ} (x y : TorchLean.Tensor ℝ (Spec.Shape.ofList dims)) : tensorToCoordVec (x.addSpec y) = tensorToCoordVec x + tensorToCoordVec y

Coordinate conversion preserves pointwise tensor addition.

theorem Proofs.Autograd.Conv.tensorToCoordVec_convBiasBroadcastSpec {d outC : ℕ} {kernel stride padding inSpatial : TorchLean.Tensor ℕ [d]} (bias : TorchLean.Tensor ℝ [outC]) : tensorToCoordVec (Spec.convBiasBroadcastSpec bias) = convBiasBroadcastCLM (tensorToCoordVec bias)

Tensor bias broadcasting agrees with the corresponding coordinate map.

noncomputable def Proofs.Autograd.Conv.convForwardVec {d inC outC : ℕ} {kernel stride padding inSpatial : TorchLean.Tensor ℕ [d]} (state : (CoordVec (outC :: inC :: kernel.to (List ℕ)) × CoordVec [outC]) × CoordVec (inC :: inSpatial.to (List ℕ))) : CoordVec (outC :: (Spec.convOutSpatial inSpatial kernel stride padding).to (List ℕ))

Coordinate form of a complete convolution layer, including bias.

theorem Proofs.Autograd.Conv.tensorToCoordVec_convSpec {d inC outC : ℕ} {kernel stride padding inSpatial : TorchLean.Tensor ℕ [d]} (layer : Spec.ConvSpec d inC outC kernel stride padding ℝ) (input : TorchLean.Tensor ℝ (Spec.Shape.ofList (inC :: inSpatial.to (List ℕ)))) : tensorToCoordVec (Spec.convSpec layer input) = convForwardVec ((tensorToCoordVec layer.kernel, tensorToCoordVec layer.bias), tensorToCoordVec input)

Tensor-level convSpec agrees with convForwardVec.

@[reducible, inline]

abbrev Proofs.Autograd.Conv.ConvState {d : ℕ} (inC outC : ℕ) (kernel inSpatial : TorchLean.Tensor ℕ [d]) : Type

Euclidean state space of one rank-general convolution application.

def Proofs.Autograd.Conv.convWeightProjection {d inC outC : ℕ} {kernel inSpatial : TorchLean.Tensor ℕ [d]} : ConvState inC outC kernel inSpatial →L[ℝ] CoordVec (outC :: inC :: kernel.to (List ℕ))

Projection of the kernel coordinates from a convolution state.

def Proofs.Autograd.Conv.convBiasProjection {d inC outC : ℕ} {kernel inSpatial : TorchLean.Tensor ℕ [d]} : ConvState inC outC kernel inSpatial →L[ℝ] CoordVec [outC]

Projection of the bias coordinates from a convolution state.

def Proofs.Autograd.Conv.convInputProjection {d inC outC : ℕ} {kernel inSpatial : TorchLean.Tensor ℕ [d]} : ConvState inC outC kernel inSpatial →L[ℝ] CoordVec (inC :: inSpatial.to (List ℕ))

Projection of the input coordinates from a convolution state.

noncomputable def Proofs.Autograd.Conv.convDerivative {d inC outC : ℕ} {kernel stride padding inSpatial : TorchLean.Tensor ℕ [d]} (state : ConvState inC outC kernel inSpatial) : ConvState inC outC kernel inSpatial →L[ℝ] CoordVec (outC :: (Spec.convOutSpatial inSpatial kernel stride padding).to (List ℕ))

Product-rule derivative of a complete convolution state.

theorem Proofs.Autograd.Conv.hasFDerivAt_convForwardVec {d inC outC : ℕ} {kernel stride padding inSpatial : TorchLean.Tensor ℕ [d]} (state : ConvState inC outC kernel inSpatial) : HasFDerivAt convForwardVec (convDerivative state) state

The exact derivative of a rank-general convolution is its kernel/input product rule plus bias.

theorem Proofs.Autograd.Conv.tensorToCoordVec_convJvpSpec {d inC outC : ℕ} {kernel stride padding inSpatial : TorchLean.Tensor ℕ [d]} (layer tangentLayer : Spec.ConvSpec d inC outC kernel stride padding ℝ) (input tangentInput : TorchLean.Tensor ℝ (Spec.Shape.ofList (inC :: inSpatial.to (List ℕ)))) : tensorToCoordVec (Spec.convJvpSpec layer tangentLayer input tangentInput) = (convDerivative ((tensorToCoordVec layer.kernel, tensorToCoordVec layer.bias), tensorToCoordVec input)) ((tensorToCoordVec tangentLayer.kernel, tensorToCoordVec tangentLayer.bias), tensorToCoordVec tangentInput)

Applying the analytic derivative gives the tensor-level convolution JVP.

theorem Proofs.Autograd.Conv.convJvpSpec_convBackwardSpec_adjoint {d inC outC : ℕ} {kernel stride padding inSpatial : TorchLean.Tensor ℕ [d]} (layer tangentLayer : Spec.ConvSpec d inC outC kernel stride padding ℝ) (input tangentInput : TorchLean.Tensor ℝ (Spec.Shape.ofList (inC :: inSpatial.to (List ℕ)))) (gradOutput : TorchLean.Tensor ℝ (Spec.Shape.ofList (outC :: (Spec.convOutSpatial inSpatial kernel stride padding).to (List ℕ)))) (hStride : Spec.Conv.Internal.PositiveStrides (stride.to (List ℕ))) : TensorAlgebra.dot (Spec.convJvpSpec layer tangentLayer input tangentInput) gradOutput = have gradients := Spec.convBackwardSpec layer input gradOutput; TensorAlgebra.dot tangentLayer.kernel gradients.kernelGradient + TensorAlgebra.dot tangentLayer.bias gradients.biasGradient + TensorAlgebra.dot tangentInput gradients.inputGradient

The convolution backward specification is the adjoint of the exact JVP.

The ConvGradients fields pair the kernel, bias, and input gradients with their corresponding tangents. Positive strides are needed for the transpose input-index relation.