Commit 2023-11-12 00:13 adefdc2a

View on Github →

feat: add last implication of portmanteau characterizations of weak convergence (#8097) This PR adds the last missing implication of the general case of portmanteau equivalent characterizations of convergence in distribution: a sufficient condition for convergence in distribution of a sequence of probability measures is that for all open sets the candidate limit measure is at most the liminf of the measures.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/MeasureTheory/Integral/BoundedContinuousFunction.lean

added theorem BoundedContinuousFunction.apply_le_nndist_zero

added theorem BoundedContinuousFunction.lintegral_le_edist_mul

Modified Mathlib/MeasureTheory/Measure/Portmanteau.lean

added theorem MeasureTheory.integral_le_liminf_integral_of_forall_isOpen_measure_le_liminf_measure

added theorem MeasureTheory.lintegral_le_liminf_lintegral_of_forall_isOpen_measure_le_liminf_measure

added theorem MeasureTheory.tendsto_integral_of_forall_integral_le_liminf_integral

added theorem MeasureTheory.tendsto_of_forall_isOpen_le_liminf

Modified Mathlib/Topology/Instances/ENNReal.lean

added theorem ENNReal.continuousOn_toReal

added theorem ENNReal.continuous_truncateToReal

added theorem ENNReal.liminf_toReal_eq

added theorem ENNReal.limsup_toReal_eq

added theorem ENNReal.monotone_truncateToReal

added theorem ENNReal.truncateToReal_eq_toReal

added theorem ENNReal.truncateToReal_le

added theorem ENNReal.truncateToReal_nonneg

Modified Mathlib/Topology/MetricSpace/Lipschitz.lean

added theorem Real.lipschitzWith_toNNReal

Created Mathlib/Topology/Order/Bounded.lean

added theorem Filter.isBounded_ge_map_of_bounded_range

added theorem Filter.isBounded_le_map_of_bounded_range