Commit 2025-01-07 17:42 3e203da7

View on Github →

feat: results on inner regularity of finite measures (#19780) in a PseudoEMetricSpace and CompleteSpace with SecondCountableTopology, any finite measure is inner regular with respect to compact sets. In other words, finite measures are tight. Important result in probability

Estimated changes

Modified Mathlib.lean

Modified Mathlib/MeasureTheory/Measure/MeasureSpace.lean

added theorem MeasureTheory.exists_measure_iInter_lt

Created Mathlib/MeasureTheory/Measure/RegularityCompacts.lean

added theorem MeasureTheory.PolishSpace.innerRegular_isCompact_isClosed_measurableSet

added theorem MeasureTheory.exists_isCompact_closure_measure_compl_lt

added theorem MeasureTheory.innerRegularWRT_isCompact

added theorem MeasureTheory.innerRegularWRT_isCompact_closure

added theorem MeasureTheory.innerRegularWRT_isCompact_closure_iff

added theorem MeasureTheory.innerRegularWRT_isCompact_closure_of_univ

added theorem MeasureTheory.innerRegularWRT_isCompact_isClosed

added theorem MeasureTheory.innerRegularWRT_isCompact_isClosed_iff

added theorem MeasureTheory.innerRegularWRT_isCompact_isClosed_iff_innerRegularWRT_isCompact_closure

added theorem MeasureTheory.innerRegularWRT_isCompact_isClosed_isOpen

added theorem MeasureTheory.innerRegularWRT_isCompact_isOpen

added theorem MeasureTheory.innerRegularWRT_of_exists_compl_lt

added theorem MeasureTheory.innerRegular_isCompact_isClosed_measurableSet_of_finite

Modified Mathlib/Topology/Instances/ENNReal.lean

added theorem ENNReal.tendsto_atTop_zero_iff_le_of_antitone

added theorem ENNReal.tendsto_atTop_zero_iff_lt_of_antitone

Modified Mathlib/Topology/UniformSpace/Cauchy.lean

added def interUnionBalls

added theorem isCompact_closure_interUnionBalls

added theorem totallyBounded_interUnionBalls