Commit 2024-10-17 03:45 b1267a6b

View on Github →

feat: sigma-algebra of cylinder events (#17833) From GibbsMeasure

Estimated changes

Modified Mathlib/MeasureTheory/Constructions/Cylinders.lean

added theorem MeasureTheory.Measurable.eval_cylinderEvents

added def MeasureTheory.cylinderEvents

added theorem MeasureTheory.cylinderEvents_le_pi

added theorem MeasureTheory.cylinderEvents_mono

added theorem MeasureTheory.cylinderEvents_univ

added theorem MeasureTheory.measurable_cylinderEvent_apply

added theorem MeasureTheory.measurable_cylinderEvents_iff

added theorem MeasureTheory.measurable_cylinderEvents_lambda

added theorem MeasureTheory.measurable_restrict_cylinderEvents

added theorem MeasureTheory.measurable_uniqueElim_cylinderEvents

added theorem MeasureTheory.measurable_update_cylinderEvents'

added theorem MeasureTheory.measurable_update_cylinderEvents

added theorem MeasureTheory.measurable_update_cylinderEvents_left