Identification of the joint count law by its complex generating function.

theorem BGW.Probability.map_eq_pi_poisson_of_complex_pgf {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {k : ℕ} (N : Fin k → Ω → ℕ) (hN : ∀ (i : Fin k), Measurable (N i)) (r : Fin k → NNReal) (hpgf : ∀ (z : Fin k → ℂ), (∀ (i : Fin k), ‖z i‖ ≤ 1) → ∫ (ω : Ω), ∏ i : Fin k, z i ^ N i ω ∂P = Complex.exp (∑ i : Fin k, ↑↑(r i) * (z i - 1))) : MeasureTheory.Measure.map (fun (ω : Ω) (i : Fin k) => N i ω) P = MeasureTheory.Measure.pi fun (i : Fin k) => ProbabilityTheory.poissonMeasure (r i)

A complex generating function on the unit polydisk identifies a product Poisson law.

theorem BGW.Probability.counts_poisson_independent {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {M : Type u_2} [MeasurableSpace M] {ξ : Ω → MeasureTheory.Measure (NNReal × M)} (hξ : IsTimeSimpleLevy P ξ) {k : ℕ} (A : Fin k → Set M) (hA : ∀ (i : Fin k), IsFiniteRate P ξ (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 (ω : Ω) (i : Fin k) => natCount (ξ ω) (Set.Ioc (s i) (t i) ×ˢ A i)) P = MeasureTheory.Measure.pi fun (i : Fin k) => ProbabilityTheory.poissonMeasure ((t i - s i) * (markRate P ξ (A i)).toNNReal)

Independent Poisson counts on finitely many disjoint finite-rate boxes.