Truncated first moments of time-simple counting measures.

theorem BGW.Probability.ae_count_le_one_or_two_le {Ω : 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) : ∀ᵐ (ω : Ω) ∂P, (ξ ω) B ≤ 1 ∨ 2 ≤ (ξ ω) B

A counting-measure value cannot lie strictly between one and two.

theorem BGW.Probability.sum_grid_counts {M : Type u_2} [MeasurableSpace M] {A : Set M} (hA : MeasurableSet A) (μ : MeasureTheory.Measure (NNReal × M)) (h : NNReal) {n : ℕ} (hn : n ≠ 0) : ∑ i : Fin n, μ (gridBox h n (↑i) A) = μ (Set.Ioc 0 h ×ˢ A)

Counts add exactly over a uniform grid partition of a window.

theorem BGW.Probability.lintegral_window_stationary_comp {Ω : 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) {f : ENNReal → ENNReal} (hf : Measurable f) (a h : NNReal) : ∫⁻ (ω : Ω), f ((ξ ω) (Set.Ioc a (a + h) ×ˢ A)) ∂P = ∫⁻ (ω : Ω), f ((ξ ω) (Set.Ioc 0 h ×ˢ A)) ∂P

Every nonnegative measurable transform of a window count has stationary expectation.

theorem BGW.Probability.lintegral_count_le_exp_rate {Ω : 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) {c : ℝ} (hc : 0 ≤ c) (hnc : ∀ (t : NNReal), (P {ω : Ω | (ξ ω) (Set.Ioc 0 t ×ˢ A) = 0}).toReal = Real.exp (-↑t * c)) (h : NNReal) : ∫⁻ (ω : Ω), (ξ ω) (Set.Ioc 0 h ×ˢ A) ∂P ≤ ENNReal.ofReal (c * ↑h)

The mean count is at most the rate determined by the no-arrival exponential law.