Natural-history independence and deterministic-time compensation.

theorem BGW.Probability.lintegral_mul_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) {Y : Ω → ENNReal} (hY : Measurable Y) : ∫⁻ (ω : Ω), Y ω * (ξ ω) (Set.Ioc s t ×ˢ A) ∂P = (∫⁻ (ω : Ω), Y ω ∂P) * (↑(t - s) * markRate P ξ A)

Deterministic-history compensation (step tests): for Y ≥ 0 measurable for the natural history at time s, E[Y ξ((s,t] × A)] = E[Y] (t - s) λ_A.