Basic definitions and measurability lemmas for time-simple random point measures.

noncomputable def BGW.Probability.natCount {M : Type u_2} [MeasurableSpace M] (μ : MeasureTheory.Measure (NNReal × M)) (B : Set (NNReal × M)) : ℕ

The count of a set read in ℕ (junk 0 for an infinite count, a.s. irrelevant).

Equations

• BGW.Probability.natCount μ B = ⌊(μ B).toNNReal⌋₊

noncomputable def BGW.Probability.windowRestrict {M : Type u_2} [MeasurableSpace M] (a b : NNReal) (μ : MeasureTheory.Measure (NNReal × M)) : MeasureTheory.Measure (NNReal × M)

The restriction of a point measure to the time window (a, b] (all marks).

Equations

• BGW.Probability.windowRestrict a b μ = μ.restrict (Set.Ioc a b ×ˢ Set.univ)

noncomputable def BGW.Probability.windowShift {M : Type u_2} [MeasurableSpace M] (a b : NNReal) (μ : MeasureTheory.Measure (NNReal × M)) : MeasureTheory.Measure (NNReal × M)

The same window, translated to start at time 0.

Equations

• BGW.Probability.windowShift a b μ = MeasureTheory.Measure.map (fun (p : NNReal × M) => (p.1 - a, p.2)) (BGW.Probability.windowRestrict a b μ)

noncomputable def BGW.Probability.naturalHistory {Ω : Type u_1} {M : Type u_2} [MeasurableSpace M] (ξ : Ω → MeasureTheory.Measure (NNReal × M)) (t : NNReal) : MeasurableSpace Ω

The natural history of ξ up to time t: the σ-algebra generated by ξ restricted to [0,t] × M.

Equations

• BGW.Probability.naturalHistory ξ t = MeasurableSpace.comap (fun (ω : Ω) => (ξ ω).restrict (Set.Iic t ×ˢ Set.univ)) inferInstance

structure BGW.Probability.IsTimeSimpleLevy {Ω : Type u_1} {M : Type u_2} [MeasurableSpace Ω] [MeasurableSpace M] (P : MeasureTheory.Measure Ω) (ξ : Ω → MeasureTheory.Measure (NNReal × M)) : Prop

Time-simple finite-rate random point measure: the structural hypotheses of the characterization.

• measurable : Measurable ξ
• atZero : ∀ᵐ (ω : Ω) ∂P, (ξ ω) ({0} ×ˢ Set.univ) = 0

  zero mass at label 0

• counting : ∀ᵐ (ω : Ω) ∂P, ∃ (S : Set (NNReal × M)), S.Countable ∧ ξ ω = MeasureTheory.Measure.sum fun (p : ↑S) => MeasureTheory.Measure.dirac ↑p

  counting measure: a countable sum of unit point masses.

• timeSimple : ∀ᵐ (ω : Ω) ∂P, ∀ (s : NNReal), (ξ ω) ({s} ×ˢ Set.univ) ≤ 1

  time-simplicity: almost surely at most one mark per time label.

• stationary (a h : NNReal) : MeasureTheory.Measure.map (fun (ω : Ω) => windowShift a (a + h) (ξ ω)) P = MeasureTheory.Measure.map (fun (ω : Ω) => windowShift 0 h (ξ ω)) P

  stationarity of window restrictions

• indep (n : ℕ) (t : Fin (n + 1) → NNReal) : Monotone t → ProbabilityTheory.iIndepFun (fun (i : Fin n) (ω : Ω) => windowRestrict (t i.castSucc) (t i.succ) (ξ ω)) P

  independence of restrictions to consecutive windows

def BGW.Probability.IsFiniteRate {Ω : Type u_1} {M : Type u_2} [MeasurableSpace Ω] [MeasurableSpace M] (P : MeasureTheory.Measure Ω) (ξ : Ω → MeasureTheory.Measure (NNReal × M)) (A : Set M) : Prop

A measurable set of marks of finite rate: finitely many marks in (0,t] × A a.s.

Equations

• BGW.Probability.IsFiniteRate P ξ A = (MeasurableSet A ∧ ∀ (t : NNReal), ∀ᵐ (ω : Ω) ∂P, (ξ ω) (Set.Ioc 0 t ×ˢ A) < ⊤)

noncomputable def BGW.Probability.markRate {Ω : Type u_1} {M : Type u_2} [MeasurableSpace Ω] [MeasurableSpace M] (P : MeasureTheory.Measure Ω) (ξ : Ω → MeasureTheory.Measure (NNReal × M)) (A : Set M) : ENNReal

The mark rate of A: E ξ((0,1] × A).

Equations

• BGW.Probability.markRate P ξ A = ∫⁻ (ω : Ω), (ξ ω) (Set.Ioc 0 1 ×ˢ A) ∂P

theorem BGW.Probability.measurable_box {M : Type u_2} [MeasurableSpace M] {A : Set M} {a b : NNReal} (hA : MeasurableSet A) : MeasurableSet (Set.Ioc a b ×ˢ A)

theorem BGW.Probability.measurable_count {Ω : Type u_1} {M : Type u_2} [MeasurableSpace Ω] [MeasurableSpace M] {ξ : Ω → MeasureTheory.Measure (NNReal × M)} (hξ : Measurable ξ) {B : Set (NNReal × M)} (hB : MeasurableSet B) : Measurable fun (ω : Ω) => (ξ ω) B

theorem BGW.Probability.measurable_natCount {Ω : Type u_1} {M : Type u_2} [MeasurableSpace Ω] [MeasurableSpace M] {ξ : Ω → MeasureTheory.Measure (NNReal × M)} (hξ : Measurable ξ) {B : Set (NNReal × M)} (hB : MeasurableSet B) : Measurable fun (ω : Ω) => natCount (ξ ω) B

theorem BGW.Probability.measurable_restrict_pointMeasure {Ω : Type u_1} {M : Type u_2} [MeasurableSpace Ω] [MeasurableSpace M] {ξ : Ω → MeasureTheory.Measure (NNReal × M)} (hξ : Measurable ξ) {B : Set (NNReal × M)} (hB : MeasurableSet B) : Measurable fun (ω : Ω) => (ξ ω).restrict B

theorem BGW.Probability.measurable_windowRestrict {Ω : Type u_1} {M : Type u_2} [MeasurableSpace Ω] [MeasurableSpace M] {ξ : Ω → MeasureTheory.Measure (NNReal × M)} (hξ : Measurable ξ) (a b : NNReal) : Measurable fun (ω : Ω) => windowRestrict a b (ξ ω)

theorem BGW.Probability.measurable_windowShift {Ω : Type u_1} {M : Type u_2} [MeasurableSpace Ω] [MeasurableSpace M] {ξ : Ω → MeasureTheory.Measure (NNReal × M)} (hξ : Measurable ξ) (a b : NNReal) : Measurable fun (ω : Ω) => windowShift a b (ξ ω)

theorem BGW.Probability.measurable_historyRestriction {Ω : Type u_1} {M : Type u_2} [MeasurableSpace Ω] [MeasurableSpace M] {ξ : Ω → MeasureTheory.Measure (NNReal × M)} (hξ : Measurable ξ) (s : NNReal) : Measurable fun (ω : Ω) => (ξ ω).restrict (Set.Iic s ×ˢ Set.univ)

theorem BGW.Probability.measurable_markRate {Ω : 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) : Measurable fun (ω : Ω) => (ξ ω) (Set.Ioc 0 1 ×ˢ A)

theorem BGW.Probability.restrict_apply_box {M : Type u_2} [MeasurableSpace M] {A : Set M} (μ : MeasureTheory.Measure (NNReal × M)) {a b : NNReal} (_hA : MeasurableSet A) : (windowRestrict a b μ) (Set.Ioc 0 (b - a) ×ˢ A) = μ (Set.Ioc 0 (b - a) ×ˢ A ∩ Set.Ioc a b ×ˢ Set.univ)