Joint complex generating functions of disjoint measurable subsets of a finite-rate box.

On each grid cell, the generating function agrees with its linear count expression when the containing cell has at most one arrival. The integrated remainder is controlled by the mean count minus the probability of a nonempty cell. Stationarity and the exponential no-arrival law make the sum of these remainders vanish as the grid is refined. Intersecting cells with the tested sets allows arbitrary box endpoints without an additional time partition.

theorem BGW.Probability.isFiniteRate_iUnion {Ω : Type u_1} {M : Type u_2} [MeasurableSpace Ω] [MeasurableSpace M] {P : MeasureTheory.Measure Ω} {ξ : Ω → MeasureTheory.Measure (NNReal × M)} {k : ℕ} (A : Fin k → Set M) (hA : ∀ (i : Fin k), IsFiniteRate P ξ (A i)) : IsFiniteRate P ξ (⋃ (i : Fin k), A i)

A finite union of finite-rate mark sets has finite rate.

theorem BGW.Probability.integral_natCount_subset {Ω : Type u_1} {M : Type u_2} [MeasurableSpace Ω] [MeasurableSpace M] {P : MeasureTheory.Measure Ω} {ξ : Ω → MeasureTheory.Measure (NNReal × M)} {A : Set M} (hξ : IsTimeSimpleLevy P ξ) (hA : IsFiniteRate P ξ A) {T : NNReal} {B : Set (NNReal × M)} (hB : MeasurableSet B) (hsub : B ⊆ Set.Ioc 0 T ×ˢ A) : ∫ (ω : Ω), ↑(natCount (ξ ω) B) ∂P = (∫⁻ (ω : Ω), (ξ ω) B ∂P).toReal

Expected natural-number counts agree with the extended nonnegative expected counts.

theorem BGW.Probability.integral_complex_pgf_subsets {Ω : Type u_1} {M : Type u_2} [MeasurableSpace Ω] [MeasurableSpace M] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {ξ : Ω → MeasureTheory.Measure (NNReal × M)} {A : Set M} {k : ℕ} (hξ : IsTimeSimpleLevy P ξ) (hA : IsFiniteRate P ξ A) (T : NNReal) (B : Fin k → Set (NNReal × M)) (hB : ∀ (j : Fin k), MeasurableSet (B j)) (hsub : ∀ (j : Fin k), B j ⊆ Set.Ioc 0 T ×ˢ A) (hd : Pairwise (Function.onFun Disjoint B)) (z : Fin k → ℂ) (hz : ∀ (j : Fin k), ‖z j‖ ≤ 1) : ∫ (ω : Ω), ∏ j : Fin k, z j ^ natCount (ξ ω) (B j) ∂P = Complex.exp (∑ j : Fin k, ↑(∫ (ω : Ω), ↑(natCount (ξ ω) (B j)) ∂P) * (z j - 1))

Joint complex generating functions of disjoint finite-intensity subsets factor exponentially.