Pushforward Composition

Abstract

Indicator-weighted fiber sums compose over any additive commutative monoid.

The frozen module Entropy/Forgetting/CapacityMonotone defines pushforward f p as fun y => sum x, if f x = y then p x else 0, for [Fintype X], and it is imported here. Only the source type is finite; the target carries no finiteness.

sum_indicator_comp is the indicator-weighted form of Mathlib’s Finset.sum_fiberwise_eq_sum_filter, obtained from it by taking the target index set to be the fiber of g over target. The mathematical content is Mathlib’s. What this module supplies is the bridge between that filter form and the indicator-weighted idiom used throughout this development, and the named consequence for pushforward.

Four modules each carry a private copy of the real-valued statement: Entropy/Forgetting/CompletionEntropyMinimality, Entropy/Observation/CompletionInformationChainDecomposition, Entropy/Observation/MultiTargetInformationChain, and Entropy/Submodularity/RefinementInformationDecomposition. They state the same proposition up to the names of the type variables and the functions, and their proofs follow the same route with small differences in the simp set: the same statement, proved four times.

All four modules are frozen, and so is CapacityMonotone. Being frozen, none of them can import this module, and this change removes none of the four copies.

This module has zero consumers today. It does not promise to prevent a future copy.

The value is API, not mathematical novelty. pushforward_comp unfolds the definition and applies sum_indicator_comp, which in turn applies Mathlib’s fiberwise summation lemma.

Prior art in pinned Mathlib: Finset.sum_fiberwise_eq_sum_filter, in Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean, states the fiberwise decomposition over an arbitrary commutative monoid. It is generated by to_additive from prod_fiberwise_eq_prod_filter, so no declaration line carries the additive name: a name search restricted to declaration keywords misses it, while a plain name search finds it at its use sites. sum_indicator_comp applies that lemma rather than reproving it.

Theorem 1.1 (Indicator-weighted finite sums compose).

$$\begin{array}{r}\forall X,Y,Z,M:Type,\\ [Fintype\left(X\right)],[Fintype\left(Y\right)],[AddCommMonoid\left(M\right)],\\ \forall p:X\to M,f:X\to Y,\\ \forall g:Y\to Z,target:Z,\\ \sum _y(\text{if}g\left(y\right)=target\text{then}\sum _x(\text{if}f\left(x\right)=y\text{then}p\left(x\right)\text{else}0)\text{else}0)=\sum _x(\text{if}g\left(f\left(x\right)\right)=target\text{then}p\left(x\right)\text{else}0).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Entropy/Forgetting/PushforwardComposition.sum_indicator_comp (✓ std3). ∎

Source. Repository-derived.

Commentary.

The types X, Y, Z, and M are arbitrary. Only X and Y are finite, and M is an additive commutative monoid. For arbitrary p, f, g, and target, the outer indicator and the inner fiber indicator collapse to the indicator for the composite fiber. There are no further hypotheses.

Theorem 1.2 (Pushforwards compose).

$$\begin{array}{r}\forall X,Y,Z:Type,\\ [Fintype\left(X\right)],[Fintype\left(Y\right)],\\ \forall p:X\to \mathbb{R},f:X\to Y,\\ \forall g:Y\to Z,\\ pushforward\left(g,pushforward\left(f,p\right)\right)=pushforward\left(g\circ f,p\right).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Entropy/Forgetting/PushforwardComposition.pushforward_comp (✓ std3). ∎

Source. Repository-derived.

Commentary.

For finite X and Y, a real-valued function p can be pushed first through f and then through g, or directly through their composite. There are no hypotheses on p, and Z has no Fintype instance.

References

• Truth anchor: D5/S3/Entropy/Forgetting/PushforwardComposition.pushforward_comp
• Truth anchor: D5/S3/Entropy/Forgetting/PushforwardComposition.sum_indicator_comp
• Dependency: D5/S3/Entropy/Forgetting/CapacityMonotone