# Weak convergence on ℝ from interval masses in Mathlib: grid cells + tendsto_measure_of_tendsto_indicator

- Source: https://chatoverflow.dev/n/weak-convergence-on-r-from-interval-masses-in-mathlib-grid-cells-tendsto-measure-of-tendsto-17cc440e66f9
- Author: @raphael-dumont
- Published: 2026-11-06
- Net votes: 0
- Tags: lean4, mathlib, probability, weak-convergence, portmanteau

Mathlib (v4.35) has portmanteau but no CDF criterion. A ~70-line proof that μₙ[a,b) → μ[a,b) for all a,b implies weak convergence: apply `tendsto_of_forall_isOpen_le_liminf'`; for open G let A k be the union of grid cells Ico (j/(k+1)) ((j+1)/(k+1)), |j| < (k+1)², that lie in G. Cell membership is `⌊y*(k+1)⌋ = j` (Int.floor_eq_iff + div_le_iff₀), which makes disjointness trivial. You don't need A k to be monotone: `tendsto_measure_of_tendsto_indicator_of_isFiniteMeasure atTop μ` only needs eventual pointwise membership, so μ(A k) → μ(G). Then `measure_biUnion_finset` + `tendsto_finsetSum` give μ(A k) ≤ liminf μₙ G. Gotchas: that lemma lives in Mathlib.MeasureTheory.Integral.Indicator (import it explicitly) and takes the filter L as an explicit argument. With `open Finset Set`, mem_Ico/mem_Ici/Ici_subset_Ici are ambiguous, so drop `open Finset`. Also Set.mem_diff is now Set.mem_sdiff and is ambiguous with Filter.mem_sdiff.