Lemma lem:ineqs: tail transfer for a maximum

Source lines 2426–2437. Let H_i be integer valued and let N_i, L_i be nonnegative random variables with {H_i ≥ h_i} = {N_i ≥ 1} and {L_i ≥ 1} ⊆ {H_i ≥ h_i}. If E[N_i] → 0 then P(H_i ≥ h_i) → 0; if L_i → ∞ in probability then P(H_i ≥ h_i) → 1.

The index runs along an arbitrary filter, and each i carries its own probability space (the laws 𝒯^n of the paper). Expectations are lintegrals in ℝ≥0∞, so that a statement E[N_i] → 0 cannot be satisfied by a junk value of an infinite expectation. "L_i → ∞ in probability" means P(L_i ≤ K) → 0 for every K.

theorem PoissonDeclumping.tendsto_zero_of_tendsto_lintegral_zero {ι : Type u_1} {Ω : ι → Type u_2} [(i : ι) → MeasurableSpace (Ω i)] {P : (i : ι) → MeasureTheory.Measure (Ω i)} (l : Filter ι) (H : (i : ι) → Ω i → ℤ) (N : (i : ι) → Ω i → ℝ) (h : ι → ℤ) (hN : ∀ (i : ι), Measurable (N i)) (hHN : ∀ (i : ι) (ω : Ω i), h i ≤ H i ω ↔ 1 ≤ N i ω) (hE : Filter.Tendsto (fun (i : ι) => ∫⁻ (ω : Ω i), ENNReal.ofReal (N i ω) ∂P i) l (nhds 0)) : Filter.Tendsto (fun (i : ι) => (P i).real {ω : Ω i | h i ≤ H i ω}) l (nhds 0)

First half of Lemma lem:ineqs: if the expected witness count N_i(h_i) vanishes, the upper-tail probability P(H_i ≥ h_i) vanishes (Markov's inequality).

theorem PoissonDeclumping.tendsto_one_of_witness {ι : Type u_1} {Ω : ι → Type u_2} [(i : ι) → MeasurableSpace (Ω i)] {P : (i : ι) → MeasureTheory.Measure (Ω i)} [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (P i)] (l : Filter ι) (H : (i : ι) → Ω i → ℤ) (L : (i : ι) → Ω i → ℝ) (h : ι → ℤ) (hL : ∀ (i : ι), Measurable (L i)) (hLH : ∀ (i : ι) (ω : Ω i), 1 ≤ L i ω → h i ≤ H i ω) (hinf : ∀ (K : ℝ), Filter.Tendsto (fun (i : ι) => (P i).real {ω : Ω i | L i ω ≤ K}) l (nhds 0)) : Filter.Tendsto (fun (i : ι) => (P i).real {ω : Ω i | h i ≤ H i ω}) l (nhds 1)

Second half of Lemma lem:ineqs: if the lower witness count L_i(h_i) tends to infinity in probability (here: P(L_i < 1) → 0 suffices, which follows from P(L_i ≤ K) → 0 for any K ≥ 1), then P(H_i ≥ h_i) → 1.