Generators and measurable sections for the stopped-filtration predictable sigma algebra.

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

def BGW.StableTrees.predictableSigma : MeasurableSpace (NNReal × Skorokhod.DLoc)

The predictable σ-algebra on ℝ≥0 × DLoc of the filtration G_x = F_{T_x} ((isStoppingTime_firstPassageBelow x).measurableSpace): generated by the rectangles (a,b] × F with a ≤ b, F ∈ G_a, and {0} × F with F ∈ G_0. (Not packaged as a Mathlib Filtration, to avoid proving monotonicity/≤ m of G just for the statement.)

Equations

• One or more equations did not get rendered due to their size.

def BGW.StableTrees.excursionPredictableRectangles : Set (Set (NNReal × Skorokhod.DLoc))

The elementary rectangles generating the stopped-filtration predictable sigma algebra.

Equations

• One or more equations did not get rendered due to their size.

theorem BGW.StableTrees.predictableSigma_eq_generate : predictableSigma = MeasurableSpace.generateFrom (insert Set.univ excursionPredictableRectangles)

Predictable measurability is generated by elementary rectangles and the whole space.

theorem BGW.StableTrees.isPiSystem_excursionPredictableRectangles : IsPiSystem excursionPredictableRectangles

The elementary predictable rectangles form a pi system.

theorem BGW.StableTrees.predictableSigma_le_prod : predictableSigma ≤ inferInstance

Every predictable set is measurable for the ambient product sigma algebra.

theorem BGW.StableTrees.measurable_predictable_timeSection (f : Skorokhod.DLoc) : Measurable fun (x : NNReal) => (x, f)

At a fixed sample path, the time section into the predictable space is measurable.