Dyadic separation of distinct arrivals and the small-window multiple-arrival estimate.

theorem BGW.Probability.exists_ne_of_one_lt_count {M : Type u_2} [MeasurableSpace M] {μ : MeasureTheory.Measure (NNReal × M)} {S : Set (NNReal × M)} (hμ : μ = MeasureTheory.Measure.sum fun (p : ↑S) => MeasureTheory.Measure.dirac ↑p) {B : Set (NNReal × M)} (hB : MeasurableSet B) (h : 1 < μ B) : ∃ (p : ↑S) (q : ↑S), p ≠ q ∧ ↑p ∈ B ∧ ↑q ∈ B

A counting measure assigning mass greater than one contains two distinct points.

noncomputable def BGW.Probability.pointGridTime (h : NNReal) (n i : ℕ) : NNReal

The left endpoint of cell i in a uniform n-cell partition of (0, h].

Equations

• BGW.Probability.pointGridTime h n i = h * ↑i / ↑n

noncomputable def BGW.Probability.gridBox {M : Type u_2} (h : NNReal) (n i : ℕ) (A : Set M) : Set (NNReal × M)

The set of points in cell i of a uniform time partition and with mark in A.

Equations

• BGW.Probability.gridBox h n i A = Set.Ioc (BGW.Probability.pointGridTime h n i) (BGW.Probability.pointGridTime h n (i + 1)) ×ˢ A

def BGW.Probability.separatedDouble {Ω : Type u_1} {M : Type u_2} [MeasurableSpace M] (ξ : Ω → MeasureTheory.Measure (NNReal × M)) (h : NNReal) (n : ℕ) (A : Set M) : Set Ω

The event that two different grid cells each contain an arrival.

Equations

• BGW.Probability.separatedDouble ξ h n A = {ω : Ω | ∃ (i : Fin n) (j : Fin n), i < j ∧ 1 ≤ (ξ ω) (BGW.Probability.gridBox h n (↑i) A) ∧ 1 ≤ (ξ ω) (BGW.Probability.gridBox h n (↑j) A)}

theorem BGW.Probability.pointGridTime_monotone (h : NNReal) {n : ℕ} (hn : n ≠ 0) : Monotone (pointGridTime h n)

theorem BGW.Probability.pointGridTime_start (h : NNReal) (n : ℕ) : pointGridTime h n 0 = 0

theorem BGW.Probability.pointGridTime_end (h : NNReal) {n : ℕ} (hn : n ≠ 0) : pointGridTime h n n = h

theorem BGW.Probability.pointGridTime_width (h : NNReal) {n i : ℕ} (hn : n ≠ 0) : pointGridTime h n (i + 1) - pointGridTime h n i = h / ↑n

theorem BGW.Probability.exists_grid_box {h : NNReal} {n : ℕ} (hn : n ≠ 0) {x : NNReal} (hx : x ∈ Set.Ioc 0 h) : ∃ (i : Fin n), x ∈ Set.Ioc (pointGridTime h n ↑i) (pointGridTime h n (↑i + 1))

theorem BGW.Probability.pointGridTime_two_even (h : NNReal) {n : ℕ} (hn : n ≠ 0) (i : ℕ) : pointGridTime h (2 * n) (2 * i) = pointGridTime h n i

theorem BGW.Probability.pointGridTime_two_odd (h : NNReal) {n : ℕ} (hn : n ≠ 0) (i : ℕ) : pointGridTime h (2 * n) (2 * i + 1) = (pointGridTime h n i + pointGridTime h n (i + 1)) / 2

theorem BGW.Probability.exists_mem_of_one_le_count {M : Type u_2} [MeasurableSpace M] {μ : MeasureTheory.Measure (NNReal × M)} {S : Set (NNReal × M)} (hμ : μ = MeasureTheory.Measure.sum fun (p : ↑S) => MeasureTheory.Measure.dirac ↑p) {B : Set (NNReal × M)} (hB : MeasurableSet B) (h : 1 ≤ μ B) : ∃ (p : ↑S), ↑p ∈ B

theorem BGW.Probability.separatedDouble_subset_double {Ω : Type u_1} {M : Type u_2} [MeasurableSpace M] {ξ : Ω → MeasureTheory.Measure (NNReal × M)} {A : Set M} {h : NNReal} {n : ℕ} (hn : n ≠ 0) (hAm : MeasurableSet A) : separatedDouble ξ h n A ⊆ {ω : Ω | 2 ≤ (ξ ω) (Set.Ioc 0 h ×ˢ A)}

theorem BGW.Probability.ae_double_eq_iUnion_separated {Ω : 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) : {ω : Ω | 2 ≤ (ξ ω) (Set.Ioc 0 h ×ˢ A)} =ᵐ[P] ⋃ (N : ℕ), separatedDouble ξ h (2 ^ N) A

def BGW.Probability.separatedDoubleNE {Ω : Type u_1} {M : Type u_2} [MeasurableSpace M] (ξ : Ω → MeasureTheory.Measure (NNReal × M)) (h : NNReal) (n : ℕ) (A : Set M) : Set Ω

The nonzero-arrival version of separatedDouble, useful for exact refinement.

Equations

• BGW.Probability.separatedDoubleNE ξ h n A = {ω : Ω | ∃ (i : Fin n) (j : Fin n), i < j ∧ (ξ ω) (BGW.Probability.gridBox h n (↑i) A) ≠ 0 ∧ (ξ ω) (BGW.Probability.gridBox h n (↑j) A) ≠ 0}

theorem BGW.Probability.separatedDouble_subset_NE {Ω : Type u_1} {M : Type u_2} [MeasurableSpace M] {ξ : Ω → MeasureTheory.Measure (NNReal × M)} {A : Set M} {h : NNReal} {n : ℕ} : separatedDouble ξ h n A ⊆ separatedDoubleNE ξ h n A

theorem BGW.Probability.gridBox_split {M : Type u_2} [MeasurableSpace M] {A : Set M} (h : NNReal) (_hAm : MeasurableSet A) {n : ℕ} (hn : n ≠ 0) (i : Fin n) : gridBox h n (↑i) A = gridBox h (2 * n) (2 * ↑i) A ∪ gridBox h (2 * n) (2 * ↑i + 1) A

theorem BGW.Probability.separatedDoubleNE_mono_two {Ω : Type u_1} {M : Type u_2} [MeasurableSpace M] {ξ : Ω → MeasureTheory.Measure (NNReal × M)} {A : Set M} (h : NNReal) (hAm : MeasurableSet A) {n : ℕ} (hn : n ≠ 0) : separatedDoubleNE ξ h n A ⊆ separatedDoubleNE ξ h (2 * n) A

theorem BGW.Probability.separatedDoubleNE_mono {Ω : Type u_1} {M : Type u_2} [MeasurableSpace M] {ξ : Ω → MeasureTheory.Measure (NNReal × M)} {A : Set M} (h : NNReal) (hAm : MeasurableSet A) : Monotone fun (N : ℕ) => separatedDoubleNE ξ h (2 ^ N) A

theorem BGW.Probability.ae_double_eq_iUnion_separatedNE {Ω : 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) : {ω : Ω | 2 ≤ (ξ ω) (Set.Ioc 0 h ×ˢ A)} =ᵐ[P] ⋃ (N : ℕ), separatedDoubleNE ξ h (2 ^ N) A

theorem BGW.Probability.pointGridTime_succ_eq_add (h : NNReal) {n i : ℕ} (hn : n ≠ 0) : pointGridTime h n (i + 1) = pointGridTime h n i + h / ↑n

theorem BGW.Probability.prob_noMark_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) : P {ω : Ω | (ξ ω) (Set.Ioc a (a + h) ×ˢ A) = 0} = P {ω : Ω | (ξ ω) (Set.Ioc 0 h ×ˢ A) = 0}

theorem BGW.Probability.iIndep_grid_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) (h : NNReal) {n : ℕ} (hn : n ≠ 0) : ProbabilityTheory.iIndepFun (fun (i : Fin n) (ω : Ω) => (ξ ω) (gridBox h n (↑i) A)) P