Independent Poisson counts of finite-intensity excursion boxes.

See Bertoin, Lévy Processes, Chapter IV.

theorem BGW.StableTrees.excursionCounts_poisson_independent {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {ξ : Skorokhod.DLoc → MeasureTheory.Measure (NNReal × Excursion)} (hξ : Measurable ξ) (hae : ξ =ᵐ[↑(stableLocalLaw θ)] excursionPointMeasure) {k : ℕ} (A : Fin k → Set Excursion) (hA : ∀ (i : Fin k), MeasurableSet (A i)) (hfin : ∀ (i : Fin k), (excursionMeasure θ) (A i) < ⊤) (s t : Fin k → NNReal) (hst : ∀ (i : Fin k), s i ≤ t i) (hdisj : Pairwise (Function.onFun Disjoint fun (i : Fin k) => Set.Ioc (s i) (t i) ×ˢ A i)) : MeasureTheory.Measure.map (fun (f : Skorokhod.DLoc) (i : Fin k) => Probability.natCount (ξ f) (Set.Ioc (s i) (t i) ×ˢ A i)) ↑(stableLocalLaw θ) = MeasureTheory.Measure.pi fun (i : Fin k) => ProbabilityTheory.poissonMeasure ((t i - s i) * ((excursionMeasure θ) (A i)).toNNReal)

Poisson theorem (counts): for every measurable modification ξ, counts of boxes (s i, t i] × A i with N (A i) < ∞ and pairwise disjoint boxes are independent Poisson with means (t i - s i) * N (A i).

theorem BGW.StableTrees.excursionCounts_poisson_independent_pointMeasure {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {k : ℕ} (A : Fin k → Set Excursion) (hA : ∀ (i : Fin k), MeasurableSet (A i)) (hfin : ∀ (i : Fin k), (excursionMeasure θ) (A i) < ⊤) (s t : Fin k → NNReal) (hst : ∀ (i : Fin k), s i ≤ t i) (hdisj : Pairwise (Function.onFun Disjoint fun (i : Fin k) => Set.Ioc (s i) (t i) ×ˢ A i)) : MeasureTheory.Measure.map (fun (f : Skorokhod.DLoc) (i : Fin k) => Probability.natCount (excursionPointMeasure f) (Set.Ioc (s i) (t i) ×ˢ A i)) ↑(stableLocalLaw θ) = MeasureTheory.Measure.pi fun (i : Fin k) => ProbabilityTheory.poissonMeasure ((t i - s i) * ((excursionMeasure θ) (A i)).toNNReal)

The same law for the unmodified excursionPointMeasure (the map is a.e. equal to the one of ξ, so no measurable modification needs to be named).