def ProbabilityTheory.IsSpan (μ : MeasureTheory.Measure ℝ) (h : ℝ) : Prop

IsSpan μ h asserts that h > 0 and the support of μ (its atoms) is contained in some arithmetic progression a + h · ℤ. Equivalently, h is a span of μ.

def ProbabilityTheory.IsMaximalSpan (μ : MeasureTheory.Measure ℝ) (h : ℝ) : Prop

IsMaximalSpan μ h says that h is the largest span of μ: every other span h' of μ satisfies h' ≤ h.

noncomputable def ProbabilityTheory.gaussianDensity (σ x : ℝ) : ℝ

The density n(x) = (2π σ²)^{-1/2} · exp(-x²/(2σ²)) of the centered Gaussian with variance σ² evaluated at x.

theorem ProbabilityTheory.local_clt_lattice {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] (X : ℕ → Ω → ℝ) (σ b h : ℝ) (hσ : 0 < σ) (hh : 0 < h) (hmeas : ∀ (i : ℕ), Measurable (X i)) (hmean : ∀ (i : ℕ), ∫ (x : Ω), X i x ∂P = 0) (hvar : ∀ (i : ℕ), ∫ (x : Ω), X i x ^ 2 ∂P = σ ^ 2) (hindep : iIndepFun X P) (hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P) (hlattice : IsLatticeRV (MeasureTheory.Measure.map (X 0) P)) (hspan : IsMaximalSpan (MeasureTheory.Measure.map (X 0) P) h) (hbase : ∀ (x : ℝ), (MeasureTheory.Measure.map (X 0) P) {x} ≠ 0 → ∃ (j : ℤ), x = b + ↑j * h) (ε : ℝ) : 0 < ε → ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (k : ℤ), have x := (↑n * b + ↑k * h) / √↑n; |√↑n / h * ((MeasureTheory.Measure.map (fun (ω : Ω) => ∑ i ∈ Finset.range n, X i ω) P) {↑n * b + ↑k * h}).toReal - gaussianDensity σ x| < ε

Local central limit theorem for lattice random walks.

Let X₀, X₁, … be i.i.d. lattice random variables with 𝔼 Xᵢ = 0, 𝔼 Xᵢ² = σ² ∈ (0, ∞), supported on b + h ℤ (where h is the maximal span). Write Sₙ = ∑_{i<n} Xᵢ and let pₙ(x) = P(Sₙ/√n = x) for x ∈ (nb + hℤ)/√n. Then for every ε > 0, eventually in n, sup_k |(√n / h) · P(Sₙ = nb + kh) - n(x)| < ε, where n(x) = (2π σ²)^{-1/2} exp(-x²/(2σ²)).