Height of the straddling excursion

The continuous height of the normalized excursion straddling a fixed positive time is the normalized host height. The joint law of the normalized path and height is excLaw, and it is independent of the age and lifetime of the straddling excursion.

Definition

noncomputable def BGW.StableTrees.straddleHeightPath (θ : ℝ) (t : NNReal) (f : Skorokhod.DLoc) : C(↑(Set.Icc 0 1), ℝ)

Normalized host height of the straddling excursion (C25, height part): the continuous function s ↦ ζ_t^{1/θ-1} H_{g_t + ζ_t s} on [0,1], with H = heightLoc θ f the continuous height of the host path.

Equations

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

Almost-sure identification

theorem BGW.StableTrees.ae_heightLoc_straddling {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {t : NNReal} (ht : 0 < t) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ u ≤ straddleEnd t f - straddleStart t f, heightLoc θ f (straddleStart t f + u) = (excursionHeight θ (straddlingExcursion t f)) u

Locality at the straddling level: almost surely, the host height on [g_t, d_t] is the height of the straddling excursion, H_{g_t + u} = H(e_t)(u) for u ≤ d_t - g_t.

theorem BGW.StableTrees.ae_heightLoc_straddle_endpoints {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (t : NNReal) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), heightLoc θ f (straddleStart t f) = 0 ∧ heightLoc θ f (straddleEnd t f) = 0

The host height vanishes at both ends g_t and d_t of the straddling excursion.

theorem BGW.StableTrees.ae_excursionHeight_straddling_scale {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {t : NNReal} (ht : 0 < t) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ (s : NNReal), (excursionHeight θ (straddlingExcursion t f)) ((straddlingExcursion t f).lifetime * s) = ↑(straddlingExcursion t f).lifetime ^ (1 - 1 / θ) * (excursionHeight θ (normalizeExc θ (straddlingExcursion t f))) s

Scaling of the straddling excursion's height (the H04 normalization identity at the random lifetime ζ_t): H(e_t)(ζ s) = ζ^{1-1/θ} H(normalizeExc e_t)(s) for all s, a.s.

theorem BGW.StableTrees.ae_excursionHeight_normalize_straddling {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {t : NNReal} (ht : 0 < t) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ s ≤ 1, (excursionHeight θ (normalizeExc θ (straddlingExcursion t f))) s = straddleLife t f ^ (1 / θ - 1) * heightLoc θ f (straddleStart t f + (straddleEnd t f - straddleStart t f) * s)

Duquesne's pathHexc identity (C25, height part, pointwise form): almost surely, for all s ∈ [0,1], the height of the normalized straddling excursion is ζ_t^{1/θ-1} H_{g_t + ζ_t s}.

theorem BGW.StableTrees.ae_excursionPair_normalize_straddling {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {t : NNReal} (ht : 0 < t) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), excursionPair θ 1 (normalizeExc θ (straddlingExcursion t f)) = (excursionRestrict 1 (normalizeExc θ (straddlingExcursion t f)), straddleHeightPath θ t f)

Pair identity: almost surely, the J01 pair of the normalized straddling excursion is (normalized straddling path on [0,1], normalized host height).

Laws

theorem BGW.StableTrees.map_straddleHeight_eq_excLaw {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {t : NNReal} (ht : 0 < t) : MeasureTheory.Measure.map (fun (f : Skorokhod.DLoc) => (excursionRestrict 1 (normalizeExc θ (straddlingExcursion t f)), straddleHeightPath θ t f)) ↑(stableLocalLaw θ) = ↑(excLaw θ)

C25 (height part), joint law. The normalized straddling path on [0,1] and the normalized host height s ↦ ζ_t^{1/θ-1} H_{g_t + ζ_t s} have JOINTLY the law excLaw θ of (X^exc, H^exc).

theorem BGW.StableTrees.map_straddleHeightPath_eq {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {t : NNReal} (ht : 0 < t) : MeasureTheory.Measure.map (straddleHeightPath θ t) ↑(stableLocalLaw θ) = MeasureTheory.Measure.map Prod.snd ↑(excLaw θ)

Height marginal: s ↦ ζ_t^{1/θ-1} H_{g_t + ζ_t s} has the law of H^exc.

theorem BGW.StableTrees.map_straddleHeightData_eq_prod {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {t : NNReal} (ht : 0 < t) : MeasureTheory.Measure.map (fun (f : Skorokhod.DLoc) => ((↑(straddleStart t f), straddleLife t f), excursionRestrict 1 (normalizeExc θ (straddlingExcursion t f)), straddleHeightPath θ t f)) ↑(stableLocalLaw θ) = (straddleLaw θ t).prod ↑(excLaw θ)

Joint law with the age and lifetime: ((g_t, ζ_t), (path, height)) has the product law straddleLaw θ t ⊗ excLaw θ (independence of (g_t, ζ_t) and the normalized pair).