Theorem BoundedContinuousFunction.apply_le_nndist_zero

Modification history

2026-05-29 07:38

Mathlib/MeasureTheory/Integral/BoundedContinuousFunction.lean

feat(MeasureTheory/Function): ae convergence implies convergence in distribution (#39517) …

Modified BoundedContinuousFunction.apply_le_nndist_zero View on Github →

2023-11-12 00:13

Mathlib/MeasureTheory/Integral/BoundedContinuousFunction.lean

feat: add last implication of portmanteau characterizations of weak convergence (#8097) …

Added BoundedContinuousFunction.apply_le_nndist_zero View on Github →