Transfer of prefix events with an independent fresh path #
A measurable event that reads its first path only up to a fixed horizon has the same probability for the reversed prefix and fresh increments as for two independent stable paths.
theorem
BGW.StableTrees.measure_reversed_prefix_fresh_event
{θ : ℝ}
(hθ : 1 < θ ∧ θ ≤ 2)
{t : NNReal}
(ht : 0 < t)
{E : Set (Skorokhod.DLoc × Skorokhod.DLoc)}
(hE : MeasurableSet E)
(hloc :
∀ (f g h : Skorokhod.DLoc), Skorokhod.DLoc.restrict t f = Skorokhod.DLoc.restrict t g → ((f, h) ∈ E ↔ (g, h) ∈ E))
:
↑(stableLocalLaw θ) {f : Skorokhod.DLoc | (reversedAt t f, Skorokhod.DLoc.shift t f) ∈ E} = ((↑(stableLocalLaw θ)).prod ↑(stableLocalLaw θ)) E
Prefix-local events transfer together with independent fresh increments.
theorem
BGW.StableTrees.supLocalTime_eq_of_restrict_eq
(θ : ℝ)
{t : NNReal}
(f g : Skorokhod.DLoc)
(he : Skorokhod.DLoc.restrict t f = Skorokhod.DLoc.restrict t g)
(u : NNReal)
(hu : u ≤ t)
:
Equality of compact prefixes preserves the supremum clock at every earlier age.
theorem
BGW.StableTrees.supRunning_eq_of_restrict_eq
{t : NNReal}
(f g : Skorokhod.DLoc)
(he : Skorokhod.DLoc.restrict t f = Skorokhod.DLoc.restrict t g)
(u : NNReal)
(hu : u ≤ t)
:
Equality of compact prefixes preserves the running supremum at every earlier age.