Identification and finiteness of the intensity of a finite-rate mark set.

theorem BGW.Probability.markRate_lt_top {Ω : Type u_1} {M : Type u_2} [MeasurableSpace Ω] [MeasurableSpace M] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {ξ : Ω → MeasureTheory.Measure (NNReal × M)} {A : Set M} (hξ : IsTimeSimpleLevy P ξ) (hA : IsFiniteRate P ξ A) : markRate P ξ A < ⊤

Finite expected intensity of a finite-rate mark set.

theorem BGW.Probability.prob_noMark_window {Ω : Type u_1} {M : Type u_2} [MeasurableSpace Ω] [MeasurableSpace M] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {ξ : Ω → MeasureTheory.Measure (NNReal × M)} {A : Set M} (hξ : IsTimeSimpleLevy P ξ) (hA : IsFiniteRate P ξ A) (t : NNReal) : P {ω : Ω | (ξ ω) (Set.Ioc 0 t ×ˢ A) = 0} = ENNReal.ofReal (Real.exp (-(↑t * (markRate P ξ A).toReal)))

No-arrival exponential law: P(no A-mark in (0,t]) = exp(-t λ_A), with λ_A finite.

theorem BGW.Probability.lintegral_count_window {Ω : Type u_1} {M : Type u_2} [MeasurableSpace Ω] [MeasurableSpace M] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {ξ : Ω → MeasureTheory.Measure (NNReal × M)} {A : Set M} (hξ : IsTimeSimpleLevy P ξ) (hA : IsFiniteRate P ξ A) {s t : NNReal} (hst : s ≤ t) : ∫⁻ (ω : Ω), (ξ ω) (Set.Ioc s t ×ˢ A) ∂P = ↑(t - s) * markRate P ξ A

Expected count on a window: E ξ((s,t] × A) = (t - s) λ_A.