Consistent path-law families on growing horizons

Construct the unique law on compatible càdlàg path families from consistent laws on an increasing sequence of time horizons.

The construction uses the Kolmogorov extension theorem of the vendored kolmogorov_extension4 (R. Degenne and P. Pfaffelhuber), applied to the projective family of restrictions; see also O. Kallenberg, Foundations of Modern Probability, Theorem 8.21.

def BGW.Skorokhod.CompatiblePaths (b : ℕ → ℝ) (hb : StrictMono b) : Type

Compatible horizon families with adjacent restrictions agreeing.

Equations

• BGW.Skorokhod.CompatiblePaths b hb = { p : (n : ℕ) → BGW.Skorokhod.D (b n) ℝ // ∀ (n : ℕ), BGW.Skorokhod.restrict ⋯ (p (n + 1)) = p n }

@[instance_reducible]

noncomputable instance BGW.Skorokhod.instMeasurableSpaceCompatiblePaths (b : ℕ → ℝ) (hb : StrictMono b) : MeasurableSpace (CompatiblePaths b hb)

The compatible-family subtype carries its subspace measurable structure.

Equations

• BGW.Skorokhod.instMeasurableSpaceCompatiblePaths b hb = inferInstance

def BGW.Skorokhod.CompatiblePaths.coord {b : ℕ → ℝ} {hb : StrictMono b} (n : ℕ) (p : CompatiblePaths b hb) : D (b n) ℝ

The coordinate map of the compatible-family subtype.

Equations

• BGW.Skorokhod.CompatiblePaths.coord n p = ↑p n

theorem BGW.Skorokhod.CompatiblePaths.measurable_coord (b : ℕ → ℝ) (hb : StrictMono b) (n : ℕ) : Measurable (coord n)

Coordinate maps on compatible families are measurable.

theorem BGW.Skorokhod.CompatiblePaths.measure_ext (b : ℕ → ℝ) (hb : StrictMono b) {Q Q' : MeasureTheory.Measure (CompatiblePaths b hb)} [MeasureTheory.IsFiniteMeasure Q] (h : ∀ (n : ℕ), MeasureTheory.Measure.map (coord n) Q = MeasureTheory.Measure.map (coord n) Q') : Q = Q'

Finite measures on compatible paths are determined by their coordinate marginals.

theorem BGW.Skorokhod.measurableSet_compatible (b : ℕ → ℝ) (hb : StrictMono b) : MeasurableSet {p : (n : ℕ) → D (b n) ℝ | ∀ (n : ℕ), restrict ⋯ (p (n + 1)) = p n}

The set of compatible product paths is measurable.

theorem BGW.Skorokhod.map_restrict_eq_of_le (b : ℕ → ℝ) (hb : StrictMono b) (P : (k : ℕ) → MeasureTheory.ProbabilityMeasure (D (b k) ℝ)) (hP : ∀ (k : ℕ), (P (k + 1)).map (restrict ⋯) = P k) {n m : ℕ} (hnm : n ≤ m) : (P m).map (restrict ⋯) = P n

Consistency at adjacent horizons implies consistency at every pair of horizons.

noncomputable def BGW.Skorokhod.maxIndexLaw (b : ℕ → ℝ) (hb : StrictMono b) (P : (n : ℕ) → MeasureTheory.ProbabilityMeasure (D (b n) ℝ)) (J : Finset ℕ) : MeasureTheory.Measure ((j : ↥J) → D (b ↑j) ℝ)

The law on a finite index set obtained by restricting the law at its largest horizon.

Equations

• BGW.Skorokhod.maxIndexLaw b hb P J = MeasureTheory.Measure.map (fun (f : BGW.Skorokhod.D (b (J.sup id)) ℝ) (j : ↥J) => BGW.Skorokhod.restrict ⋯ f) ↑(P (J.sup id))

theorem BGW.Skorokhod.isProjectiveMeasureFamily_maxIndexLaw (b : ℕ → ℝ) (hb : StrictMono b) (P : (n : ℕ) → MeasureTheory.ProbabilityMeasure (D (b n) ℝ)) (hP : ∀ (n : ℕ), (P (n + 1)).map (restrict ⋯) = P n) : MeasureTheory.IsProjectiveMeasureFamily (maxIndexLaw b hb P)

The max-index laws form a projective family over finite index sets.

theorem BGW.Skorokhod.exists_unique_compatiblePathLaw (b : ℕ → ℝ) (hb : StrictMono b) (hb0 : ∀ (n : ℕ), 0 < b n) (P : (n : ℕ) → MeasureTheory.ProbabilityMeasure (D (b n) ℝ)) (hP : ∀ (n : ℕ), (P (n + 1)).map (restrict ⋯) = P n) : ∃! Q : MeasureTheory.ProbabilityMeasure (CompatiblePaths b hb), ∀ (n : ℕ), MeasureTheory.Measure.map (CompatiblePaths.coord n) ↑Q = ↑(P n)

Existence and uniqueness of the compatible path law with prescribed coordinate marginals.