Commit 2024-08-16 08:13 c9122d8d

View on Github →

chore: a clean-up of files on finite measures, probability measures, and portmanteau theorem (#12822)

Estimated changes

Modified Mathlib/MeasureTheory/Measure/FiniteMeasure.lean

modified theorem MeasureTheory.FiniteMeasure.apply_mono

modified theorem MeasureTheory.FiniteMeasure.continuous_mass

modified def MeasureTheory.FiniteMeasure.mass

modified theorem MeasureTheory.FiniteMeasure.mass_nonzero_iff

added theorem MeasureTheory.FiniteMeasure.null_iff_toMeasure_null

added theorem MeasureTheory.FiniteMeasure.tendsto_iff_weakDual_tendsto

deleted theorem MeasureTheory.FiniteMeasure.tendsto_iff_weak_star_tendsto

modified theorem MeasureTheory.FiniteMeasure.toMeasure_add

modified theorem MeasureTheory.FiniteMeasure.toMeasure_zero

modified theorem MeasureTheory.FiniteMeasure.val_eq_toMeasure

modified theorem MeasureTheory.FiniteMeasure.zero_mass

Modified Mathlib/MeasureTheory/Measure/Portmanteau.lean

Modified Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean

added theorem MeasureTheory.ProbabilityMeasure.null_iff_toMeasure_null

modified def MeasureTheory.ProbabilityMeasure.toFiniteMeasure

modified theorem MeasureTheory.ProbabilityMeasure.toWeakDualBCNN_continuous

modified theorem MeasureTheory.ProbabilityMeasure.val_eq_to_measure