Commit 2025-02-25 17:02 b1df36da

View on Github →

feat(MeasureTheory): define an additive content from a projective family of measures (#22271) This will be used to build projective limits of families of measures in both the Ionescu-Tulcea and the Kolmogorov extension theorems.

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Constructions/ProjectiveFamilyContent.lean

added theorem MeasureTheory.isSetAlgebra_measurableCylinders

added theorem MeasureTheory.isSetRing_measurableCylinders

added theorem MeasureTheory.isSetSemiring_measurableCylinders

added theorem MeasureTheory.projectiveFamilyContent_congr

added theorem MeasureTheory.projectiveFamilyContent_cylinder

added theorem MeasureTheory.projectiveFamilyContent_diff

added theorem MeasureTheory.projectiveFamilyContent_diff_of_subset

added theorem MeasureTheory.projectiveFamilyContent_eq

added theorem MeasureTheory.projectiveFamilyContent_iUnion_le

added theorem MeasureTheory.projectiveFamilyContent_mono

added theorem MeasureTheory.projectiveFamilyContent_ne_top

added theorem MeasureTheory.projectiveFamilyFun_congr

added theorem MeasureTheory.projectiveFamilyFun_empty

added theorem MeasureTheory.projectiveFamilyFun_union