Verified Deep Learning with Lean 4

7 Depthwise Convolution

Axiom 50 Depthwise conv forward
#
Axiom 51 Depthwise input VJP
#
Axiom 52 Depthwise weight VJP
#

Phase 7: reuses \(\mathsf{HasVJP3}\) directly since DepthwiseKernel is definitionally \(\mathsf{Tensor3}\).

Axiom 53 Depthwise bias VJP
#

Phase 9.