Numerical limits for binomial and finite-mark grid approximations.

theorem BGW.Probability.tendsto_grid_mean (a : ℝ) : Filter.Tendsto (fun (n : ℕ) => ↑n * (1 - Real.exp (-a / ↑n))) Filter.atTop (nhds a)

The expected number of occupied cells tends to the exponential rate.