Measurability and normalized convergence of rounding

theorem BGW.Probability.measurable_round : Measurable round

Rounding a real number to the nearest integer is measurable.

theorem BGW.Probability.round_normalized_tendsto {v b : ℕ → ℝ} {x : ℝ} (hv : Filter.Tendsto v Filter.atTop (nhds x)) (hb : Filter.Tendsto b Filter.atTop Filter.atTop) : Filter.Tendsto (fun (k : ℕ) => ↑(round (v k * b k)) / b k) Filter.atTop (nhds x)

Rounding v k * b k and dividing by b k preserves the limit of v when b diverges.