Eager Tensor Operations

PyTorch-style tensor operations recorded on the session's tape. Each one runs the CPU or the CUDA kernel of the operation, as the session's device selects, and preserves the typed TensorRef surface.

Pooling operations

def Runtime.Autograd.Torch.Internal.EagerSession.maxPool {α : Type} [TorchLean.Storage α] (s : EagerSession α) [Context α] {d C : ℕ} {inSpatial kernel stride padding : TorchLean.Tensor ℕ [d]} (x : TensorRef α (Spec.Shape.ofList (C :: inSpatial.to (List ℕ)))) : IO (TensorRef α (Spec.Shape.ofList (C :: (Spec.poolOutSpatialPad inSpatial kernel stride padding).to (List ℕ))))

N-D max pooling for channels-first tensors (C, spatial...) (no batch axis).

PyTorch comparison: torch.nn.functional.max_pool1d / max_pool2d / max_pool3d depending on the spatial rank d.

def Runtime.Autograd.Torch.Internal.EagerSession.avgPool {α : Type} [TorchLean.Storage α] (s : EagerSession α) [Context α] {d C : ℕ} {inSpatial kernel stride padding : TorchLean.Tensor ℕ [d]} (x : TensorRef α (Spec.Shape.ofList (C :: inSpatial.to (List ℕ)))) : IO (TensorRef α (Spec.Shape.ofList (C :: (Spec.poolOutSpatialPad inSpatial kernel stride padding).to (List ℕ))))

N-D average pooling for channels-first tensors (C, spatial...) (no batch axis).

PyTorch comparison: torch.nn.functional.avg_pool1d / avg_pool2d / avg_pool3d depending on the spatial rank d.

def Runtime.Autograd.Torch.Internal.EagerSession.smoothMaxPool {α : Type} [TorchLean.Storage α] [TensorTransfer α] (s : EagerSession α) [Context α] [DecidableEq α] {d C : ℕ} {inSpatial kernel stride padding : TorchLean.Tensor ℕ [d]} (x : TensorRef α (Spec.Shape.ofList (C :: inSpatial.to (List ℕ)))) (beta : α) : IO (TensorRef α (Spec.Shape.ofList (C :: (Spec.poolOutSpatialPad inSpatial kernel stride padding).to (List ℕ))))

N-D smooth max pooling (log-sum-exp surrogate) for channels-first tensors (C, spatial...).

This is a differentiable approximation to max pooling; PyTorch does not expose it as a single primitive, but it can be emulated with logsumexp over local windows. Executable backends require at least one spatial dimension and a finite, nonzero beta; evaluation uses an input-space max/min shift so the exponential weights remain stable for large finite values.