TorchLean API

NN.Spec.Layers.Pooling.ND

N-D Pooling #

Dimension-polymorphic pooling specs for spatial tensors and channels-first tensors.

Generic N-D pooling (channels-first, no batch) #

These operators generalize the existing 2D pooling specs to an arbitrary spatial rank d.

Conventions:

PyTorch comparisons (conceptual, without batch axis):

Layer configs + output shapes #

structure Spec.MaxPoolSpec (d : ) (kernel stride padding : Vector d) (hKernel : ∀ (i : Fin d), kernel.get i 0) (hStride : ∀ (i : Fin d), stride.get i 0) :

Witness that an N-D max-pooling configuration has nonzero kernel and stride on every axis.

The vectors are indices of the type rather than duplicate structure fields, so a value cannot advertise one configuration while its type describes another.

    Instances For
      structure Spec.AvgPoolSpec (d : ) (kernel stride padding : Vector d) (hKernel : ∀ (i : Fin d), kernel.get i 0) (hStride : ∀ (i : Fin d), stride.get i 0) :

      Witness that an N-D average-pooling configuration has nonzero kernel and stride on every axis.

        Instances For
          def Spec.poolOutDim (input kernel stride padding : ) :

          Output spatial sizes with symmetric padding.

          Pooling follows the usual floor-mode sliding-window formula, but an empty input axis, empty kernel, or padding larger than half the kernel gives an empty output axis. The last condition is part of the pooling contract used by PyTorch and by TorchLean's native implementations; it is not a restriction on convolution.

          Instances For
            def Spec.poolOutSpatial {d : } (inSpatial kernel stride : Vector d) :

            Output spatial sizes without padding.

            An invalid axis (empty input, zero kernel, zero stride, or a kernel larger than the input) has size zero.

            Instances For
              def Spec.poolOutSpatialPad {d : } (inSpatial kernel stride padding : Vector d) :

              Apply poolOutDim independently to each spatial axis.

              Instances For
                theorem Spec.poolOutSpatialPad_global {d : } (spatial : Vector d) (hSpatial : ∀ (i : Fin d), spatial.get i 0) :

                Pooling over the complete spatial extent produces one value on every spatial axis.

                def Spec.poolOutShape {d : } (inSpatial kernel stride : Vector d) :

                Output shape for single-channel N-D pooling (no padding).

                Instances For
                  def Spec.poolMultiOutShape {d : } (inC : ) (inSpatial kernel stride : Vector d) :

                  Output shape for channels-first N-D pooling (no padding; channels preserved).

                  Instances For
                    def Spec.poolOutShapePad {d : } (inSpatial kernel stride padding : Vector d) :

                    Output shape for single-channel N-D pooling with symmetric padding.

                    Instances For
                      def Spec.poolMultiOutShapePad {d : } (inC : ) (inSpatial kernel stride padding : Vector d) :

                      Output shape for channels-first N-D pooling with symmetric padding (channels preserved).

                      Instances For
                        def Spec.Private.tensorOfDims {α : Type} (dims : List ) (f : List α) :
                        Instances For
                          def Spec.Private.foldlIndices' {β : Type} (dims : List ) (init : β) (f : βList β) :
                          β
                          Instances For
                            def Spec.Private.paddedCoords? (outIdxs winIdxs stride : List ) :
                            Instances For
                              def Spec.Private.unpadCoords? (padded padding : List ) :
                              Instances For
                                Instances For
                                  def Spec.Private.getPaddedAverageInputVal {α : Type} [Context α] {d : } {inSpatial : Vector d} (input : Tensor α (Shape.ofList inSpatial.toList)) (outIdxs winIdxs stride padding : List ) :
                                  α

                                  Input lookup for average/smooth pooling.

                                  For average-style pooling, padded cells contribute numeric zero and are still counted by the denominator chosen by the surrounding pooling spec. We keep this separate from getPaddedMaxInputVal?, where padded cells must be ignored rather than treated as zero.

                                  Instances For
                                    def Spec.Private.getPaddedMaxInputVal? {α : Type} [Context α] {d : } {inSpatial : Vector d} (input : Tensor α (Shape.ofList inSpatial.toList)) (outIdxs winIdxs stride padding : List ) :

                                    Input lookup for hard max-pooling.

                                    Unlike average pooling, max pooling does not insert numeric zero for an individual padded cell: PyTorch's valid max-pool configurations behave as though those cells were -∞. TorchLean keeps the spec scalar-polymorphic by returning none for padded coordinates and ignoring them in the max fold. poolOutSpatialPad rejects empty input axes, empty kernels, and padding beyond PyTorch's half-kernel restriction, so every emitted output window contains at least one input coordinate.

                                    Instances For
                                      Instances For
                                        def Spec.Private.maxPoolValue {α : Type} [Context α] {d : } {inSpatial : Vector d} (input : Tensor α (Shape.ofList inSpatial.toList)) (outIdxs kernel stride padding : List ) :
                                        α
                                        Instances For
                                          def Spec.Private.maxPoolSelectedTangentValue {α : Type} [Context α] {d : } {inSpatial : Vector d} (input tangent : Tensor α (Shape.ofList inSpatial.toList)) (outIdxs kernel stride padding : List ) :
                                          α

                                          Selected-branch tangent for one hard max-pooling window.

                                          The tangent follows the same winner selected by maxPoolValue. At a tie this is a deterministic generalized-derivative convention, not the mathematical directional derivative of max.

                                          Instances For
                                            def Spec.Private.avgPoolValue {α : Type} [Context α] {d : } {inSpatial : Vector d} (input : Tensor α (Shape.ofList inSpatial.toList)) (outIdxs kernel stride padding : List ) :
                                            α
                                            Instances For
                                              def Spec.Private.smoothMaxPoolPivot {α : Type} [Context α] {d : } {inSpatial : Vector d} (beta : α) (input : Tensor α (Shape.ofList inSpatial.toList)) (outIdxs kernel stride padding : List ) :
                                              α

                                              Input-space pivot whose scaled value is maximal over a nonempty N-D pooling window.

                                              Instances For
                                                def Spec.Private.smoothMaxPoolValue {α : Type} [Context α] {d : } {inSpatial : Vector d} (beta : α) (input : Tensor α (Shape.ofList inSpatial.toList)) (outIdxs kernel stride padding : List ) :
                                                α

                                                Evaluate one N-D smooth-max window with the sign-aware input-space pivot.

                                                Instances For
                                                  def Spec.Private.smoothMaxPoolJvpValue {α : Type} [Context α] {d : } {inSpatial : Vector d} (beta : α) (input tangent : Tensor α (Shape.ofList inSpatial.toList)) (outIdxs kernel stride padding : List ) :
                                                  α

                                                  Directional derivative of the smooth log-sum-exp pooling value.

                                                  For y = beta⁻¹ log Σ exp(beta*xᵢ), the directional derivative is Σ softmax(beta*xᵢ) * dxᵢ, using the same zero-padding and stable input-pivot convention as smoothMaxPoolValue.

                                                  Instances For

                                                    Forward (single-channel spatial tensor) #

                                                    def Spec.maxPoolSpatialSpec {α : Type} [Context α] {d : } {inSpatial kernel stride padding : Vector d} {hKernel : ∀ (i : Fin d), kernel.get i 0} {hStride : ∀ (i : Fin d), stride.get i 0} (_layer : MaxPoolSpec d kernel stride padding hKernel hStride) (input : Tensor α (Shape.ofList inSpatial.toList)) :
                                                    Tensor α (Shape.ofList (poolOutSpatialPad inSpatial kernel stride padding).toList)

                                                    N-D max pooling on a spatial tensor (no explicit channel axis).

                                                    Instances For
                                                      def Spec.maxPoolSpatialLinearizationSpec {α : Type} [Context α] {d : } {inSpatial kernel stride padding : Vector d} {hKernel : ∀ (i : Fin d), kernel.get i 0} {hStride : ∀ (i : Fin d), stride.get i 0} (_layer : MaxPoolSpec d kernel stride padding hKernel hStride) (input tangent : Tensor α (Shape.ofList inSpatial.toList)) :
                                                      Tensor α (Shape.ofList (poolOutSpatialPad inSpatial kernel stride padding).toList)

                                                      Selected-branch linearization for N-D hard max-pooling on a spatial tensor.

                                                      Away from ties this is the ordinary JVP. At ties it follows the first row-major primal maximizer, matching the VJP convention but not claiming an analytic directional derivative.

                                                      Instances For
                                                        def Spec.avgPoolSpatialSpec {α : Type} [Context α] {d : } {inSpatial kernel stride padding : Vector d} {hKernel : ∀ (i : Fin d), kernel.get i 0} {hStride : ∀ (i : Fin d), stride.get i 0} (_layer : AvgPoolSpec d kernel stride padding hKernel hStride) (input : Tensor α (Shape.ofList inSpatial.toList)) :
                                                        Tensor α (Shape.ofList (poolOutSpatialPad inSpatial kernel stride padding).toList)

                                                        N-D average pooling on a spatial tensor (no explicit channel axis).

                                                        Instances For

                                                          Backward (single-channel spatial tensor) #

                                                          These are the VJPs of the forward pooling specs above.

                                                          Conventions:

                                                          def Spec.maxPoolSpatialBackwardSpec {α : Type} [Context α] {d : } {inSpatial kernel stride padding : Vector d} {hKernel : ∀ (i : Fin d), kernel.get i 0} {hStride : ∀ (i : Fin d), stride.get i 0} (layer : MaxPoolSpec d kernel stride padding hKernel hStride) (input : Tensor α (Shape.ofList inSpatial.toList)) (grad_output : Tensor α (Shape.ofList (poolOutSpatialPad inSpatial kernel stride padding).toList)) :
                                                          Tensor α (Shape.ofList inSpatial.toList)

                                                          Backward/VJP for max_pool_spatial_spec.

                                                          Each output gradient is propagated to the argmax location in the corresponding input window. Ties keep the first position in row-major order.

                                                          Instances For
                                                            def Spec.avgPoolSpatialBackwardSpec {α : Type} [Context α] {d : } {inSpatial kernel stride padding : Vector d} {hKernel : ∀ (i : Fin d), kernel.get i 0} {hStride : ∀ (i : Fin d), stride.get i 0} (_layer : AvgPoolSpec d kernel stride padding hKernel hStride) (grad_output : Tensor α (Shape.ofList (poolOutSpatialPad inSpatial kernel stride padding).toList)) :
                                                            Tensor α (Shape.ofList inSpatial.toList)

                                                            Backward/VJP for avg_pool_spatial_spec (single-channel).

                                                            Each output gradient is evenly distributed across its kernel window.

                                                            Instances For

                                                              Forward (channels-first: C × spatial...) #

                                                              def Spec.maxPoolSpec {α : Type} [Context α] {d C : } {inSpatial kernel stride padding : Vector d} {hKernel : ∀ (i : Fin d), kernel.get i 0} {hStride : ∀ (i : Fin d), stride.get i 0} (layer : MaxPoolSpec d kernel stride padding hKernel hStride) (input : Tensor α (Shape.ofList (C :: inSpatial.toList))) :
                                                              Tensor α (Shape.ofList (C :: (poolOutSpatialPad inSpatial kernel stride padding).toList))

                                                              N-D max pooling on a channels-first tensor: shape [C] ++ spatial.

                                                              Instances For
                                                                def Spec.maxPoolLinearizationSpec {α : Type} [Context α] {d C : } {inSpatial kernel stride padding : Vector d} {hKernel : ∀ (i : Fin d), kernel.get i 0} {hStride : ∀ (i : Fin d), stride.get i 0} (layer : MaxPoolSpec d kernel stride padding hKernel hStride) (input tangent : Tensor α (Shape.ofList (C :: inSpatial.toList))) :
                                                                Tensor α (Shape.ofList (C :: (poolOutSpatialPad inSpatial kernel stride padding).toList))

                                                                N-D hard max-pool selected-branch linearization, applied channel-wise.

                                                                Instances For
                                                                  def Spec.avgPoolSpec {α : Type} [Context α] {d C : } {inSpatial kernel stride padding : Vector d} {hKernel : ∀ (i : Fin d), kernel.get i 0} {hStride : ∀ (i : Fin d), stride.get i 0} (layer : AvgPoolSpec d kernel stride padding hKernel hStride) (input : Tensor α (Shape.ofList (C :: inSpatial.toList))) :
                                                                  Tensor α (Shape.ofList (C :: (poolOutSpatialPad inSpatial kernel stride padding).toList))

                                                                  N-D average pooling on a channels-first tensor: shape [C] ++ spatial.

                                                                  Instances For

                                                                    Backward (channels-first: C × spatial...) #

                                                                    def Spec.maxPoolBackwardSpec {α : Type} [Context α] {d C : } {inSpatial kernel stride padding : Vector d} {hKernel : ∀ (i : Fin d), kernel.get i 0} {hStride : ∀ (i : Fin d), stride.get i 0} (layer : MaxPoolSpec d kernel stride padding hKernel hStride) (input : Tensor α (Shape.ofList (C :: inSpatial.toList))) (grad_output : Tensor α (Shape.ofList (C :: (poolOutSpatialPad inSpatial kernel stride padding).toList))) :
                                                                    Tensor α (Shape.ofList (C :: inSpatial.toList))

                                                                    Multi-channel VJP for max_pool_spec (apply spatial backward per channel).

                                                                    Instances For
                                                                      def Spec.avgPoolBackwardSpec {α : Type} [Context α] {d C : } {inSpatial kernel stride padding : Vector d} {hKernel : ∀ (i : Fin d), kernel.get i 0} {hStride : ∀ (i : Fin d), stride.get i 0} (layer : AvgPoolSpec d kernel stride padding hKernel hStride) (grad_output : Tensor α (Shape.ofList (C :: (poolOutSpatialPad inSpatial kernel stride padding).toList))) :
                                                                      Tensor α (Shape.ofList (C :: inSpatial.toList))

                                                                      Multi-channel VJP for avg_pool_spec (apply spatial backward per channel).

                                                                      Instances For

                                                                        Smooth max pooling (log-sum-exp surrogate) #

                                                                        def Spec.smoothMaxPoolSpatialSpec {α : Type} [Context α] {d : } {inSpatial kernel stride padding : Vector d} {hKernel : ∀ (i : Fin d), kernel.get i 0} {hStride : ∀ (i : Fin d), stride.get i 0} (_layer : MaxPoolSpec d kernel stride padding hKernel hStride) (beta : α) (input : Tensor α (Shape.ofList inSpatial.toList)) :
                                                                        Tensor α (Shape.ofList (poolOutSpatialPad inSpatial kernel stride padding).toList)

                                                                        Smooth log-sum-exp max pooling on a spatial tensor (no explicit channel axis).

                                                                        Instances For
                                                                          def Spec.smoothMaxPoolSpatialJvpSpec {α : Type} [Context α] {d : } {inSpatial kernel stride padding : Vector d} {hKernel : ∀ (i : Fin d), kernel.get i 0} {hStride : ∀ (i : Fin d), stride.get i 0} (_layer : MaxPoolSpec d kernel stride padding hKernel hStride) (beta : α) (input tangent : Tensor α (Shape.ofList inSpatial.toList)) :
                                                                          Tensor α (Shape.ofList (poolOutSpatialPad inSpatial kernel stride padding).toList)

                                                                          Forward-mode JVP for N-D smooth max-pooling on a spatial tensor.

                                                                          For the log-sum-exp surrogate this is the softmax-weighted sum of the input tangent over each window. It is the forward-mode counterpart of smoothMaxPoolSpatialBackwardSpec.

                                                                          Instances For
                                                                            def Spec.smoothMaxPoolSpec {α : Type} [Context α] {d C : } {inSpatial kernel stride padding : Vector d} {hKernel : ∀ (i : Fin d), kernel.get i 0} {hStride : ∀ (i : Fin d), stride.get i 0} (layer : MaxPoolSpec d kernel stride padding hKernel hStride) (beta : α) (input : Tensor α (Shape.ofList (C :: inSpatial.toList))) :
                                                                            Tensor α (Shape.ofList (C :: (poolOutSpatialPad inSpatial kernel stride padding).toList))

                                                                            Smooth log-sum-exp max pooling on a channels-first tensor (channel-wise application).

                                                                            Instances For
                                                                              def Spec.smoothMaxPoolJvpSpec {α : Type} [Context α] {d C : } {inSpatial kernel stride padding : Vector d} {hKernel : ∀ (i : Fin d), kernel.get i 0} {hStride : ∀ (i : Fin d), stride.get i 0} (layer : MaxPoolSpec d kernel stride padding hKernel hStride) (beta : α) (input tangent : Tensor α (Shape.ofList (C :: inSpatial.toList))) :
                                                                              Tensor α (Shape.ofList (C :: (poolOutSpatialPad inSpatial kernel stride padding).toList))

                                                                              N-D smooth max-pool JVP on a channels-first tensor (channel-wise application).

                                                                              Instances For

                                                                                Smooth max pooling backward #

                                                                                def Spec.smoothMaxPoolSpatialBackwardSpec {α : Type} [Context α] {d : } {inSpatial kernel stride padding : Vector d} {hKernel : ∀ (i : Fin d), kernel.get i 0} {hStride : ∀ (i : Fin d), stride.get i 0} (_layer : MaxPoolSpec d kernel stride padding hKernel hStride) (beta : α) (input : Tensor α (Shape.ofList inSpatial.toList)) (grad_output : Tensor α (Shape.ofList (poolOutSpatialPad inSpatial kernel stride padding).toList)) :
                                                                                Tensor α (Shape.ofList inSpatial.toList)

                                                                                Backward/VJP for smooth_max_pool_spatial_spec (log-sum-exp surrogate).

                                                                                For a window x₁,…,xₙ, the surrogate is:

                                                                                y = (1/beta) * log(∑ exp(beta*xᵢ))

                                                                                and the VJP distributes upstream gradient proportionally to exp(beta*xᵢ). The implementation evaluates the equivalent max/min-shifted weights so large finite inputs do not overflow before normalization.

                                                                                Instances For
                                                                                  def Spec.smoothMaxPoolBackwardSpec {α : Type} [Context α] {d C : } {inSpatial kernel stride padding : Vector d} {hKernel : ∀ (i : Fin d), kernel.get i 0} {hStride : ∀ (i : Fin d), stride.get i 0} (layer : MaxPoolSpec d kernel stride padding hKernel hStride) (beta : α) (input : Tensor α (Shape.ofList (C :: inSpatial.toList))) (grad_output : Tensor α (Shape.ofList (C :: (poolOutSpatialPad inSpatial kernel stride padding).toList))) :
                                                                                  Tensor α (Shape.ofList (C :: inSpatial.toList))

                                                                                  Multi-channel VJP for smooth_max_pool_spec (apply spatial backward per channel).

                                                                                  Instances For