Measurable finite random measures on the predictable marked space.

See Bertoin, Lévy Processes, Chapter IV, and Kallenberg, Foundations of Modern Probability, Chapters 12 and 22.

noncomputable def BGW.StableTrees.predictableMarkedMeasure (f : Skorokhod.DLoc) (μ : MeasureTheory.Measure (NNReal × Excursion)) : MeasureTheory.Measure ((NNReal × Skorokhod.DLoc) × Excursion)

Attach the sample path to a time-mark measure, with the predictable target sigma algebra.

Equations

• BGW.StableTrees.predictableMarkedMeasure f μ = MeasureTheory.Measure.map (fun (p : NNReal × BGW.StableTrees.Excursion) => ((p.1, f), p.2)) μ

theorem BGW.StableTrees.measurable_predictableMarkedMeasure {μ : Skorokhod.DLoc → MeasureTheory.Measure (NNReal × Excursion)} (hμ : Measurable μ) [∀ (f : Skorokhod.DLoc), MeasureTheory.IsFiniteMeasure (μ f)] : Measurable fun (f : Skorokhod.DLoc) => predictableMarkedMeasure f (μ f)

Finite measurable random measures remain measurable after the predictable sample-path coordinate is attached. This uses the pi system of predictable rectangles.