Poisson point processes

DefinitionCounting measure of a finite tuple of points#✓fully proved

The counting measure ∑_{i < n} δ_{x_i} of a finite tuple of points.

noncomputable def countingMeasure {n : ℕ} (x : Fin n → E) : Measure E :=
  ∑ i, Measure.dirac (x i)

Used by 11

Used byCounting measure of a set as a sum of indicators · Image of a counting measure under a map · Laplace functional · Integral against a counting measure · Campbell's formula · Mecke equation · Point counts of a Poisson point process are Poisson · Mixed binomial process is a Poisson process · Mapping theorem · Measurability of the counting measure in the points · Poisson point process with finite intensity

DefinitionPoisson point process with finite intensity#✓fully proved

The law of the Poisson point process with finite intensity μ on E: ∑_n e^{-μ(E)} / n! • (μ^{⊗n}).map countingMeasure, a probability measure on Measure E (Last–Penrose Prop. 3.5, mixed binomial construction).

noncomputable def poissonPointProcess (μ : Measure E) [IsFiniteMeasure μ] :
    Measure (Measure E) :=
  Measure.sum fun n : ℕ => ENNReal.ofReal (Real.exp (-μ.real univ) / n !) •
    (Measure.pi fun _ : Fin n => μ).map countingMeasure

Uses 1 · Used by 7

Statement usesCounting measure of a finite tuple of points

Used byLaplace functional · Campbell's formula · Mecke equation · Point counts of a Poisson point process are Poisson · Mixed binomial process is a Poisson process · Mapping theorem · Restriction theorem

TheoremCounting measure of a set as a sum of indicators#✓fully proved

(∑ δ_{x_i})(s) = #{i | x_i ∈ s}, as a sum of indicators.

theorem countingMeasure_apply {n : ℕ} (x : Fin n → E) {s : Set E} (hs : MeasurableSet s) :
    countingMeasure x s = ∑ i, s.indicator 1 (x i)

Uses 1 · Used by 2

Statement usesCounting measure of a finite tuple of points

Used byImage of a counting measure under a map · Measurability of the counting measure in the points

TheoremMeasurability of the counting measure in the points#✓fully proved

The counting measure of a tuple depends measurably on the tuple.

theorem measurable_countingMeasure (n : ℕ) :
    Measurable (countingMeasure : (Fin n → E) → Measure E)

Uses 2 · Used by 6

Statement usesCounting measure of a finite tuple of points

Proof usesCounting measure of a set as a sum of indicators

Used byLaplace functional · Campbell's formula · Mecke equation · Point counts of a Poisson point process are Poisson · Mixed binomial process is a Poisson process · Mapping theorem

TheoremIntegral against a counting measure#✓fully proved

∫ f d(∑ δ_{x_i}) = ∑ f(x_i).

theorem lintegral_countingMeasure {n : ℕ} (x : Fin n → E) {f : E → ℝ≥0∞} (hf : Measurable f) :
    ∫⁻ y, f y ∂(countingMeasure x) = ∑ i, f (x i)

Uses 1 · Used by 2

Statement usesCounting measure of a finite tuple of points

Used byLaplace functional · Campbell's formula

TheoremPoisson weights sum to one#✓fully proved

The Poisson weights sum to one: ∑_n e^{-μ(E)} μ(E)^n / n! = 1.

theorem tsum_coeff_mul_pow (μ : Measure E) [IsFiniteMeasure μ] :
    ∑' n : ℕ, ENNReal.ofReal (Real.exp (-μ.real univ) / n !) * μ univ ^ n = 1

Used by 4

Used byLaplace functional · Campbell's formula · Point counts of a Poisson point process are Poisson · Mixed binomial process is a Poisson process

TheoremIntegral of a coordinate function under a product measure#✓fully proved

∫ f(x_i) dμ^{⊗n}(x) = μ(E)^{n-1} ∫ f dμ.

theorem lintegral_pi_eval (μ : Measure E) [IsFiniteMeasure μ] {n : ℕ} (i : Fin n)
    {f : E → ℝ≥0∞} (hf : Measurable f) :
    ∫⁻ x, f (x i) ∂(Measure.pi fun _ : Fin n => μ) = μ univ ^ (n - 1) * ∫⁻ y, f y ∂μ

Used by 1

Used byCampbell's formula

TheoremImage of a counting measure under a map#✓fully proved

The image of ∑ δ_{x_i} under T is ∑ δ_{T(x_i)}.

theorem countingMeasure_comp {n : ℕ} (x : Fin n → E) {T : E → F} (hT : Measurable T) :
    countingMeasure (T ∘ x) = (countingMeasure x).map T

Uses 2 · Used by 1

Statement usesCounting measure of a finite tuple of points

Proof usesCounting measure of a set as a sum of indicators

Used byMapping theorem

TheoremPoint counts of a Poisson point process are Poisson#✓fully proved

The number of points η(B) in a measurable set B has the Poisson law of mean μ(B).

theorem map_apply_eq_poissonMeasure {B : Set E} (hB : MeasurableSet B) :
    (poissonPointProcess μ).map (fun η => η B) =
      (poissonMeasure (μ B).toNNReal).map (Nat.cast : ℕ → ℝ≥0∞)

Uses 4

Statement usesPoisson point process with finite intensity

Proof usesCounting measure of a finite tuple of points · Measurability of the counting measure in the points · Poisson weights sum to one

TheoremMixed binomial process is a Poisson process#✓fully proved

The counts η(A i) of pairwise disjoint measurable sets are independent, and η(A i) has the Poisson law of mean μ(A i): the mixed binomial process is a Poisson process with intensity μ in the sense of Last–Penrose Def. 3.1 (Last–Penrose Prop. 3.5).

theorem map_apply_pi {ι : Type*} [Fintype ι] (A : ι → Set E)
    (hA : ∀ i, MeasurableSet (A i)) (hd : Pairwise (Disjoint on A)) :
    (poissonPointProcess μ).map (fun η i => η (A i)) =
      Measure.pi fun i => (poissonMeasure (μ (A i)).toNNReal).map (Nat.cast : ℕ → ℝ≥0∞)

Uses 4

Statement usesPoisson point process with finite intensity

Proof usesCounting measure of a finite tuple of points · Measurability of the counting measure in the points · Poisson weights sum to one

TheoremCampbell's formula#✓fully proved

E ∫ f dη = ∫ f dμ for measurable f : E → [0, ∞] (Last–Penrose Prop. 2.7).

theorem lintegral_lintegral {f : E → ℝ≥0∞} (hf : Measurable f) :
    ∫⁻ η, ∫⁻ x, f x ∂η ∂(poissonPointProcess μ) = ∫⁻ x, f x ∂μ

Uses 6

Statement usesPoisson point process with finite intensity

Proof usesCounting measure of a finite tuple of points · Integral against a counting measure · Integral of a coordinate function under a product measure · Measurability of the counting measure in the points · Poisson weights sum to one

TheoremLaplace functional#✓fully proved

For measurable f : E → [0, ∞), E exp(-∫ f dη) = exp(-∫ (1 - e^{-f}) dμ) (Last–Penrose Thm. 3.9). The integral ∫ f dη is a finite sum ∑ f(x_i) for every configuration charged by the process.

theorem integral_exp_neg {f : E → ℝ≥0} (hf : Measurable f) :
    ∫ η, Real.exp (-(∫⁻ x, (f x : ℝ≥0∞) ∂η).toReal) ∂(poissonPointProcess μ) =
      Real.exp (-∫ x, (1 - Real.exp (-(f x : ℝ))) ∂μ)

Uses 5

Statement usesPoisson point process with finite intensity

Proof usesCounting measure of a finite tuple of points · Integral against a counting measure · Measurability of the counting measure in the points · Poisson weights sum to one

TheoremMecke equation#✓fully proved

For measurable h : E × Measure E → [0, ∞], E ∫ h(x, η) η(dx) = ∫ E h(x, η + δ_x) μ(dx) (Mecke 1967; Last–Penrose Thm. 4.1).

theorem lintegral_lintegral_mecke {h : E → Measure E → ℝ≥0∞}
    (hh : Measurable (Function.uncurry h)) :
    ∫⁻ η, ∫⁻ x, h x η ∂η ∂(poissonPointProcess μ) =
      ∫⁻ x, ∫⁻ η, h x (η + Measure.dirac x) ∂(poissonPointProcess μ) ∂μ

Uses 3

Statement usesPoisson point process with finite intensity

Proof usesCounting measure of a finite tuple of points · Measurability of the counting measure in the points

TheoremMapping theorem#✓fully proved

The image η ∘ T⁻¹ of a Poisson point process under a measurable map T : E → F is the Poisson point process with intensity μ ∘ T⁻¹ (Last–Penrose Thm. 5.1).

theorem map_map {T : E → F} (hT : Measurable T) :
    (poissonPointProcess μ).map (fun η => η.map T) = poissonPointProcess (μ.map T)

Uses 4

Statement usesPoisson point process with finite intensity

Proof usesCounting measure of a finite tuple of points · Image of a counting measure under a map · Measurability of the counting measure in the points

TheoremRestriction theorem#●ready to prove

The restrictions η|_{A i} of a Poisson point process with finite intensity μ to pairwise disjoint measurable sets A i are independent Poisson point processes with intensities μ|_{A i} (Last–Penrose Thm. 5.2).

theorem_wanted map_restrict_pi {E : Type*} [MeasurableSpace E] (μ : Measure E)
    [IsFiniteMeasure μ] {ι : Type*} [Fintype ι] (A : ι → Set E)
    (hA : ∀ i, MeasurableSet (A i)) (hd : Pairwise (Disjoint on A)) :
    (poissonPointProcess μ).map (fun η i => η.restrict (A i)) =
      Measure.pi fun i => poissonPointProcess (μ.restrict (A i))

Uses 1

Statement usesPoisson point process with finite intensity

14 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.