Theorem MeasureTheory.tendsto_iff_forall_lipschitz_integral_tendsto

Modification history

2025-10-28 16:45
Mathlib/MeasureTheory/Measure/Portmanteau.lean
feat: Lipschitz function criterion for weak convergence of probability measures (#30742) …
Added MeasureTheory.tendsto_iff_forall_lipschitz_integral_tendstoView on Github →