The batched 2×2 pool at a fixed selection — the per-example kit, lifted over the batch #
SmallParamGrad proves the chapter nets' loss gradients through their 2×2 pools by freezing each
pool's routing at a selection σ (one cell per window): the pool is then a gather, linear and
differentiable everywhere, and maxPool_relu_eventuallyEq_sel says the pooled ReLU IS that gather
along any parameter, near a point where every window is dead or tied only between twins. This file
is the same kit at the batched index N·(c·h·w): a selection per example (poolSelIdxB), the
selection and smoothness predicates per example (PoolSelDomB, MaxPool2SmoothUpToB), the pooled
batch as a gather (batchMap_maxPoolFlat_eq_gatherB), the germ along a parameter
(maxPoolB_relu_eventuallyEq_sel, row by row from the per-example lemma), and the render's pool
backward as the scatter at the first argmax (batchMapAux_maxPoolBackFlat_eq_selScatter), which is
what makes a batched step tie's pool cotangent the loss-gradient chain's at σ = argmax.
The pull-backs a batched chain needs that ParamGradNodes does not have are here too: through the
gather with the ReLU mask spelled reluMaskB (hasGradAt_gatherReluB), and through a batched dense
layer with its backward spelled rowDenseBackFlat (hasGradAt_denseB).
ReLU slices: it is coordinatewise.
Taking example r's slice is continuous (a reindex).
The flat batched index of the cell σ selects for pooled entry k: example k's row, and
poolSelIdx of that example's selection within it.
Equations
- Proofs.SmallParamGrad.poolSelIdxB N σ k = finProdFinEquiv ((finProdFinEquiv.symm k).1, Proofs.SmallParamGrad.poolSelIdx (σ (finProdFinEquiv.symm k).1) (finProdFinEquiv.symm k).2)
Instances For
Every example's selection names a maximum of every window of its slice.
Equations
- Proofs.SmallParamGrad.PoolSelDomB N σ u = ∀ (r : Fin N), Proofs.SmallParamGrad.PoolSelDom (σ r) (Proofs.StableHLO.batchSlice N (c * (2 * h) * (2 * w)) u r)
Instances For
The per-example first argmax is a selection of the batch.
Smooth, dead, or tied only between twins, in every example's windows; the twin relation
T r is that example's.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The pooled batch is the gather at σ wherever σ names a maximum of every window.
Along a parameter, ReLU then the batched 2×2 pool is the gather at a fixed selection.
Z θ is the batch's pool pre-activation as the parameter moves; at θ₀ it has no zero entry,
every example's windows are dead or tied only between that example's T-twins, σ names a
maximum of every window of its ReLU, and twins are equal at EVERY θ. Each example is
maxPool_relu_eventuallyEq_sel on its own slice; the batch is the conjunction over the
finitely many examples.
The batched scatter at example r is the per-example scatter of that example's slices.
maxPoolBackFlat is the flattened first-argmax routing maxPoolBackDenote.
The per-example pool backward is the scatter at the first argmax, at every point.
The render's batched pool backward (den maxPoolBackB) is the scatter at the per-example
first argmax, at every point, ties included — so a batched step tie's pool cotangent is the
loss-gradient chain's at that selection.
Through ReLU then a gather, off the ReLU kinks: the scatter along σ, then the mask
reluMaskB. hasGradAt_gatherRelu with its cotangent in the batched ties' spelling.
Through a batched dense layer: the backward is rowDenseBackFlat (den of .denseRowBack).