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.

def TorchLean.Tensor.maxAbs {α : Type} [Storage α] [MathFunctions α] [BEq α] [Max α] [Zero α] {shape : Shape} (tensor : Tensor α shape) : α

Largest absolute entry, or zero for an empty tensor. Self-unequal values are propagated: for IEEE scalars this prevents a NaN from being hidden by the scalar max operation.

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.

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.

def TorchLean.Tensor.meanSquaredError {α : Type} [Storage α] [Add α] [Sub α] [Mul α] [Div α] [Zero α] [NatCast α] {shape : Shape} (predicted target : Tensor α shape) : α

Mean squared difference between two equally shaped tensors.