Commit 2023-12-20 13:11 905338fc

View on Github →

feat: projective families of measures and projective limits (#8933) Part of the formalization of the Kolmogorov Extension theorem.

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Constructions/Projective.lean

added theorem MeasureTheory.IsProjectiveLimit.isFiniteMeasure

added theorem MeasureTheory.IsProjectiveLimit.isProbabilityMeasure

added theorem MeasureTheory.IsProjectiveLimit.measure_cylinder

added theorem MeasureTheory.IsProjectiveLimit.measure_univ_eq

added theorem MeasureTheory.IsProjectiveLimit.measure_univ_unique

added theorem MeasureTheory.IsProjectiveLimit.unique

added def MeasureTheory.IsProjectiveLimit

added theorem MeasureTheory.IsProjectiveMeasureFamily.congr_cylinder

added theorem MeasureTheory.IsProjectiveMeasureFamily.congr_cylinder_of_subset

added theorem MeasureTheory.IsProjectiveMeasureFamily.measure_univ_eq

added theorem MeasureTheory.IsProjectiveMeasureFamily.measure_univ_eq_of_subset

added def MeasureTheory.IsProjectiveMeasureFamily