Commit 2023-11-30 18:08 7a22f15e

View on Github →

feat: define the marginal of a function (#8379)

This is a convenient way to work with iterated integrals and apply Fubini's theorem, without requiring the hassle of working with measurable equivalences.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Finset/Update.lean

added theorem Function.updateFinset_def

Modified Mathlib/MeasureTheory/Constructions/Pi.lean

Created Mathlib/MeasureTheory/Integral/Marginal.lean

added theorem Measurable.lmarginal

added theorem MeasureTheory.lintegral_eq_lmarginal_univ

added theorem MeasureTheory.lintegral_eq_of_lmarginal_eq

added theorem MeasureTheory.lintegral_le_of_lmarginal_le

added def MeasureTheory.lmarginal

added theorem MeasureTheory.lmarginal_congr

added theorem MeasureTheory.lmarginal_empty

added theorem MeasureTheory.lmarginal_eq_of_subset

added theorem MeasureTheory.lmarginal_erase'

added theorem MeasureTheory.lmarginal_erase

added theorem MeasureTheory.lmarginal_image

added theorem MeasureTheory.lmarginal_insert'

added theorem MeasureTheory.lmarginal_insert

added theorem MeasureTheory.lmarginal_le_of_subset

added theorem MeasureTheory.lmarginal_mono

added theorem MeasureTheory.lmarginal_singleton

added theorem MeasureTheory.lmarginal_union'

added theorem MeasureTheory.lmarginal_union

added theorem MeasureTheory.lmarginal_univ

added theorem MeasureTheory.lmarginal_update_of_mem

added theorem MeasureTheory.lmarginal_update_of_not_mem