Commit 2024-08-01 17:52 852c1ad8

View on Github →

feat: notations to specify sigma algebras for integrability, measures and kernels (#15316) from GibbsMeasure

Estimated changes

Modified Mathlib/MeasureTheory/Function/L1Space.lean

Modified Mathlib/MeasureTheory/MeasurableSpace/Defs.lean

Modified Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean

Modified Mathlib/Probability/Kernel/Basic.lean