Commit 2024-03-17 14:50 0a75699a

View on Github →

feat: Levy-Prokhorov topology is finer than convergence in distribution (#10406) This PR establishes an easy topology comparison: the topology given by the Lévy-Prokhorov distance is finer than the topology of convergence in distribution.

Estimated changes

Modified Mathlib/MeasureTheory/Integral/BoundedContinuousFunction.lean

added theorem BoundedContinuousFunction.tendsto_integral_of_forall_integral_le_liminf_integral

added theorem BoundedContinuousFunction.tendsto_integral_of_forall_limsup_integral_le_integral

Modified Mathlib/MeasureTheory/Integral/IntegrableOn.lean

added theorem MeasureTheory.Measure.integrableOn_of_bounded

Modified Mathlib/MeasureTheory/Integral/Layercake.lean

added theorem MeasureTheory.Integrable.integral_eq_integral_Ioc_meas_le

added theorem MeasureTheory.Integrable.integral_eq_integral_meas_le

Modified Mathlib/MeasureTheory/Measure/LevyProkhorovMetric.lean

added theorem MeasureTheory.BoundedContinuousFunction.integral_eq_integral_meas_le

added theorem MeasureTheory.BoundedContinuousFunction.integral_eq_integral_meas_le_of_hasFiniteIntegral

added theorem MeasureTheory.BoundedContinuousFunction.integral_le_of_levyProkhorovEDist_lt

added theorem MeasureTheory.LevyProkhorov.dist_def

added def MeasureTheory.LevyProkhorov.finiteMeasure

added def MeasureTheory.LevyProkhorov.probabilityMeasure

added theorem MeasureTheory.continuous_levyProkhorov_to_probabilityMeasure

added theorem MeasureTheory.levyProkhorovEDist_ne_top

added theorem MeasureTheory.levyProkhorov_le_convergenceInDistribution

added theorem MeasureTheory.tendsto_integral_meas_thickening_le

Modified Mathlib/MeasureTheory/Measure/Portmanteau.lean

deleted theorem MeasureTheory.tendsto_integral_of_forall_integral_le_liminf_integral