Spatial tensor utilities

Padding, indexing, and window-extraction operations used by convolution and pooling specifications. The signatures use Tensor directly; channels-first layout is visible in each shape rather than hidden behind a second family of tensor aliases.

def Spec.Private.smoothMaxPivotStep {α : Type} [Context α] (beta current candidate : α) : α

Choose the input-space pivot whose scaled value beta * pivot is maximal.

Selecting a maximum for positive beta and a minimum for negative beta avoids forming beta * x before the log-sum-exp shift. Both fixed-rank and dimension-polymorphic smooth pooling use this operation.

def Spec.getValueAtPosition {α : Type} [Context α] {H W : ℕ} (img : Tensor α (Shape.dim H (Shape.dim W Shape.scalar))) (x y : ℕ) : Tensor α Shape.scalar

Read position (x, y) from a rank-two tensor, returning 0 when out of bounds.

This helper is used by window-extraction and padding utilities for conv/pooling specs.

theorem Spec.get_at_or_zero_getValueAtPosition {α : Type} [Context α] {H W : ℕ} (img : Tensor α (Shape.dim H (Shape.dim W Shape.scalar))) (x y : ℕ) : getAtOrZero (getValueAtPosition img x y) [] = getAtOrZero img [x, y]

getValueAtPosition agrees with the generic list-indexing helper get_at_or_zero.

In particular, reading a scalar via the specialized (x, y) accessor is the same as reading with indices [x, y], where both return 0 out of bounds.

def Spec.extractWindow {α : Type} [Context α] {H W : ℕ} (kW kH : ℕ) (img : Tensor α (Shape.dim H (Shape.dim W Shape.scalar))) (start_i start_j : ℕ) : Tensor α (Shape.dim kH (Shape.dim kW Shape.scalar))

Extract a kH × kW patch from an image starting at (start_i, start_j).

Out-of-bounds pixels are treated as 0, matching the behavior of getValueAtPosition. This is spec-level "im2col"-style logic (cf. PyTorch nn.Unfold, conceptually).

def Spec.padMultiChannel {α : Type} [Context α] {inC inH inW : ℕ} (img : Tensor α (Shape.dim inC (Shape.dim inH (Shape.dim inW Shape.scalar)))) (padding : ℕ) : Tensor α (Shape.dim inC (Shape.dim (inH + 2 * padding) (Shape.dim (inW + 2 * padding) Shape.scalar)))

Zero-pad a channels-first image by padding pixels on each spatial axis.

This is the spec analogue of torch.nn.functional.pad (with constant 0 padding). The output shape is [inC, inH + 2*padding, inW + 2*padding].

theorem Spec.get_at_or_zero_pad_multi_channel {α : Type} [Context α] {inC inH inW padding : ℕ} (img : Tensor α (Shape.dim inC (Shape.dim inH (Shape.dim inW Shape.scalar)))) (c : Fin inC) (p q : ℕ) : getAtOrZero (padMultiChannel img padding) [↑c, p, q] = if _h : p < padding ∨ q < padding then 0 else getAtOrZero img [↑c, p - padding, q - padding]

Characterization lemma for pad_multi_channel under list-indexing (get_at_or_zero).

Reading the padded tensor at [c, p, q] yields 0 in the top/left padding region, and otherwise reads the original tensor at [c, p - padding, q - padding] (with out-of-bounds falling back to 0 on both sides).

theorem Spec.get_at_or_zero_pad_multi_channel_shift {α : Type} [Context α] {inC inH inW padding : ℕ} (img : Tensor α (Shape.dim inC (Shape.dim inH (Shape.dim inW Shape.scalar)))) (c : Fin inC) (i : Fin inH) (j : Fin inW) : getAtOrZero (padMultiChannel img padding) [↑c, ↑i + padding, ↑j + padding] = getAtOrZero img [↑c, ↑i, ↑j]

Index-shift lemma for pad_multi_channel.

If (i, j) is in-bounds for the original image, then reading the padded image at (i + padding, j + padding) returns the same value.

def Spec.extractMultiWindow {α : Type} [Context α] {inC kH kW inH inW padding : ℕ} (img : Tensor α (Shape.dim inC (Shape.dim (inH + 2 * padding) (Shape.dim (inW + 2 * padding) Shape.scalar)))) (start_i start_j : ℕ) : Tensor α (Shape.dim inC (Shape.dim kH (Shape.dim kW Shape.scalar)))

Extract a kH × kW window from each channel of a channels-first image.

The input is typically a padded image, and the result has shape [inC, kH, kW].

def Spec.padChannelsZero {α : Type} [Zero α] {inChannels outChannels height width : ℕ} (_h : inChannels ≤ outChannels) (img : Tensor α (Shape.dim inChannels (Shape.dim height (Shape.dim width Shape.scalar)))) : Tensor α (Shape.dim outChannels (Shape.dim height (Shape.dim width Shape.scalar)))

Increase the channel dimension by zero-padding extra channels.

This is used in some ResNet-style skip connections when inChannels < outChannels. Existing channels are copied; newly introduced channels are identically zero.

def Spec.setValueAtPosition {α : Type} {H W : ℕ} (img : Tensor α (Shape.dim H (Shape.dim W Shape.scalar))) (x y : ℕ) (value : α) : Tensor α (Shape.dim H (Shape.dim W Shape.scalar))

Write a value at pixel (x, y) if it is in-bounds; otherwise return the original image.

This uses update_tensor_spec under the hood and is intended for small spec-level utilities.

def Spec.addValueAtPosition {α : Type} [Add α] {H W : ℕ} (img : Tensor α (Shape.dim H (Shape.dim W Shape.scalar))) (x y : ℕ) (value : α) : Tensor α (Shape.dim H (Shape.dim W Shape.scalar))

Add value to pixel (x, y) if it is in-bounds; otherwise return the original image.

This is a small helper for accumulation-style specs (e.g. naive convolution).