Slice / gather / split operator bounds

This file provides IBP and affine transfer rules for a small subset of indexing-like operations:

• Slice: extract a contiguous range [start, stop) from a flattened tensor,
• Gather: select entries by a runtime array of static indices, and
• Split: split a flattened tensor into an array of parts.

Important limitation: this does not model tensor-valued index dtypes inside the differentiable graph (i.e. no PyTorch-style LongTensor indexing/gather/scatter driven by data tensors).

def NN.MLTheory.CROWN.Operators.Slice.getDimScalarFn {α : Type} [TorchLean.Storage α] {n : ℕ} (t : TorchLean.Tensor α [n]) : Fin n → TorchLean.Tensor α Spec.Shape.scalar

View a vector tensor through its leading-axis slices.

def NN.MLTheory.CROWN.Operators.Slice.ibpSlice? {α : Type} [TorchLean.Storage α] [Context α] (xB : FlatBox α) (start stop : ℕ) : Option (FlatBox α)

IBP for Slice: extract elements [start, stop) from a flattened vector. Slice is a linear operation, so bounds propagate exactly.

def NN.MLTheory.CROWN.Operators.Slice.ibpGather? {α : Type} [TorchLean.Storage α] [Context α] (xB : FlatBox α) (indices : Array ℕ) : Option (FlatBox α)

IBP for Gather: index into a vector using integer indices.

For input $x$ and a concrete index vector, the output satisfies $y_j=x_{\mathrm{indices}[j]}$. This is a permutation or selection.

def NN.MLTheory.CROWN.Operators.Slice.ibpSplit? {α : Type} [TorchLean.Storage α] [Context α] (xB : FlatBox α) (splitSizes : Array ℕ) : Option (Array (FlatBox α))

IBP for Split: split a rank-one tensor into multiple parts. Returns an array of FlatBox values, one for each split.

def NN.MLTheory.CROWN.Operators.Slice.affSlice? {α : Type} [TorchLean.Storage α] [Context α] {inDim outDim : ℕ} (start sliceSize : ℕ) (aff : AffineVec α inDim outDim) : Option (AffineVec α inDim sliceSize)

Affine bounds for Slice: extract a subvector of an affine form.

If the input represents $y=Ax+c$, slicing selects the corresponding rows of $A$ and entries of $c$.

def NN.MLTheory.CROWN.Operators.Slice.affGather? {α : Type} [TorchLean.Storage α] [Context α] {inDim outDim : ℕ} (indices : Array ℕ) (aff : AffineVec α inDim outDim) : Option (AffineVec α inDim indices.size)

Affine bounds for Gather: permute/select rows of affine form.

def NN.MLTheory.CROWN.Operators.Slice.derivSlice? {α : Type} [TorchLean.Storage α] [Context α] (dB : FlatBox α) (start stop : ℕ) : Option (FlatBox α)

Derivative bounds for Slice: derivatives just slice through.

def NN.MLTheory.CROWN.Operators.Slice.derivGather? {α : Type} [TorchLean.Storage α] [Context α] (dB : FlatBox α) (indices : Array ℕ) : Option (FlatBox α)

Derivative bounds for Gather: derivatives follow the same indexing.

def NN.MLTheory.CROWN.Operators.Slice.ibpConcat {α : Type} [TorchLean.Storage α] [Context α] (boxes : Array (FlatBox α)) : FlatBox α

Concatenate multiple FlatBoxes into one.