Scalar window probabilities and intensities of a time-simple Lévy point measure.

theorem BGW.Probability.one_le_count_of_ne_zero {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) (hne : μ B ≠ 0) : 1 ≤ μ B

theorem BGW.Probability.ae_one_le_count_of_ne_zero {Ω : 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 ≠ 0 → 1 ≤ (ξ ω) B

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

Stochastic continuity at zero: the probability of at least one A-mark in (0,h] tends to zero as h ↓ 0.

theorem BGW.Probability.windowShift_slice {M : Type u_2} [MeasurableSpace M] {A : Set M} (μ : MeasureTheory.Measure (NNReal × M)) {a b u : NNReal} (hau : a < u) (hub : u ≤ b) (hA : MeasurableSet A) : (windowShift a b μ) ({u - a} ×ˢ A) = μ ({u} ×ˢ A)

theorem BGW.Probability.prob_atom_eq_shift {Ω : 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 u : NNReal} (hau : a < u) (huh : u ≤ a + h) : P {ω : Ω | (ξ ω) ({u} ×ˢ A) ≠ 0} = P {ω : Ω | (ξ ω) ({u - a} ×ˢ A) ≠ 0}

theorem BGW.Probability.prob_atom_pos_eq {Ω : 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) {u v : NNReal} (hu : 0 < u) (hv : 0 < v) : P {ω : Ω | (ξ ω) ({u} ×ˢ A) ≠ 0} = P {ω : Ω | (ξ ω) ({v} ×ˢ A) ≠ 0}

theorem BGW.Probability.ae_not_mark_at {Ω : 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 : NNReal) : ∀ᵐ (ω : Ω) ∂P, (ξ ω) ({s} ×ˢ A) = 0

No deterministic-time atom (derived): for fixed s, a.s. no mark at label s.