def ProbabilityTheory.IsBernoulliRV {Ω : Type u_1} [MeasurableSpace Ω] (X : Ω → ℕ) (μ : MeasureTheory.Measure Ω) (p : ℝ) : Prop

IsBernoulliRV X μ p says that X : Ω → ℕ is a Bernoulli(p) random variable under the measure μ: the parameter p ∈ [0,1] satisfies P(X = 0) = 1 - p and P(X = 1) = p.

theorem ProbabilityTheory.bernoulli_sum_pmf {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {m : ℕ} {X : Fin m → Ω → ℕ} {p : Fin m → ℝ} (hBernoulli : ∀ (i : Fin m), IsBernoulliRV (X i) μ (p i)) (hIndep : iIndepFun X μ) (hMeas : ∀ (i : Fin m), Measurable (X i)) (j : ℕ) : (μ ((fun (ω : Ω) => ∑ i : Fin m, X i ω) ⁻¹' {j})).toReal = ∑ A ∈ Finset.powersetCard j Finset.univ, (∏ i ∈ A, p i) * ∏ i ∈ Finset.univ \ A, (1 - p i)

Probability mass function of a sum of independent (possibly nonidentical) Bernoulli random variables: if X₁, …, X_m are independent with X_i ∼ Bernoulli(p_i), then for any j ∈ ℕ, P(∑ X_i = j) = ∑_{A ⊆ [m], |A| = j} ∏_{i ∈ A} p_i · ∏_{i ∉ A} (1 - p_i) (the j-th elementary symmetric polynomial in (p_i) weighted by the complementary product).

theorem ProbabilityTheory.elem_symm_poly_tendsto_poisson {k : ℕ → ℕ} {p : (n : ℕ) → Fin (k n) → ℝ} {lam : NNReal} (hMaxTendsto : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (i : Fin (k n)), p n i < ε) (hSumTendsto : Filter.Tendsto (fun (n : ℕ) => ∑ i : Fin (k n), p n i) Filter.atTop (nhds ↑lam)) (j : ℕ) : Filter.Tendsto (fun (n : ℕ) => ∑ A ∈ Finset.powersetCard j Finset.univ, (∏ i ∈ A, p n i) * ∏ i ∈ Finset.univ \ A, (1 - p n i)) Filter.atTop (nhds (poissonPMFReal lam j))

Analytic core of Poisson convergence: if max_i p_{n,i} → 0 and ∑_i p_{n,i} → λ as n → ∞, then the j-th elementary symmetric polynomial expression ∑_{|A|=j} ∏_{i ∈ A} p_{n,i} · ∏_{i ∉ A} (1 - p_{n,i}) converges to the Poisson pmf λ^j e^{-λ} / j!.

theorem ProbabilityTheory.poisson_convergence {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {k : ℕ → ℕ} {X : (n : ℕ) → Fin (k n) → Ω → ℕ} {p : (n : ℕ) → Fin (k n) → ℝ} {lam : NNReal} (hBernoulli : ∀ (n : ℕ) (i : Fin (k n)), IsBernoulliRV (X n i) μ (p n i)) (hIndep : ∀ (n : ℕ), iIndepFun (X n) μ) (hMeas : ∀ (n : ℕ) (i : Fin (k n)), Measurable (X n i)) (hMaxTendsto : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (i : Fin (k n)), p n i < ε) (hSumTendsto : Filter.Tendsto (fun (n : ℕ) => ∑ i : Fin (k n), p n i) Filter.atTop (nhds ↑lam)) (j : ℕ) : Filter.Tendsto (fun (n : ℕ) => (μ ((fun (ω : Ω) => ∑ i : Fin (k n), X n i ω) ⁻¹' {j})).toReal) Filter.atTop (nhds (poissonPMFReal lam j))

Poisson convergence theorem (Lecture 17): let X_{n,m} be independent {0,1}-valued random variables with P(X_{n,m} = 1) = p_{n,m}. If ∑_{m=1}^{k(n)} p_{n,m} → λ and max_{m} p_{n,m} → 0, then the row sums S_n = ∑_{m} X_{n,m} converge in law to Poisson(λ). Here we state the pointwise convergence of the pmf values P(S_n = j) → λ^j e^{-λ}/j! for each j ∈ ℕ.