Commit 2022-02-28 10:33 770a7ce2

feat(measure_theory/function/convergence_in_measure): Define convergence in measure (#11774) This PR defines convergence in measure and proves some properties about them. In particular, we prove that

• convergence a.e. in a finite measure space implies convergence in measure
• convergence in measure implies there exists a subsequence that converges a.e.
• convergence in Lp implies convergence in measure