Public Tensor Reductions

Shape-polymorphic scalar reductions for ordinary tensor programs. Empty means use denominator one (meanDenominator), the same totalized convention as meanSpec and the loss layer.

@[inline]

def TorchLean.Tensor.foldl {α β : Type} [Storage α] {shape : Shape} (step : β → α → β) (initial : β) (tensor : Tensor α shape) : β

Traverse entries in row-major order without converting the buffer to an array.

The accumulator may have a different type from the entries and does not require a Storage instance. For a configured binary tensor, we can accumulate in native binary32 without allocating a converted tensor:

let total := tensor.foldl
  (fun (total : Float32) value => total + FloatLib.Floats.ExecFloat.Binary.toFloat32 value) 0
let average := total / (Tensor.meanDenominator shape : Float32)

The conversion, additions, and final division use the chosen accumulator's arithmetic. Widening does not make those operations exact or prevent overflow for every input.

def TorchLean.Tensor.maxAbsDiff {α : Type} [Storage α] [MathFunctions α] [BEq α] [Max α] [Zero α] [Sub α] {shape : Shape} (actual expected : Tensor α shape) : α

Maximum absolute entrywise difference, with the exceptional-value policy of maxAbs.

@[reducible, inline]

abbrev TorchLean.Tensor.sum {α : Type} [Storage α] [Add α] [Zero α] {shape : Shape} (tensor : Tensor α shape) : α

Add every tensor entry in row-major order. Public spelling of sumSpec.

def TorchLean.Tensor.mean {α : Type} [Storage α] [Add α] [Zero α] [Div α] [NatCast α] {shape : Shape} (tensor : Tensor α shape) : α

Arithmetic mean of all entries, using denominator one for an empty tensor.

The sum and element-count conversion both use the tensor's scalar type. Either can overflow in a low-precision format even when the exact mean is representable. To select a wider accumulator, convert the entries with Tensor.map before calling mean, or convert them inside Tensor.foldl to accumulate in one pass. The latter also avoids allocating a wider tensor.

theorem TorchLean.Tensor.mean_eq_meanSpec {α : Type} [Storage α] [Context α] {shape : Shape} (tensor : Tensor α shape) : tensor.mean = tensor.meanSpec

Under a full scalar Context, the public mean is the specification mean.