Commit 2023-09-29 06:57 c0af8b81

View on Github →

feat: add standard Borel space class (#7243) add a class StandardBorelSpace, whose relationship to PolishSpace is analogous to the relationship between PolishSpace and complete metric space. The usefulness is shown by _root_.MeasurableSet.standardBorel: A measurable subset of a standard Borel space is Polish. Note that a borel measurable subset of a Polish space will not typically be Polish in the induced topology! Specific things done in this PR:

added some basic instances for StandardBorelSpace
changed theorems with hypotheses [MeasurableSpace X] [TopologicalSpace X] [BorelSpace X] [PolishSpace X] but which do not refer to the topology on X to depend instead on [MeasurableSpace X][StandardBorelSpace X]. These automatically generalize the old theorems thanks to standardBorel_of_polish. I believe this sort of refactoring can be pushed a lot farther in future PRs.

Estimated changes

Modified Mathlib/MeasureTheory/Constructions/Polish.lean

modified theorem Continuous.measurableEmbedding

modified theorem ContinuousOn.measurableEmbedding

modified theorem IsClosed.measurableSet_image_of_continuousOn_injOn

modified theorem Measurable.measurableEmbedding

modified theorem MeasurableSet.analyticSet_image

modified theorem MeasurableSet.image_of_continuousOn_injOn

modified theorem MeasurableSet.image_of_measurable_injOn

added theorem MeasurableSet.isClopenable'

added theorem MeasurableSet.standardBorel

added theorem MeasureTheory.borel_eq_borel_of_le

modified theorem MeasureTheory.isClopenable_iff_measurableSet

modified theorem MeasureTheory.measurableSet_exists_tendsto

modified theorem MeasureTheory.measurableSet_range_of_continuous_injective

added theorem eq_borel_upgradeStandardBorel

added def upgradeStandardBorel

Modified Mathlib/Probability/Martingale/Convergence.lean

Modified Mathlib/Topology/MetricSpace/Polish.lean