Probability bounds on separated doubles and the multiple-arrival estimate.

theorem BGW.Probability.prob_inter_grid {Ω : 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) (h : NNReal) {n : ℕ} (hn : n ≠ 0) {i j : Fin n} (hij : i ≠ j) : P.real ({ω : Ω | (ξ ω) (gridBox h n (↑i) A) ≠ 0} ∩ {ω : Ω | (ξ ω) (gridBox h n (↑j) A) ≠ 0}) = P.real {ω : Ω | (ξ ω) (gridBox h n (↑i) A) ≠ 0} * P.real {ω : Ω | (ξ ω) (gridBox h n (↑j) A) ≠ 0}

theorem BGW.Probability.probReal_ne_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) {B : Set (NNReal × M)} (hB : MeasurableSet B) : P.real {ω : Ω | (ξ ω) B ≠ 0} = 1 - P.real {ω : Ω | (ξ ω) B = 0}

theorem BGW.Probability.prob_noMark_grid {Ω : 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) (h : NNReal) {n i : ℕ} (hn : n ≠ 0) {c : ℝ} (hnc : ∀ (t : NNReal), (P {ω : Ω | (ξ ω) (Set.Ioc 0 t ×ˢ A) = 0}).toReal = Real.exp (-↑t * c)) : P.real {ω : Ω | (ξ ω) (gridBox h n i A) = 0} = Real.exp (-(↑h / ↑n) * c)

theorem BGW.Probability.sum_grid_arrival_le {Ω : 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) (h : NNReal) {n : ℕ} (hn : n ≠ 0) {c : ℝ} (_hc : 0 ≤ c) (hnc : ∀ (t : NNReal), (P {ω : Ω | (ξ ω) (Set.Ioc 0 t ×ˢ A) = 0}).toReal = Real.exp (-↑t * c)) : ∑ i : Fin n, P.real {ω : Ω | (ξ ω) (gridBox h n (↑i) A) ≠ 0} ≤ c * ↑h

theorem BGW.Probability.separatedDoubleNE_real_le {Ω : 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) (h : NNReal) {n : ℕ} (hn : n ≠ 0) {c : ℝ} (hc : 0 ≤ c) (hnc : ∀ (t : NNReal), (P {ω : Ω | (ξ ω) (Set.Ioc 0 t ×ˢ A) = 0}).toReal = Real.exp (-↑t * c)) : P.real (separatedDoubleNE ξ h n A) ≤ (c * ↑h) ^ 2

theorem BGW.Probability.double_real_le_sq {Ω : 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) (h : NNReal) {N : ℕ} {c : ℝ} (hc : 0 ≤ c) (hnc : ∀ (t : NNReal), (P {ω : Ω | (ξ ω) (Set.Ioc 0 t ×ˢ A) = 0}).toReal = Real.exp (-↑t * c)) : P.real {ω : Ω | 2 ≤ (ξ ω) (Set.Ioc 0 h ×ˢ A)} ≤ (c * ↑h) ^ 2

theorem BGW.Probability.prob_two_marks_window_isLittleO {Ω : 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 (h : NNReal) => (P {ω : Ω | 2 ≤ (ξ ω) (Set.Ioc 0 h ×ˢ A)}).toReal / ↑h) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

Small-interval multiple-arrival estimate: P(≥ 2 marks in (0,h]) = o(h).