Commit 2024-02-17 14:51 778c315f

View on Github →

feat: Lévy-Prokhorov distance (#8719) This PR adds the Lévy-Prokhorov distance on the space of finite measures on an emetric space, and shows that it is a pseudoemetric.

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Measure/LevyProkhorovMetric.lean

added def MeasureTheory.LevyProkhorov

added theorem MeasureTheory.left_measure_le_of_levyProkhorovEDist_lt

added theorem MeasureTheory.levyProkhorovDist_comm

added theorem MeasureTheory.levyProkhorovDist_self

added theorem MeasureTheory.levyProkhorovDist_triangle

added theorem MeasureTheory.levyProkhorovEDist_comm

added theorem MeasureTheory.levyProkhorovEDist_le_max_measure_univ

added theorem MeasureTheory.levyProkhorovEDist_le_of_forall

added theorem MeasureTheory.levyProkhorovEDist_le_of_forall_add_pos_le

added theorem MeasureTheory.levyProkhorovEDist_lt_top

added theorem MeasureTheory.levyProkhorovEDist_self

added theorem MeasureTheory.levyProkhorovEDist_triangle

added theorem MeasureTheory.meas_le_of_le_of_forall_le_meas_thickening_add

added theorem MeasureTheory.right_measure_le_of_levyProkhorovEDist_lt