The Stein solution for the Poisson law

For a rate r > 0 and an event A ⊆ ℕ, steinSolution r A solves the Poisson Stein equation

r f(w + 1) - w f(w) = 1_A(w) - Po(r)(A) for every w : ℕ,

and is bounded by one in absolute value. Writing F = P(Z ≤ w), T = P(Z > w) and p_w = P(Z = w) for Z ~ Po(r), the explicit numerator is bounded by F T, and F T ≤ r p_w follows from the head bound (r - w) F ≤ r p_w and the tail bound (w + 1 - r) T ≤ r p_w, both consequences of the recursion (k + 1) p_{k+1} = r p_k.

This is the analytic input to the Arratia–Goldstein–Gordon Chen–Stein bound (Proposition prop:AGG of the source); it is the crude Stein factor ‖f‖ ≤ 1 and not the sharper factors of AGG89.

theorem PoissonDeclumping.ChenStein.succ_mul_poissonMeasure_real_singleton (r : NNReal) (w : ℕ) : (↑w + 1) * (ProbabilityTheory.poissonMeasure r).real {w + 1} = ↑r * (ProbabilityTheory.poissonMeasure r).real {w}

The Poisson recursion (w + 1) p_{w+1} = r p_w.

theorem PoissonDeclumping.ChenStein.poissonMeasure_real_inter_Iic_succ (r : NNReal) (A : Set ℕ) (w : ℕ) : (ProbabilityTheory.poissonMeasure r).real (A ∩ Set.Iic (w + 1)) = (ProbabilityTheory.poissonMeasure r).real (A ∩ Set.Iic w) + A.indicator 1 (w + 1) * (ProbabilityTheory.poissonMeasure r).real {w + 1}

theorem PoissonDeclumping.ChenStein.poissonMeasure_real_Iic_succ (r : NNReal) (w : ℕ) : (ProbabilityTheory.poissonMeasure r).real (Set.Iic (w + 1)) = (ProbabilityTheory.poissonMeasure r).real (Set.Iic w) + (ProbabilityTheory.poissonMeasure r).real {w + 1}

theorem PoissonDeclumping.ChenStein.sub_mul_poissonMeasure_real_Iic_le (r : NNReal) (w : ℕ) : (↑r - ↑w) * (ProbabilityTheory.poissonMeasure r).real (Set.Iic w) ≤ ↑r * (ProbabilityTheory.poissonMeasure r).real {w}

Head bound: (r - w) P(Z ≤ w) ≤ r P(Z = w) for Z ~ Po(r).

@[reducible, inline]

noncomputable abbrev PoissonDeclumping.ChenStein.poissonWeight (r : NNReal) (n : ℕ) : ℝ

The Poisson weights exp (-r) r ^ n / n! as a real function.

Equations

• PoissonDeclumping.ChenStein.poissonWeight r n = Real.exp (-↑r) * ↑r ^ n / ↑n.factorial

theorem PoissonDeclumping.ChenStein.summable_poissonWeight (r : NNReal) : Summable (poissonWeight r)

theorem PoissonDeclumping.ChenStein.poissonMeasure_real_Iic (r : NNReal) (w : ℕ) : (ProbabilityTheory.poissonMeasure r).real (Set.Iic w) = ∑ k ∈ Finset.range (w + 1), poissonWeight r k

theorem PoissonDeclumping.ChenStein.poissonMeasure_real_Ioi (r : NNReal) (w : ℕ) : (ProbabilityTheory.poissonMeasure r).real (Set.Ioi w) = ∑' (n : ℕ), poissonWeight r (n + (w + 1))

theorem PoissonDeclumping.ChenStein.sub_mul_poissonMeasure_real_Ioi_le (r : NNReal) (w : ℕ) : (↑w + 1 - ↑r) * (ProbabilityTheory.poissonMeasure r).real (Set.Ioi w) ≤ ↑r * (ProbabilityTheory.poissonMeasure r).real {w}

Tail bound: (w + 1 - r) P(Z > w) ≤ r P(Z = w) for Z ~ Po(r).

theorem PoissonDeclumping.ChenStein.poissonMeasure_real_Iic_mul_Ioi_le (r : NNReal) (w : ℕ) : (ProbabilityTheory.poissonMeasure r).real (Set.Iic w) * (ProbabilityTheory.poissonMeasure r).real (Set.Ioi w) ≤ ↑r * (ProbabilityTheory.poissonMeasure r).real {w}

P(Z ≤ w) P(Z > w) ≤ r P(Z = w) for Z ~ Po(r).

theorem PoissonDeclumping.ChenStein.abs_steinNumerator_le (r : NNReal) (A : Set ℕ) (w : ℕ) : |(ProbabilityTheory.poissonMeasure r).real (A ∩ Set.Iic w) - (ProbabilityTheory.poissonMeasure r).real A * (ProbabilityTheory.poissonMeasure r).real (Set.Iic w)| ≤ (ProbabilityTheory.poissonMeasure r).real (Set.Iic w) * (ProbabilityTheory.poissonMeasure r).real (Set.Ioi w)

The numerator of the Stein solution is bounded by P(Z ≤ w) P(Z > w).

noncomputable def PoissonDeclumping.ChenStein.steinSolution (r : NNReal) (A : Set ℕ) : ℕ → ℝ

The Stein solution of r f(w+1) - w f(w) = 1_A(w) - Po(r)(A), normalized by f 0 = 0.

Equations

• One or more equations did not get rendered due to their size.
• PoissonDeclumping.ChenStein.steinSolution r A 0 = 0

theorem PoissonDeclumping.ChenStein.abs_steinSolution_le_one (r : NNReal) (A : Set ℕ) (k : ℕ) : |steinSolution r A k| ≤ 1

The Stein solution is bounded by one.

theorem PoissonDeclumping.ChenStein.abs_sub_le_two_mul_of_abs_le_one {f : ℕ → ℝ} (hf : ∀ (k : ℕ), |f k| ≤ 1) (a d : ℕ) : |f (a + d) - f a| ≤ 2 * ↑d

A function bounded by one changes by at most 2 d over a step of length d.

theorem PoissonDeclumping.ChenStein.steinSolution_equation {r : NNReal} (hr : 0 < r) (A : Set ℕ) (w : ℕ) : ↑r * steinSolution r A (w + 1) - ↑w * steinSolution r A w = A.indicator 1 w - (ProbabilityTheory.poissonMeasure r).real A

The Stein equation: r f(w+1) - w f(w) = 1_A(w) - Po(r)(A) for every w : ℕ.

theorem PoissonDeclumping.ChenStein.abs_steinSolution_succ_sub_le_two (r : NNReal) (A : Set ℕ) (w : ℕ) : |steinSolution r A (w + 1) - steinSolution r A w| ≤ 2

Increments of the Stein solution are bounded by two.

theorem PoissonDeclumping.ChenStein.integral_steinOperator_poissonMeasure (r : NNReal) {f : ℕ → ℝ} {C : ℝ} (hf : ∀ (k : ℕ), |f k| ≤ C) : ∫ (n : ℕ), ↑r * f (n + 1) - ↑n * f n ∂ProbabilityTheory.poissonMeasure r = 0

Stein identity for the Poisson law: E[r f(Z+1) - Z f(Z)] = 0 for Z ~ Po(r) and any bounded f. (Not needed for the Chen–Stein bound itself, which only uses the Stein equation pointwise.)