TorchLean API

Docs Home Installation Guide Examples Graphs Tools

NN.Spec.Layers.Pooling.TwoD

Two-Dimensional Pooling Adapters #

The fixed-window operations in this file are two-dimensional views of the rank-polymorphic definitions in NN.Spec.Layers.Pooling.ND. They retain the conventional maxPool2d and avgPool2d names used by model APIs and PyTorch interchange, but do not define a second pooling semantics.

Adaptive pooling remains genuinely two-dimensional here because its variable-size binning is a different operation from fixed-kernel N-D pooling.

structure Spec.MaxPool2DSpec (kH kW stride : ℕ) (_hH : kH ≠ 0) (_hW : kW ≠ 0) (_hStride : stride ≠ 0) :

Witness for a nonempty two-dimensional max-pooling kernel and nonzero uniform stride.

Instances For

structure Spec.AvgPool2DSpec (kH kW stride : ℕ) (_hH : kH ≠ 0) (_hW : kW ≠ 0) (_hStride : stride ≠ 0) :

Witness for a nonempty two-dimensional average-pooling kernel and nonzero uniform stride.

Instances For

def Spec.pool2dOutShape (inH inW kH kW stride : ℕ) :

Output shape for unpadded single-channel two-dimensional pooling.

Instances For

def Spec.pool2dMultiOutShape (inC inH inW kH kW stride : ℕ) :

Output shape for unpadded channel-first two-dimensional pooling.

Instances For

def Spec.pool2dOutShapePad (inH inW kH kW stride padding : ℕ) :

Output shape for single-channel two-dimensional pooling with symmetric padding.

Instances For

def Spec.pool2dMultiOutShapePad (inC inH inW kH kW stride padding : ℕ) :

Output shape for channel-first two-dimensional pooling with symmetric padding.

Instances For

theorem Spec.Private.pool2d_kernel_ne {kH kW : ℕ} (hH : kH ≠ 0) (hW : kW ≠ 0) (i : Fin 2) :

#v[kH, kW].get i ≠ 0

theorem Spec.Private.pool2d_stride_ne {stride : ℕ} (hStride : stride ≠ 0) (i : Fin 2) :

#v[stride, stride].get i ≠ 0

def Spec.Private.maxPool2DConfig {kH kW stride : ℕ} (padding : ℕ) (hH : kH ≠ 0) (hW : kW ≠ 0) (hStride : stride ≠ 0) :

MaxPoolSpec 2 #v[kH, kW] #v[stride, stride] #v[padding, padding] ⋯ ⋯

Instances For

def Spec.Private.avgPool2DConfig {kH kW stride : ℕ} (padding : ℕ) (hH : kH ≠ 0) (hW : kW ≠ 0) (hStride : stride ≠ 0) :

AvgPoolSpec 2 #v[kH, kW] #v[stride, stride] #v[padding, padding] ⋯ ⋯

Instances For

theorem Spec.Private.pool2d_spatial_out_shape_eq (inH inW kH kW stride padding : ℕ) :

Shape.ofList (poolOutSpatialPad #v[inH, inW] #v[kH, kW] #v[stride, stride] #v[padding, padding]).toList = pool2dOutShapePad inH inW kH kW stride padding

theorem Spec.Private.pool2d_multi_out_shape_eq (inC inH inW kH kW stride padding : ℕ) :

Shape.ofList (inC :: (poolOutSpatialPad #v[inH, inW] #v[kH, kW] #v[stride, stride] #v[padding, padding]).toList) = pool2dMultiOutShapePad inC inH inW kH kW stride padding

Fixed-window adapters #

def Spec.maxPool2dSpec {α : Type} [Context α] {kH kW inH inW stride : ℕ} {h1 : kH ≠ 0} {h2 : kW ≠ 0} {hStride : stride ≠ 0} (layer : MaxPool2DSpec kH kW stride h1 h2 hStride) (input : Tensor α (Shape.dim inH (Shape.dim inW Shape.scalar))) :

Tensor α (pool2dOutShape inH inW kH kW stride)

Single-channel two-dimensional max pooling, specialized from maxPoolSpatialSpec.

Instances For

def Spec.maxPool2dMultiSpec {α : Type} [Context α] {kH kW inH inW inC stride : ℕ} {h1 : kH ≠ 0} {h2 : kW ≠ 0} {hStride : stride ≠ 0} (layer : MaxPool2DSpec kH kW stride h1 h2 hStride) (input : Tensor α (Shape.dim inC (Shape.dim inH (Shape.dim inW Shape.scalar)))) :

Tensor α (pool2dMultiOutShape inC inH inW kH kW stride)

Channel-first two-dimensional max pooling, specialized from maxPoolSpec.

Instances For

def Spec.maxPool2dLinearizationSpec {α : Type} [Context α] {kH kW inH inW stride : ℕ} {h1 : kH ≠ 0} {h2 : kW ≠ 0} {hStride : stride ≠ 0} (layer : MaxPool2DSpec kH kW stride h1 h2 hStride) (input tangent : Tensor α (Shape.dim inH (Shape.dim inW Shape.scalar))) :

Tensor α (pool2dOutShape inH inW kH kW stride)

Selected-branch JVP for single-channel two-dimensional hard max pooling.

Instances For

def Spec.maxPool2dMultiLinearizationSpec {α : Type} [Context α] {kH kW inH inW inC stride : ℕ} {h1 : kH ≠ 0} {h2 : kW ≠ 0} {hStride : stride ≠ 0} (layer : MaxPool2DSpec kH kW stride h1 h2 hStride) (input tangent : Tensor α (Shape.dim inC (Shape.dim inH (Shape.dim inW Shape.scalar)))) :

Tensor α (pool2dMultiOutShape inC inH inW kH kW stride)

Selected-branch JVP for channel-first two-dimensional hard max pooling.

Instances For

def Spec.avgPool2dSpec {α : Type} [Context α] {kH kW inH inW stride : ℕ} {h1 : kH ≠ 0} {h2 : kW ≠ 0} {hStride : stride ≠ 0} (layer : AvgPool2DSpec kH kW stride h1 h2 hStride) (input : Tensor α (Shape.dim inH (Shape.dim inW Shape.scalar))) :

Tensor α (pool2dOutShape inH inW kH kW stride)

Single-channel two-dimensional average pooling, specialized from avgPoolSpatialSpec.

Instances For

def Spec.avgPool2dMultiSpec {α : Type} [Context α] {kH kW inH inW inC stride : ℕ} (h1 : kH ≠ 0) (h2 : kW ≠ 0) {hStride : stride ≠ 0} (layer : AvgPool2DSpec kH kW stride h1 h2 hStride) (input : Tensor α (Shape.dim inC (Shape.dim inH (Shape.dim inW Shape.scalar)))) :

Tensor α (pool2dMultiOutShape inC inH inW kH kW stride)

Channel-first two-dimensional average pooling, specialized from avgPoolSpec.

Instances For

def Spec.maxPool2dBackwardSpec {α : Type} [Context α] {kH kW inH inW stride : ℕ} {h1 : kH ≠ 0} {h2 : kW ≠ 0} {hStride : stride ≠ 0} (_layer : MaxPool2DSpec kH kW stride h1 h2 hStride) (input : Tensor α (Shape.dim inH (Shape.dim inW Shape.scalar))) (grad_output : Tensor α (pool2dOutShape inH inW kH kW stride)) :

Tensor α (Shape.dim inH (Shape.dim inW Shape.scalar))

VJP for single-channel two-dimensional max pooling.

Instances For

def Spec.maxPool2dMultiBackwardSpec {α : Type} [Context α] {kH kW inH inW inC stride : ℕ} {h1 : kH ≠ 0} {h2 : kW ≠ 0} {hStride : stride ≠ 0} (layer : MaxPool2DSpec kH kW stride h1 h2 hStride) (input : Tensor α (Shape.dim inC (Shape.dim inH (Shape.dim inW Shape.scalar)))) (grad_output : Tensor α (pool2dMultiOutShape inC inH inW kH kW stride)) :

Tensor α (Shape.dim inC (Shape.dim inH (Shape.dim inW Shape.scalar)))

VJP for channel-first two-dimensional max pooling.

Instances For

def Spec.avgPool2dBackwardSpec {α : Type} [Context α] {kH kW inH inW stride : ℕ} (_h1 : kH ≠ 0) (_h2 : kW ≠ 0) {hStride : stride ≠ 0} (_layer : AvgPool2DSpec kH kW stride _h1 _h2 hStride) (grad_output : Tensor α (pool2dOutShape inH inW kH kW stride)) :

Tensor α (Shape.dim inH (Shape.dim inW Shape.scalar))

VJP for single-channel two-dimensional average pooling.

Instances For

Smooth max pooling #

def Spec.smoothMaxPool2dSpec {α : Type} [Context α] {kH kW inH inW stride : ℕ} {h1 : kH ≠ 0} {h2 : kW ≠ 0} {hStride : stride ≠ 0} (layer : MaxPool2DSpec kH kW stride h1 h2 hStride) (beta : α) (input : Tensor α (Shape.dim inH (Shape.dim inW Shape.scalar))) :

Tensor α (pool2dOutShape inH inW kH kW stride)

Single-channel smooth max pooling using the N-D log-sum-exp specification.

Instances For

def Spec.smoothMaxPool2dMultiSpec {α : Type} [Context α] {kH kW inH inW inC stride : ℕ} {h1 : kH ≠ 0} {h2 : kW ≠ 0} {hStride : stride ≠ 0} (layer : MaxPool2DSpec kH kW stride h1 h2 hStride) (beta : α) (input : Tensor α (Shape.dim inC (Shape.dim inH (Shape.dim inW Shape.scalar)))) :

Tensor α (pool2dMultiOutShape inC inH inW kH kW stride)

Channel-first smooth max pooling using the N-D log-sum-exp specification.

Instances For

def Spec.smoothMaxPool2dJvpSpec {α : Type} [Context α] {kH kW inH inW stride : ℕ} {h1 : kH ≠ 0} {h2 : kW ≠ 0} {hStride : stride ≠ 0} (layer : MaxPool2DSpec kH kW stride h1 h2 hStride) (beta : α) (input tangent : Tensor α (Shape.dim inH (Shape.dim inW Shape.scalar))) :

Tensor α (pool2dOutShape inH inW kH kW stride)

JVP for single-channel smooth max pooling.

Instances For

def Spec.smoothMaxPool2dMultiJvpSpec {α : Type} [Context α] {kH kW inH inW inC stride : ℕ} {h1 : kH ≠ 0} {h2 : kW ≠ 0} {hStride : stride ≠ 0} (layer : MaxPool2DSpec kH kW stride h1 h2 hStride) (beta : α) (input tangent : Tensor α (Shape.dim inC (Shape.dim inH (Shape.dim inW Shape.scalar)))) :

Tensor α (pool2dMultiOutShape inC inH inW kH kW stride)

JVP for channel-first smooth max pooling.

Instances For

Adaptive pooling #

structure Spec.AdaptiveAvgPool2DSpec (outH outW : ℕ) :

Witness for adaptive average pooling to a fixed two-dimensional output shape.

Instances For

structure Spec.AdaptiveMaxPool2DSpec (outH outW : ℕ) :

Witness for adaptive max pooling to a fixed two-dimensional output shape.

Instances For

def Spec.adaptiveStart (inSize outSize i : ℕ) :

Start of adaptive-pooling bin i: floor(i * input / output).

Instances For

def Spec.adaptiveEnd (inSize outSize i : ℕ) :

End of adaptive-pooling bin i: ceil((i + 1) * input / output).

Instances For

def Spec.adaptiveAvgPool2dSpec {α : Type} [Context α] {inH inW inC : ℕ} (outH outW : ℕ) (_layer : AdaptiveAvgPool2DSpec outH outW) (input : Tensor α (Shape.dim inC (Shape.dim inH (Shape.dim inW Shape.scalar)))) (_hInH : inH > 0 := by norm_num) (_hInW : inW > 0 := by norm_num) (_hOutH : outH > 0 := by norm_num) (_hOutW : outW > 0 := by norm_num) :

Tensor α (Shape.dim inC (Shape.dim outH (Shape.dim outW Shape.scalar)))

Two-dimensional adaptive average pooling with PyTorch-compatible bins.

Instances For

def Spec.adaptiveMaxPool2dSpec {α : Type} [Context α] {inH inW inC : ℕ} (outH outW : ℕ) (_layer : AdaptiveMaxPool2DSpec outH outW) (input : Tensor α (Shape.dim inC (Shape.dim inH (Shape.dim inW Shape.scalar)))) (_hInH : inH > 0 := by norm_num) (_hInW : inW > 0 := by norm_num) (_hOutH : outH > 0 := by norm_num) (_hOutW : outW > 0 := by norm_num) :

Tensor α (Shape.dim inC (Shape.dim outH (Shape.dim outW Shape.scalar)))

Two-dimensional adaptive max pooling with PyTorch-compatible bins.

Instances For