Mean-reduction adjoint

Mean reduction and its reverse map are adjoint for every finite coordinate map whose fibers are nonempty.

def TorchLean.Tensor.Internal.Rep.meanReduceVjp {R : Type u} [Storage R] [DivisionRing R] {s t : Shape} (f : Coord s → Coord t) (outputCotangent : Rep R t) : Rep R s

The reverse map for mean reduction divides each output cotangent by the cardinality of the input fiber to which it is broadcast.

The definition is geometric: it depends only on the coordinate map and not on the primal tensor. Nonemptiness and characteristic zero are needed by the forward mean and its adjoint theorem, not to evaluate this map.

theorem TorchLean.Tensor.Internal.Rep.dot_reduceNonempty_mean_eq_dot_meanReduceVjp {R : Type u} [Storage R] [DivisionRing R] [CharZero R] {s t : Shape} (f : Coord s → Coord t) (fiberNonempty : ∀ (outputCoordinate : Coord t), 0 < Fintype.card (Fiber f outputCoordinate)) (inputTangent : Rep R s) (outputCotangent : Rep R t) : (reduceNonempty Reduction.mean f fiberNonempty inputTangent).dot outputCotangent = inputTangent.dot (meanReduceVjp f outputCotangent)

Mean reduction and meanReduceVjp are adjoint under the finite tensor pairing.

This is a theorem for every finite coordinate map, not only maps produced by einops. The positive-cardinality premise rules out empty means. The proof partitions the input pairing into the same fibers used by the forward reduction and does not assume commutative multiplication.