Equal-share tie rules

For attained-value reducers such as minimum and maximum, this module specifies and proves an explicit convention that distributes cotangents equally among tied coordinates.

def TorchLean.Tensor.Internal.Rep.equalShareTieWeight {R : Type u} [Storage R] [DivisionRing R] [DecidableEq R] {s t : Shape} (aggregate : (values : Multiset R) → values ≠ 0 → R) (f : Coord s → Coord t) (fiberNonempty : ∀ (outputCoordinate : Coord t), 0 < Fintype.card (Fiber f outputCoordinate)) (inputTensor : Rep R s) (outputCoordinate : Coord t) (inputCoordinate : Fiber f outputCoordinate) : R

The equal-share weight assigned to one coordinate tied at a reducer's output.

All coordinates in the fiber whose primal value equals the reduced value receive the reciprocal of their count; every other coordinate receives zero. The reducer is kept as an ordinary function, so the same convention can be used for minimum, maximum, or a custom attained-value reducer.

def TorchLean.Tensor.Internal.Rep.equalShareTieDifferential {R : Type u} [Storage R] [DivisionRing R] [DecidableEq R] {s t : Shape} (aggregate : (values : Multiset R) → values ≠ 0 → R) (f : Coord s → Coord t) (fiberNonempty : ∀ (outputCoordinate : Coord t), 0 < Fintype.card (Fiber f outputCoordinate)) (inputTensor inputTangent : Rep R s) : Rep R t

The equal-sharing linearization of a nonempty reduction at a fixed primal tensor.

When several coordinates attain the reduced value, their input tangents are averaged. For minimum and maximum this is an explicit tie convention, not a claim that the classical derivative is unique at a tie.

def TorchLean.Tensor.Internal.Rep.equalShareTieVjp {R : Type u} [Storage R] [DivisionRing R] [DecidableEq R] {s t : Shape} (aggregate : (values : Multiset R) → values ≠ 0 → R) (f : Coord s → Coord t) (fiberNonempty : ∀ (outputCoordinate : Coord t), 0 < Fintype.card (Fiber f outputCoordinate)) (inputTensor : Rep R s) (outputCotangent : Rep R t) : Rep R s

The reverse map adjoint to equalShareTieDifferential.

Each selected input receives the same fraction of its fiber's output cotangent; nonselected inputs receive zero.

theorem TorchLean.Tensor.Internal.Rep.sum_equalShareTieWeight {R : Type u} [Storage R] [DivisionRing R] [CharZero R] [DecidableEq R] {s t : Shape} (aggregate : (values : Multiset R) → values ≠ 0 → R) (aggregate_mem : ∀ (values : Multiset R) (hValues : values ≠ 0), aggregate values hValues ∈ values) (f : Coord s → Coord t) (fiberNonempty : ∀ (outputCoordinate : Coord t), 0 < Fintype.card (Fiber f outputCoordinate)) (inputTensor : Rep R s) (outputCoordinate : Coord t) : ∑ inputCoordinate : Fiber f outputCoordinate, equalShareTieWeight aggregate f fiberNonempty inputTensor outputCoordinate inputCoordinate = 1

If a reducer returns one of its input values, the equal-share weights in every nonempty fiber sum to one.

Reduction.min_mem and Reduction.max_mem provide the premise for minimum and maximum. Thus a tie among n extrema contributes exactly 1 / n at each selected coordinate and contributes total weight one.

theorem TorchLean.Tensor.Internal.Rep.dot_equalShareTieDifferential_eq_dot_equalShareTieVjp {R : Type u} [Storage R] [Field R] [DecidableEq R] {s t : Shape} (aggregate : (values : Multiset R) → values ≠ 0 → R) (f : Coord s → Coord t) (fiberNonempty : ∀ (outputCoordinate : Coord t), 0 < Fintype.card (Fiber f outputCoordinate)) (inputTensor inputTangent : Rep R s) (outputCotangent : Rep R t) : (equalShareTieDifferential aggregate f fiberNonempty inputTensor inputTangent).dot outputCotangent = inputTangent.dot (equalShareTieVjp aggregate f fiberNonempty inputTensor outputCotangent)

The equal-sharing differential and VJP are adjoint under the finite tensor pairing.

This is an algebraic identity for the named tie policy. At a minimum or maximum tie it describes one symmetric generalized derivative; it does not assert that the ordinary derivative exists there.