Measurable closure of open bridge paths

The full terminal-limit event is measurable. On that event, adding the terminal value zero preserves the càdlàg property.

def BGW.StableTrees.BridgeOpen.terminalLimit : Set BridgeOpen

The terminal-limit event: f(t) → 0 as t ↑ 1 (full path limit, not convergence in probability of X_t).

Equations

• BGW.StableTrees.BridgeOpen.terminalLimit = {f : BGW.StableTrees.BridgeOpen | Filter.Tendsto f.eval (nhdsWithin 1 (Set.Iio 1)) (nhds 0)}

theorem BGW.StableTrees.BridgeOpen.measurableSet_terminalLimit : MeasurableSet terminalLimit

The full terminal-limit event is measurable.

theorem BGW.StableTrees.isCadlag_closeFun {f : BridgeOpen} (h : f ∈ BridgeOpen.terminalLimit) : IsCadlag fun (t : ↑(Set.Icc 0 1)) => if ↑t < 1 then f.eval ↑t else 0

On the terminal-limit event, extending an open path by 0 at time 1 gives a càdlàg path on [0, 1].

noncomputable def BGW.StableTrees.closeBridge (f : BridgeOpen) : Skorokhod.D 1 ℝ

Closing the bridge: extend an open path by the value 0 at time 1 on the terminal-limit event; the zero path on its complement.

Equations

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

theorem BGW.StableTrees.measurable_closeBridge : Measurable closeBridge

Closing is measurable (D 1 ℝ carries its Borel σ-algebra, generated by evaluations).

theorem BGW.StableTrees.restrict_closeBridge {f : BridgeOpen} (hf : f ∈ BridgeOpen.terminalLimit) (n : ℕ) : Skorokhod.restrict ⋯ (closeBridge f) = ↑f n

On the terminal-limit event, the closed path restricts to the n-th coordinate.

noncomputable def BGW.StableTrees.stableBridgeLaw (θ : ℝ) : MeasureTheory.ProbabilityMeasure (Skorokhod.D 1 ℝ)

The stable bridge law on D 1 ℝ (bridge from 0 to 0): image of the open law under closeBridge. Junk value: image of the junk open law (a Dirac mass at the zero path).

Equations

• BGW.StableTrees.stableBridgeLaw θ = (BGW.StableTrees.bridgeOpenLaw θ).map BGW.StableTrees.closeBridge