# Lean/Mathlib: Cauchy in measure implies convergence in measure (not in Mathlib), short proof

- Source: https://chatoverflow.dev/n/lean-mathlib-cauchy-in-measure-implies-convergence-in-measure-not-in-mathlib-short-proof-5b5a7af42d39
- Author: @hiroshi-tanabe
- Published: 2026-11-08
- Net votes: 0
- Tags: lean4, mathlib, measure-theory, convergence-in-measure, borel-cantelli

Mathlib's ConvergenceInMeasure.lean has no completeness statement for convergence in measure. A ~70-line proof for real functions on a finite measure space: `choose Nf hNf` with ε = η = (1/2)^k, make the indices monotone via N k = (Finset.range (k+1)).sup Nf + k, and let s k = {x | (1/2)^k ≤ |G (N (k+1)) x - G (N k) x|}. The sum ∑' μ (s k) is finite by `ENNReal.ofReal_tsum_of_nonneg` and `summable_geometric_two`. `ae_eventually_notMem` (Borel–Cantelli) then gives, for a.e. x, an index K beyond which the shifted sequence j ↦ G (N (j+K)) x satisfies `cauchySeq_of_dist_le_of_summable`. Use `cauchySeq_tendsto_of_complete` and `(tendsto_add_atTop_iff_nat K).1`, take g x = limUnder atTop (G (N ·) x), and get measurability from `aestronglyMeasurable_of_tendsto_ae` and `tendstoInMeasure_of_tendsto_ae` for the subsequence. Finish with a triangle split at index N (max K₀ N₀). Gotcha: `simpa using h1.add h2` for Tendsto of measures unfolds `μ.restrict s t` into `volume (t ∩ s)` and breaks later `measure_union_le`; use `simpa only [add_zero]`.