FDeriv

Analytic (HasFDerivAt/fderiv) correctness for a Conv2D-shaped bilinear map.

This file adds a proof-only node constructor that treats convolution as a bilinear map in (kernel, input) plus a linear bias broadcast, and defines its VJP as the adjoint of the Fréchet derivative. This is enough for the general DAG theorem Graph.backpropVec_eq_adjoint_fderiv to cover graphs using this node.

Note: the runtime engine uses Spec.conv2d_backward_spec; connecting that handwritten backward to this analytic VJP is a separate theorem.

The remaining definitions package the convolution computation into linear/bilinear maps on flattened vectors. This is the standard analytic path: show the forward map is bilinear in (kernel, input), then take Fréchet derivatives and adjoints.

@[reducible, inline]

abbrev Proofs.Autograd.TapeNodes.Conv2D.outH {IH KH stride padding : ℕ} : ℕ

Output height of conv2d, computed from input height, kernel height, stride, and padding.

@[reducible, inline]

abbrev Proofs.Autograd.TapeNodes.Conv2D.outW {IW KW stride padding : ℕ} : ℕ

Output width of conv2d, computed from input width, kernel width, stride, and padding.

@[reducible, inline]

abbrev Proofs.Autograd.TapeNodes.Conv2D.sK (OC IC KH KW : ℕ) : Spec.Shape

Shape of the Conv2D kernel parameter K (a OC × IC × KH × KW tensor).

@[reducible, inline]

abbrev Proofs.Autograd.TapeNodes.Conv2D.sB (OC : ℕ) : Spec.Shape

Shape of the Conv2D bias parameter b (a length-OC vector).

@[reducible, inline]

abbrev Proofs.Autograd.TapeNodes.Conv2D.sX (IC IH IW : ℕ) : Spec.Shape

Shape of the Conv2D input X (a IC × IH × IW tensor).

@[reducible, inline]

abbrev Proofs.Autograd.TapeNodes.Conv2D.sY (OC OH OW : ℕ) : Spec.Shape

Shape of the Conv2D output Y (a OC × OH × OW tensor).