Scalar aggregation for tensor reduction

This module defines the einops aggregates that do not already have canonical mathlib names. Multiset.sum and Multiset.prod are used directly.

Boolean any and all are total and use the usual empty identities false and true. Exact mean, min, and max take evidence that their input multiset is nonempty. The lowering layer obtains that evidence from the checked tensor shape, independently of tensor values.

def TorchLean.Tensor.Internal.Reduction.any (values : Multiset Bool) : Bool

Boolean disjunction over a multiset; the empty result is false.

def TorchLean.Tensor.Internal.Reduction.all (values : Multiset Bool) : Bool

Boolean conjunction over a multiset; the empty result is true.

def TorchLean.Tensor.Internal.Reduction.mean {α : Type u} [DivisionRing α] [CharZero α] (values : Multiset α) (_hValues : values ≠ 0) : α

The exact arithmetic mean of a nonempty multiset.

DivisionRing permits noncommutative multiplication because averaging uses only addition and division by the natural-number cardinality. CharZero ensures a positive cardinality remains nonzero in the scalar type. Neither the nonemptiness evidence nor that instance is inspected by the formula; both are retained so that exactness is part of the aggregate's public contract rather than only a later theorem.

def TorchLean.Tensor.Internal.Reduction.min {α : Type u} [LinearOrder α] (values : Multiset α) (hValues : values ≠ 0) : α

The least value in a nonempty multiset.

theorem TorchLean.Tensor.Internal.Reduction.min_mem {α : Type u} [LinearOrder α] (values : Multiset α) (hValues : values ≠ 0) : min values hValues ∈ values

A minimum of a nonempty multiset is one of its values.

def TorchLean.Tensor.Internal.Reduction.max {α : Type u} [LinearOrder α] (values : Multiset α) (hValues : values ≠ 0) : α

The greatest value in a nonempty multiset.

theorem TorchLean.Tensor.Internal.Reduction.max_mem {α : Type u} [LinearOrder α] (values : Multiset α) (hValues : values ≠ 0) : max values hValues ∈ values

A maximum of a nonempty multiset is one of its values.