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.

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.channelGet_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) : channelGet (Spec.convBiasDerivSpec layer input gradOutput) outCh PUnit.unit = ∑ 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.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

A bias-gradient coordinate in the ordinary rank-one tensor view.

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 transpose-index convolution used by the runtime.

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 implemented input gradient is multiplication 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 implemented input gradient 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 implemented kernel gradient 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 from a hand-written difference quotient.

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 implemented convolution backward pass is the adjoint of the exact JVP.

convBackwardSpec returns a ConvGradients record, so the equation below reads one inner product per gradient, each paired with the matching piece of the input tangent. An earlier version returned a bare triple and had to project the components out by position, which is the same proposition and considerably harder to check against a sentence describing it.