Projective construction of the open stable bridge

The dyadic horizons approach one. Consistency of the tilted prefixes supplies a unique probability law on their compatible families.

noncomputable def BGW.StableTrees.bridgeHorizon (n : ℕ) : ℝ

The bridge prefix horizons a_n = 1 - 2^{-(n+1)}.

Equations

• BGW.StableTrees.bridgeHorizon n = 1 - (1 / 2) ^ (n + 1)

theorem BGW.StableTrees.strictMono_bridgeHorizon : StrictMono bridgeHorizon

The bridge horizons increase strictly.

theorem BGW.StableTrees.bridgeHorizon_pos (n : ℕ) : 0 < bridgeHorizon n

Every bridge horizon is positive.

theorem BGW.StableTrees.bridgeHorizon_lt_one (n : ℕ) : bridgeHorizon n < 1

Every bridge horizon is strictly smaller than one.

theorem BGW.StableTrees.exists_bridgeHorizon_ge {t : ℝ} (ht : t < 1) : ∃ (n : ℕ), t ≤ bridgeHorizon n

Every time in [0, 1) lies below some horizon.

@[reducible, inline]

abbrev BGW.StableTrees.BridgeOpen : Type

The open-bridge carrier: compatible families of paths on [0, a_n]. Internal encoding of the bridge construction: downstream results (closed-law characterization, reversal, minimum, Vervaat) are stated on D 1 ℝ through stableBridgeLaw, not through BridgeOpen, bridgeOpenLaw or closeBridge.

Equations

• BGW.StableTrees.BridgeOpen = BGW.Skorokhod.CompatiblePaths BGW.StableTrees.bridgeHorizon BGW.StableTrees.strictMono_bridgeHorizon

noncomputable def BGW.StableTrees.BridgeOpen.eval (f : BridgeOpen) (t : ℝ) : ℝ

Totalized evaluation of an open bridge path: the value at t ∈ [0, 1) read in the first coordinate whose horizon is at least t; 0 outside [0, 1).

Equations

• f.eval t = if h : 0 ≤ t ∧ ∃ (n : ℕ), t ≤ BGW.StableTrees.bridgeHorizon n then (↑f (Nat.find ⋯)) ⟨t, ⋯⟩ else 0

theorem BGW.StableTrees.BridgeOpen.coord_restrict (f : BridgeOpen) {n m : ℕ} (hnm : n ≤ m) : Skorokhod.restrict ⋯ (↑f m) = ↑f n

Every later coordinate restricts to an earlier one.

theorem BGW.StableTrees.BridgeOpen.eval_eq_coord (f : BridgeOpen) (n : ℕ) (t : ↑(Set.Icc 0 (bridgeHorizon n))) : f.eval ↑t = (↑f n) t

Evaluation is read consistently in every coordinate whose horizon contains t.

theorem BGW.StableTrees.BridgeOpen.measurable_eval (t : ℝ) : Measurable fun (f : BridgeOpen) => f.eval t

Evaluation of an open bridge at any fixed time is measurable.

noncomputable def BGW.StableTrees.bridgePrefixProb (θ : ℝ) (P : (a : ℝ) → MeasureTheory.ProbabilityMeasure (Skorokhod.D a ℝ)) (n : ℕ) : MeasureTheory.ProbabilityMeasure (Skorokhod.D (bridgeHorizon n) ℝ)

The tilted prefix laws as probability measures on D(a_n, ℝ) (mass one by isProbabilityMeasure_bridgePrefixLaw).

Equations

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

theorem BGW.StableTrees.coe_bridgePrefixProb {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (P : (a : ℝ) → MeasureTheory.ProbabilityMeasure (Skorokhod.D a ℝ)) (hP : ∀ (a : ℝ), 0 < a → a < 1 → IsStableLevyLaw θ a (P a)) (n : ℕ) : ↑(bridgePrefixProb θ P n) = bridgePrefixLaw θ (bridgeHorizon n) ⋯ ↑(P (bridgeHorizon n))

Under the hypotheses, bridgePrefixProb is the tilted prefix law.

theorem BGW.StableTrees.bridgePrefixProb_compatible {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (P : (a : ℝ) → MeasureTheory.ProbabilityMeasure (Skorokhod.D a ℝ)) (hP : ∀ (a : ℝ), 0 < a → a < 1 → IsStableLevyLaw θ a (P a)) (n : ℕ) : (bridgePrefixProb θ P (n + 1)).map (Skorokhod.restrict ⋯) = bridgePrefixProb θ P n

The tilted prefixes are compatible (from bridgePrefix_consistent).

theorem BGW.StableTrees.exists_unique_bridgeOpenLaw {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (P : (a : ℝ) → MeasureTheory.ProbabilityMeasure (Skorokhod.D a ℝ)) (hP : ∀ (a : ℝ), 0 < a → a < 1 → IsStableLevyLaw θ a (P a)) : ∃! Q : MeasureTheory.ProbabilityMeasure BridgeOpen, ∀ (n : ℕ), MeasureTheory.Measure.map (Skorokhod.CompatiblePaths.coord n) ↑Q = bridgePrefixLaw θ (bridgeHorizon n) ⋯ ↑(P (bridgeHorizon n))

Projective bridge: existence and uniqueness. There is exactly one law on the open bridge carrier whose n-th coordinate has the tilted law w_{a_n} · P_{a_n}.

def BGW.StableTrees.BridgeOpen.zero : BridgeOpen

Zero open path (junk).

Equations

• BGW.StableTrees.BridgeOpen.zero = ⟨fun (x : ℕ) => { toFun := fun (x : ↑(Set.Icc 0 (BGW.StableTrees.bridgeHorizon x))) => 0, isCadlag' := ⋯ }, BGW.StableTrees.BridgeOpen.zero._proof_3⟩

noncomputable def BGW.StableTrees.bridgeOpenLaw (θ : ℝ) : MeasureTheory.ProbabilityMeasure BridgeOpen

The open stable bridge law. The exists_unique_bridgeOpenLaw witness for P = stableProcessLaw θ; junk value (Dirac at the zero family) for θ ∉ (1,2].

Equations

• BGW.StableTrees.bridgeOpenLaw θ = if hθ : 1 < θ ∧ θ ≤ 2 then Classical.choose ⋯ else ⟨MeasureTheory.Measure.dirac BGW.StableTrees.BridgeOpen.zero, BGW.StableTrees.bridgeOpenLaw._proof_2⟩

theorem BGW.StableTrees.map_coord_bridgeOpenLaw {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (n : ℕ) : MeasureTheory.Measure.map (Skorokhod.CompatiblePaths.coord n) ↑(bridgeOpenLaw θ) = bridgePrefixLaw θ (bridgeHorizon n) ⋯ ↑(stableProcessLaw θ (bridgeHorizon n))

Prefix characterization of the open stable bridge.

theorem BGW.StableTrees.eq_bridgeOpenLaw {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {Q : MeasureTheory.ProbabilityMeasure BridgeOpen} (hQ : ∀ (n : ℕ), MeasureTheory.Measure.map (Skorokhod.CompatiblePaths.coord n) ↑Q = bridgePrefixLaw θ (bridgeHorizon n) ⋯ ↑(stableProcessLaw θ (bridgeHorizon n))) : Q = bridgeOpenLaw θ

Uniqueness of the open stable bridge law by its prefixes.