Commit 2025-11-28 15:51 7c89bb60

View on Github →

feat: universal property of weak convergence over a compact space (#32087) ... in terms of continuous maps

Estimated changes

Modified Mathlib/MeasureTheory/Measure/FiniteMeasure.lean

added theorem MeasureTheory.FiniteMeasure.continuous_iff_forall_continuousMap_continuous_integral

added theorem MeasureTheory.FiniteMeasure.continuous_iff_forall_continuousMap_continuous_lintegral

modified theorem MeasureTheory.FiniteMeasure.continuous_iff_forall_continuous_integral

modified theorem MeasureTheory.FiniteMeasure.continuous_iff_forall_continuous_lintegral

modified theorem MeasureTheory.FiniteMeasure.continuous_integral_boundedContinuousFunction

added theorem MeasureTheory.FiniteMeasure.continuous_integral_continuousMap

added theorem MeasureTheory.FiniteMeasure.continuous_lintegral_boundedContinuousFunction

added theorem MeasureTheory.FiniteMeasure.continuous_lintegral_continuousMap

Modified Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean

added theorem MeasureTheory.ProbabilityMeasure.continuous_iff_forall_continuousMap_continuous_integral

added theorem MeasureTheory.ProbabilityMeasure.continuous_iff_forall_continuousMap_continuous_lintegral

modified theorem MeasureTheory.ProbabilityMeasure.continuous_iff_forall_continuous_integral

modified theorem MeasureTheory.ProbabilityMeasure.continuous_iff_forall_continuous_lintegral

modified theorem MeasureTheory.ProbabilityMeasure.continuous_integral_boundedContinuousFunction

added theorem MeasureTheory.ProbabilityMeasure.continuous_integral_continuousMap

added theorem MeasureTheory.ProbabilityMeasure.continuous_lintegral_boundedContinuousFunction

added theorem MeasureTheory.ProbabilityMeasure.continuous_lintegral_continuousMap