Singleton masses of a measure on a finite type #

Mathlib's MeasureTheory.sum_measureReal_singleton evaluates ∑ b ∈ s, μ.real {b} as μ.real ↑s for a Finset s. This module records the two specializations used throughout the library: over a Fintype the singleton masses of a probability measure sum to 1, and the singleton masses of a pushforward are the sums of the masses over the fibers.

Main statements #

• sum_measureReal_singleton_univ_eq_one — the singleton masses of a probability measure on a finite type sum to 1.
• map_real_singleton_fiber_sum — a singleton mass of a pushforward is the sum of the masses over the fiber above that point.

Implementation notes #

The module sits at the bottom of the import DAG — it depends only on Mathlib — so any file needing either identity can import it without pulling in information-theoretic material.