Finite-partition generating functions for disjoint finite-rate boxes.
theorem
BGW.Probability.integral_complex_pgf_boxes
{Ω : Type u_1}
{M : Type u_2}
[MeasurableSpace Ω]
[MeasurableSpace M]
{P : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure P]
{ξ : Ω → 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)
(hd : Pairwise (Function.onFun Disjoint fun (i : Fin k) => Set.Ioc (s i) (t i) ×ˢ A i))
(z : Fin k → ℂ)
(hz : ∀ (i : Fin k), ‖z i‖ ≤ 1)
:
The complex generating function of disjoint finite-rate boxes, on the closed unit polydisk.
theorem
BGW.Probability.pgf_finite_partition
{Ω : Type u_1}
{M : Type u_2}
[MeasurableSpace Ω]
[MeasurableSpace M]
{P : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure P]
{ξ : Ω → 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))
(z : Fin k → ℝ)
(hz0 : ∀ (i : Fin k), 0 ≤ z i)
(hz1 : ∀ (i : Fin k), z i ≤ 1)
:
Finite-mark partition pgf. For finitely many boxes (s i, t i] × A i, pairwise disjoint
as subsets of ℝ≥0 × M and with finite-rate A i, and z i ∈ [0,1]:
E ∏ z_i^{N_i} = exp(∑ (t_i - s_i) λ_{A_i} (z_i - 1)).