Window-split identities, stationarity, and the no-arrival functional equation.

theorem BGW.Probability.ae_finite_box {Ω : Type u_1} {M : Type u_2} [MeasurableSpace Ω] [MeasurableSpace M] {P : MeasureTheory.Measure Ω} {ξ : Ω → MeasureTheory.Measure (NNReal × M)} {A : Set M} (hA : IsFiniteRate P ξ A) {s t : NNReal} (_hst : s ≤ t) : ∀ᵐ (ω : Ω) ∂P, (ξ ω) (Set.Ioc s t ×ˢ A) < ⊤

theorem BGW.Probability.windowShift_box {M : Type u_2} [MeasurableSpace M] {A : Set M} (μ : MeasureTheory.Measure (NNReal × M)) (a h : NNReal) (hA : MeasurableSet A) : (windowShift a (a + h) μ) (Set.Ioc 0 h ×ˢ A) = μ (Set.Ioc a (a + h) ×ˢ A)

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

theorem BGW.Probability.count_split {M : Type u_2} [MeasurableSpace M] {A : Set M} (μ : MeasureTheory.Measure (NNReal × M)) (hA : MeasurableSet A) {s t u : NNReal} (hst : s ≤ t) (htu : t ≤ u) : μ (Set.Ioc s u ×ˢ A) = μ (Set.Ioc s t ×ˢ A) + μ (Set.Ioc t u ×ˢ A)

theorem BGW.Probability.indep_consecutive_counts {Ω : 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) (s t : NNReal) : ProbabilityTheory.IndepFun (fun (ω : Ω) => (ξ ω) (Set.Ioc 0 s ×ˢ A)) (fun (ω : Ω) => (ξ ω) (Set.Ioc s (s + t) ×ˢ A)) P

theorem BGW.Probability.prob_noMark_mul {Ω : 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) (s t : NNReal) : P {ω : Ω | (ξ ω) (Set.Ioc 0 (s + t) ×ˢ A) = 0} = P {ω : Ω | (ξ ω) (Set.Ioc 0 s ×ˢ A) = 0} * P {ω : Ω | (ξ ω) (Set.Ioc 0 t ×ˢ A) = 0}

theorem BGW.Probability.prob_noMark_real_eq_one_sub {Ω : 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}).toReal = 1 - (P {ω : Ω | 1 ≤ (ξ ω) (Set.Ioc 0 t ×ˢ A)}).toReal

theorem BGW.Probability.tendsto_prob_noMark_real_zero {Ω : 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) : Filter.Tendsto (fun (t : NNReal) => (P {ω : Ω | (ξ ω) (Set.Ioc 0 t ×ˢ A) = 0}).toReal) (nhdsWithin 0 (Set.Ioi 0)) (nhds 1)