Main convolution backward-dot theorem layer.
This file combines the input and weight-side algebra needed to prove the tape-level dot-product form of convolution backpropagation.
theorem
Proofs.Autograd.Conv2D.conv2d_backward_spec_dot
{inC outC kH kW stride padding inH inW : ℕ}
{h1 : inC ≠ 0}
{h2 : kH ≠ 0}
{h3 : kW ≠ 0}
(layer : Spec.Conv2DSpec inC outC kH kW stride padding ℝ h1 h2 h3)
(input : Spec.MultiChannelImage inC inH inW ℝ)
(δ : Spec.MultiChannelImage outC (outH inH kH stride padding) (outW inW kW stride padding) ℝ)
(dKernel :
Spec.Tensor ℝ (Spec.Shape.dim outC (Spec.Shape.dim inC (Spec.Shape.dim kH (Spec.Shape.dim kW Spec.Shape.scalar)))))
(dBias : Spec.Tensor ℝ (Spec.Shape.dim outC Spec.Shape.scalar))
(dInput : Spec.MultiChannelImage inC inH inW ℝ)
:
have layerK := { kernel := dKernel, bias := Spec.fill 0 (Spec.Shape.dim outC Spec.Shape.scalar) };
have layer0 := { kernel := layer.kernel, bias := Spec.fill 0 (Spec.Shape.dim outC Spec.Shape.scalar) };
have jvp :=
Spec.Tensor.addSpec (Spec.conv2dSpec layerK input) ((biasBroadcast dBias).addSpec (Spec.conv2dSpec layer0 dInput));
have grads := Spec.conv2dBackwardSpec layer input δ;
Spec.dot jvp δ = Spec.dot dKernel grads.1 + Spec.dot dBias grads.2.1 + Spec.dot dInput grads.2.2
Main dot-level bridge theorem for Conv2D.
It states that the triple returned by Spec.conv2d_backward_spec is the adjoint (w.r.t. Spec.dot)
of the corresponding forward-mode directional derivatives with respect to (kernel, bias, input).
This is the key lemma connecting the handwritten runtime backward to the analytic “VJP is adjoint
of fderiv” theorem in NN.Proofs.Autograd.Tape.Ops.Conv.FDeriv.