feat(Probability): add PMF lemmas for maps, products, and failure bounds - #1063

Closed

SamuelSchlesinger wants to merge 3 commits into

samschles/crypto-pr-01-pmf-real-sumsfrom

samschles/crypto-pr-02-pmf-maps-products

Commits on Oct 4, 2026

feat(Probability): add PMF lemmas for maps, products, and failure bounds
SamuelSchlesinger
committed
afe3028
style(Probability): unsqueeze terminal simps in PMF map and product lemmas
SamuelSchlesinger
committed
2e0b6d9
style(Probability): use DFunLike.congr_fun in map_injective
SamuelSchlesinger
committed
4b3ff93