Couplings and Poisson laws in total variation

General total-variation facts used by the source (inventory item B15, source lines 1693–1696, 2115–2120 and 2392–2398), all in the paper's probability convention paperTVDist:

• the coupling bound d_TV(L(X), L(Y)) ≤ P(X ≠ Y) and its monotone form d_TV(L(X), L(Y)) ≤ E[Y - X] for ℕ-valued X ≤ Y;
• d_TV(Po(a), Po(b)) ≤ 1 - exp (-|a - b|) ≤ |a - b|;
• continuity of the Poisson law in its parameter, and the replacement of the Poisson parameter along a sequence when the parameters are asymptotically equal;
• the Poisson zero-mass bound |P(N = 0) - exp (-a)| ≤ d_TV(L(N), Po(a)).

theorem PoissonDeclumping.paperTVDist_map_le_measureReal_ne {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] (P : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P] {X Y : Ω → α} (hX : Measurable X) (hY : Measurable Y) : paperTVDist (MeasureTheory.Measure.map X P) (MeasureTheory.Measure.map Y P) ≤ P.real {ω : Ω | X ω ≠ Y ω}

Coupling bound. Two random variables on the same probability space have laws whose normalized total variation distance is at most the probability that they differ. The disagreement event need not be measurable; Measure.real is then its outer measure.

theorem PoissonDeclumping.paperTVDist_map_le_integral_sub {Ω : Type u_1} [MeasurableSpace Ω] (P : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P] {X Y : Ω → ℕ} (hX : Measurable X) (hY : Measurable Y) (hXY : ∀ᵐ (ω : Ω) ∂P, X ω ≤ Y ω) (hint : MeasureTheory.Integrable (fun (ω : Ω) => ↑(Y ω) - ↑(X ω)) P) : paperTVDist (MeasureTheory.Measure.map X P) (MeasureTheory.Measure.map Y P) ≤ ∫ (ω : Ω), ↑(Y ω) - ↑(X ω) ∂P

Monotone coupling bound. If X ≤ Y almost surely are ℕ-valued random variables and Y - X is integrable, then d_TV(L(X), L(Y)) ≤ E[Y - X]. This is the mechanism used for the truncation in Lemma lem:truncate(i), source lines 1692–1693.

theorem PoissonDeclumping.poissonMeasure_zero : ProbabilityTheory.poissonMeasure 0 = MeasureTheory.Measure.dirac 0

The Poisson law with rate zero is the Dirac mass at zero.

theorem PoissonDeclumping.paperTVDist_poissonMeasure_le_one_sub_exp_of_le {a b : NNReal} (hab : a ≤ b) : paperTVDist (ProbabilityTheory.poissonMeasure a) (ProbabilityTheory.poissonMeasure b) ≤ 1 - Real.exp (-(↑b - ↑a))

d_TV(Po(a), Po(b)) ≤ 1 - exp (-(b - a)) for a ≤ b, via the coupling X versus X + Y with independent X ~ Po(a) and Y ~ Po(b - a).

theorem PoissonDeclumping.paperTVDist_poissonMeasure_le_one_sub_exp (a b : NNReal) : paperTVDist (ProbabilityTheory.poissonMeasure a) (ProbabilityTheory.poissonMeasure b) ≤ 1 - Real.exp (-|↑a - ↑b|)

d_TV(Po(a), Po(b)) ≤ 1 - exp (-|a - b|).

theorem PoissonDeclumping.paperTVDist_poissonMeasure_le_abs_sub (a b : NNReal) : paperTVDist (ProbabilityTheory.poissonMeasure a) (ProbabilityTheory.poissonMeasure b) ≤ |↑a - ↑b|

Poisson laws in total variation. d_TV(Po(a), Po(b)) ≤ |a - b|, as used at source lines 1695 and 2115.

theorem PoissonDeclumping.tendsto_paperTVDist_poissonMeasure {ι : Type u_1} {l : Filter ι} {a b : ι → NNReal} (h : Filter.Tendsto (fun (i : ι) => ↑(a i) - ↑(b i)) l (nhds 0)) : Filter.Tendsto (fun (i : ι) => paperTVDist (ProbabilityTheory.poissonMeasure (a i)) (ProbabilityTheory.poissonMeasure (b i))) l (nhds 0)

If the Poisson parameters are asymptotically equal, the Poisson laws merge in total variation.

theorem PoissonDeclumping.tendsto_paperTVDist_poissonMeasure_of_tendsto {ι : Type u_1} {l : Filter ι} {a : ι → NNReal} {b : NNReal} (h : Filter.Tendsto a l (nhds b)) : Filter.Tendsto (fun (i : ι) => paperTVDist (ProbabilityTheory.poissonMeasure (a i)) (ProbabilityTheory.poissonMeasure b)) l (nhds 0)

Convergence of the Poisson parameter implies convergence of the Poisson laws in total variation.

theorem PoissonDeclumping.tendsto_paperTVDist_poissonMeasure_nhds (b : NNReal) : Filter.Tendsto (fun (a : NNReal) => paperTVDist (ProbabilityTheory.poissonMeasure a) (ProbabilityTheory.poissonMeasure b)) (nhds b) (nhds 0)

Continuity of the Poisson law in its parameter, for normalized total variation.

theorem PoissonDeclumping.tendsto_paperTVDist_trans {β : Type u_1} {ι : Type u_2} [MeasurableSpace β] {l : Filter ι} {μ ν ξ : ι → MeasureTheory.Measure β} [∀ (i : ι), MeasureTheory.IsFiniteMeasure (ν i)] (h₁ : Filter.Tendsto (fun (i : ι) => paperTVDist (μ i) (ν i)) l (nhds 0)) (h₂ : Filter.Tendsto (fun (i : ι) => paperTVDist (ν i) (ξ i)) l (nhds 0)) : Filter.Tendsto (fun (i : ι) => paperTVDist (μ i) (ξ i)) l (nhds 0)

Triangle inequality along a filter: total-variation convergence passes through an intermediate family of finite measures.

theorem PoissonDeclumping.tendsto_paperTVDist_poissonMeasure_congr {ι : Type u_1} {l : Filter ι} (L : ι → MeasureTheory.Measure ℕ) {a b : ι → NNReal} (hL : Filter.Tendsto (fun (i : ι) => paperTVDist (L i) (ProbabilityTheory.poissonMeasure (a i))) l (nhds 0)) (hab : Filter.Tendsto (fun (i : ι) => ↑(a i) - ↑(b i)) l (nhds 0)) : Filter.Tendsto (fun (i : ι) => paperTVDist (L i) (ProbabilityTheory.poissonMeasure (b i))) l (nhds 0)

Replacing the Poisson parameter: if d_TV(L_n, Po(a_n)) → 0 and a_n - b_n → 0, then d_TV(L_n, Po(b_n)) → 0 (source lines 2112–2119).

theorem PoissonDeclumping.abs_measureReal_zero_sub_exp_le_paperTVDist (μ : MeasureTheory.Measure ℕ) [MeasureTheory.IsProbabilityMeasure μ] (a : NNReal) : |μ.real {0} - Real.exp (-↑a)| ≤ paperTVDist μ (ProbabilityTheory.poissonMeasure a)

The Poisson zero mass is controlled by total variation: |μ{0} - exp (-a)| ≤ d_TV(μ, Po(a)) (source lines 2392–2397).