Commit 2025-10-29 22:11 810af946

View on Github →

chore(MeasureTheory): turn LevyProkhorov into a one-field structure (#30845) This caused some defeq abuse, notably in the homeo, where toFun and invFun were accidentally swapped!

Estimated changes

Modified Mathlib/MeasureTheory/Measure/LevyProkhorovMetric.lean

deleted theorem MeasureTheory.LevyProkhorov.continuous_equiv_probabilityMeasure

deleted theorem MeasureTheory.LevyProkhorov.continuous_equiv_symm_probabilityMeasure

added theorem MeasureTheory.LevyProkhorov.continuous_ofMeasure_probabilityMeasure

added theorem MeasureTheory.LevyProkhorov.continuous_toMeasure_probabilityMeasure

added def MeasureTheory.LevyProkhorov.delabOfMeasure

deleted theorem MeasureTheory.LevyProkhorov.dist_def

added theorem MeasureTheory.LevyProkhorov.dist_finiteMeasure_def

added theorem MeasureTheory.LevyProkhorov.dist_probabilityMeasure_def

added theorem MeasureTheory.LevyProkhorov.edist_finiteMeasure_def

added theorem MeasureTheory.LevyProkhorov.edist_measure_def

added theorem MeasureTheory.LevyProkhorov.edist_probabilityMeasure_def

added theorem MeasureTheory.LevyProkhorov.eq_convergenceInDistribution

deleted def MeasureTheory.LevyProkhorov.equiv

added theorem MeasureTheory.LevyProkhorov.le_convergenceInDistribution

added def MeasureTheory.LevyProkhorov.toMeasureEquiv

added theorem MeasureTheory.LevyProkhorov.toMeasure_injective

added structure MeasureTheory.LevyProkhorov

deleted def MeasureTheory.LevyProkhorov

modified theorem MeasureTheory.levyProkhorovEDist_lt_top

modified theorem MeasureTheory.levyProkhorovEDist_ne_top

modified theorem MeasureTheory.levyProkhorovEDist_self

deleted theorem MeasureTheory.levyProkhorov_eq_convergenceInDistribution

deleted theorem MeasureTheory.levyProkhorov_le_convergenceInDistribution