Shape-changing eager-engine operations.

This module implements reshape, transpose, broadcast, slice, gather/scatter, and related view-style nodes while preserving the graph metadata needed by autograd.

def Runtime.Autograd.Tape.flatten {α : Type} [TorchLean.Storage α] [Inhabited α] {s : Spec.Shape} (t : Tape α) (xId : ℕ) : Result (Tape α × ℕ)

Flatten a tensor s into a 1D vector of length Spec.Shape.size s.

PyTorch comparison: torch.flatten(x) with start_dim=0.

def Runtime.Autograd.Tape.reshape {α : Type} [TorchLean.Storage α] [Inhabited α] {s₁ s₂ : Spec.Shape} (t : Tape α) (xId : ℕ) (h : s₁.size = s₂.size) : Result (Tape α × ℕ)

Reshape a tensor while preserving number of elements.

The proof argument h enforces Spec.Shape.size s₁ = Spec.Shape.size s₂. PyTorch comparison: x.reshape(new_shape) / x.view(new_shape) (when valid).

def Runtime.Autograd.Tape.swapAdjacentAtDepth {α : Type} [TorchLean.Storage α] {s : Spec.Shape} (t : Tape α) (depth xId : ℕ) : Result (Tape α × ℕ)

Swap adjacent axes at a given depth inside a general Shape.

General permutations and arbitrary-axis transpose are lowered to this operation.

def Runtime.Autograd.Tape.broadcastTo {α : Type} [TorchLean.Storage α] [Inhabited α] [Add α] [Zero α] {s₁ s₂ : Spec.Shape} (cb : s₁.CanBroadcastTo s₂) (t : Tape α) (xId : ℕ) : Result (Tape α × ℕ)

Broadcast x : s₁ to s₂ using a proof Shape.CanBroadcastTo s₁ s₂.

PyTorch comparison: implicit broadcasting / x.expand(...).

def Runtime.Autograd.Tape.reduceSum {α : Type} [TorchLean.Storage α] [Add α] [Zero α] [Inhabited α] {s : Spec.Shape} (axis : ℕ) [_valid : Spec.Shape.HasNonemptyAxis axis s] [_wf : s.WellFormed] (t : Tape α) (xId : ℕ) : Result (Tape α × ℕ)

Sum-reduce along axis.

PyTorch comparison: torch.sum(x, dim=axis).

def Runtime.Autograd.Tape.reduceMean {α : Type} [TorchLean.Storage α] [Context α] {s : Spec.Shape} (axis : ℕ) [valid : Spec.Shape.HasNonemptyAxis axis s] [_wf : s.WellFormed] (t : Tape α) (xId : ℕ) : Result (Tape α × ℕ)

Mean-reduce along axis.

Backward rule: broadcast the upstream cotangent back to s and divide by the reduced dimension. PyTorch comparison: torch.mean(x, dim=axis).