Integer-valued counts and the probability of a collision in a fine grid.
theorem
BGW.Probability.ae_natCount_cast
{Ω : Type u_1}
{M : Type u_2}
[MeasurableSpace Ω]
[MeasurableSpace M]
{P : MeasureTheory.Measure Ω}
{ξ : Ω → MeasureTheory.Measure (NNReal × M)}
(hξ : IsTimeSimpleLevy P ξ)
{B : Set (NNReal × M)}
(hB : MeasurableSet B)
(hfin : ∀ᵐ (ω : Ω) ∂P, (ξ ω) B < ⊤)
:
Reading a finite counting-measure value in ℕ preserves its value.