Joint excursion path and height laws

This module constructs the unit and tail laws of an excursion together with its continuous height. It proves their marginals and projectivity, identifies their prefixes using the common measurable height graph, transfers the lifetime mixture and Gamma identity, and gives the Brownian specialization.

Pair maps

noncomputable def BGW.StableTrees.heightRestrict (T : NNReal) (g : C(NNReal, ℝ)) : C(↑(Set.Icc 0 ↑T), ℝ)

Restriction of a continuous function on ℝ≥0 to [0,T].

Equations

• BGW.StableTrees.heightRestrict T g = g.comp { toFun := fun (t : ↑(Set.Icc 0 ↑T)) => ⟨↑t, ⋯⟩, continuous_toFun := ⋯ }

noncomputable def BGW.StableTrees.excursionPair (θ : ℝ) (T : NNReal) (e : Excursion) : Skorokhod.D ↑T ℝ × C(↑(Set.Icc 0 ↑T), ℝ)

The excursion/height pair on [0,T]: the restricted path and the restricted height of the same excursion.

Equations

• BGW.StableTrees.excursionPair θ T e = (BGW.StableTrees.excursionRestrict T e, BGW.StableTrees.heightRestrict T (BGW.StableTrees.excursionHeight θ e))

noncomputable def BGW.StableTrees.restrictPair {a T : NNReal} (h : a ≤ T) (z : Skorokhod.D ↑T ℝ × C(↑(Set.Icc 0 ↑T), ℝ)) : Skorokhod.D ↑a ℝ × C(↑(Set.Icc 0 ↑a), ℝ)

Restriction of a pair on [0,T] to [0,a], for a ≤ T.

Equations

• BGW.StableTrees.restrictPair h z = (BGW.Skorokhod.restrict ⋯ z.1, z.2.comp { toFun := Set.inclusion ⋯, continuous_toFun := ⋯ })

noncomputable def BGW.StableTrees.extendHeight (h : C(↑(Set.Icc 0 1), ℝ)) : C(NNReal, ℝ)

Extension of a continuous function on [0,1] to ℝ≥0 by its terminal value.

Equations

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

noncomputable def BGW.StableTrees.scaleHeight (θ : ℝ) (c : ↑(Set.Ioi 0)) (g : C(NNReal, ℝ)) : C(NNReal, ℝ)

Height scaling t ↦ c^(1-1/θ) g(t/c), with the time convention of the sealed scaleLoc.

Equations

• BGW.StableTrees.scaleHeight θ c g = { toFun := fun (t : NNReal) => ↑c ^ (1 - 1 / θ) * g (t / (↑c).toNNReal), continuous_toFun := ⋯ }

noncomputable def BGW.StableTrees.pairStretch (θ : ℝ) (T : NNReal) (u : ↑(Set.Ioi 0)) (z : Skorokhod.D 1 ℝ × C(↑(Set.Icc 0 1), ℝ)) : Skorokhod.D ↑T ℝ × C(↑(Set.Icc 0 ↑T), ℝ)

A unit pair stretched to lifetime u on the horizon [0,T], with one common u: path t ↦ u^(1/θ) x((t/u) ∧ 1) and height t ↦ u^(1-1/θ) h((t/u) ∧ 1) (both stopped at time 1 of the unit pair, whose terminal values vanish a.s. under excLaw θ).

Equations

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

Joint laws

noncomputable def BGW.StableTrees.excLaw (θ : ℝ) : MeasureTheory.ProbabilityMeasure (Skorokhod.D 1 ℝ × C(↑(Set.Icc 0 1), ℝ))

The normalized excursion/height law on D 1 ℝ × C([0,1], ℝ): the image of the unit excursion law under the pair map (path and height of the same excursion).

Equations

• BGW.StableTrees.excLaw θ = (BGW.StableTrees.unitExcursionLaw θ).map (BGW.StableTrees.excursionPair θ 1)

noncomputable def BGW.StableTrees.tailExcLaw (θ : ℝ) (T : NNReal) : MeasureTheory.ProbabilityMeasure (Skorokhod.D ↑T ℝ × C(↑(Set.Icc 0 ↑T), ℝ))

The tail excursion/height law on the horizon [0,T]: the image of N(· | ζ > 1) under the pair map (the whole excursion, stopped at zero after its lifetime).

Equations

• BGW.StableTrees.tailExcLaw θ T = (BGW.StableTrees.tailExcursionLaw θ).map (BGW.StableTrees.excursionPair θ T)

Measurability guards

theorem BGW.StableTrees.measurable_excursionPair (θ : ℝ) (T : NNReal) : Measurable (excursionPair θ T)

The pair map is measurable (so excLaw and tailExcLaw are not junk images).

theorem BGW.StableTrees.measurable_restrictPair {a T : NNReal} (h : a ≤ T) : Measurable (restrictPair h)

Restriction of pairs is measurable.

theorem BGW.StableTrees.measurable_pairStretch (θ : ℝ) (T : NNReal) (u : ↑(Set.Ioi 0)) : Measurable (pairStretch θ T u)

Stretching of pairs is measurable, for each lifetime u.

Marginals and projectivity

theorem BGW.StableTrees.excLaw_map_fst (θ : ℝ) : (excLaw θ).map Prod.fst = levyExcLaw θ

First marginal of excLaw: exactly the sealed levyExcLaw θ (every θ).

theorem BGW.StableTrees.tailExcLaw_map_fst (θ : ℝ) (T : NNReal) : (tailExcLaw θ T).map Prod.fst = tailLevyExcLaw θ T

First marginal of tailExcLaw: exactly the sealed tailLevyExcLaw θ T (every θ, every horizon).

theorem BGW.StableTrees.tailExcLaw_map_restrictPair (θ : ℝ) {a T : NNReal} (h : a ≤ T) : (tailExcLaw θ T).map (restrictPair h) = tailExcLaw θ a

Projectivity of the tail pair laws in the horizon.

Common graph

theorem BGW.StableTrees.map_restrictPair_excLaw {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (a : NNReal) (ha : a ∈ Set.Ioo 0 1) : ↑((excLaw θ).map (restrictPair ⋯)) = MeasureTheory.Measure.map (fun (x : Skorokhod.D ↑a ℝ) => (x, heightPrefixAE θ a x)) (unitPrefix θ a)

Joint unit prefix on [0,a], 0 < a < 1: the graph image of the unit path prefix under the H04 a.e.-time prefix map.

theorem BGW.StableTrees.tailExcLaw_eq_map_heightPrefixAE {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (a : NNReal) (ha : a ≤ 1) : ↑(tailExcLaw θ a) = MeasureTheory.Measure.map (fun (x : Skorokhod.D ↑a ℝ) => (x, heightPrefixAE θ a x)) (tailPrefix θ a)

Joint tail prefix on [0,a], a ≤ 1: the graph image of the tail path prefix under the same H04 a.e.-time prefix map.

Common-lifetime mixture

theorem BGW.StableTrees.tailExcLaw_eq_mixture {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (T : NNReal) (hT : 0 < T) {B : Set (Skorokhod.D ↑T ℝ × C(↑(Set.Icc 0 ↑T), ℝ))} (hB : MeasurableSet B) : ↑(tailExcLaw θ T) B = ∫⁻ (u : ↑(Set.Ioi 0)), ↑(excLaw θ) (pairStretch θ T u ⁻¹' B) * {u : ↑(Set.Ioi 0) | 1 < ↑u}.indicator (fun (u : ↑(Set.Ioi 0)) => ENNReal.ofReal (1 / θ * ↑u ^ (-1 - 1 / θ))) u ∂volIoi

Joint tail mixture (C28), every horizon T > 0 (including T > 1): under N(· | ζ > 1) the pair is a unit pair stretched to an independent common lifetime u with density (1/θ) u^(-1-1/θ) on (1, ∞), path by u^(1/θ), height by u^(1-1/θ).

Joint Γ identity

theorem BGW.StableTrees.lintegral_gamma_identity {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (a : NNReal) (ha : a ∈ Set.Ioo 0 1) (F : Skorokhod.D ↑a ℝ × C(↑(Set.Icc 0 ↑a), ℝ) → ENNReal) (hF : Measurable F) : ∫⁻ (z : Skorokhod.D 1 ℝ × C(↑(Set.Icc 0 1), ℝ)), F (restrictPair ⋯ z) ∂↑(excLaw θ) = ∫⁻ (z : Skorokhod.D ↑1 ℝ × C(↑(Set.Icc 0 ↑1), ℝ)), F (restrictPair ⋯ z) * ENNReal.ofReal (gammaA θ (↑a) (evalEnd a (restrictPair ⋯ z).1)) ∂↑(tailExcLaw θ 1)

Joint Γ identity, nonnegative measurable tests of the pair prefix on [0,a], 0 < a < 1.

theorem BGW.StableTrees.gamma_identity {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (a : NNReal) (ha : a ∈ Set.Ioo 0 1) (F : Skorokhod.D ↑a ℝ × C(↑(Set.Icc 0 ↑a), ℝ) → ℝ) (hF : Measurable F) (hb : ∃ (C : ℝ), ∀ (z : Skorokhod.D ↑a ℝ × C(↑(Set.Icc 0 ↑a), ℝ)), |F z| ≤ C) : MeasureTheory.Integrable (fun (z : Skorokhod.D ↑1 ℝ × C(↑(Set.Icc 0 ↑1), ℝ)) => F (restrictPair ⋯ z)) ↑(excLaw θ) ∧ MeasureTheory.Integrable (fun (z : Skorokhod.D ↑1 ℝ × C(↑(Set.Icc 0 ↑1), ℝ)) => F (restrictPair ⋯ z) * gammaA θ (↑a) (evalEnd a (restrictPair ⋯ z).1)) ↑(tailExcLaw θ 1) ∧ ∫ (z : Skorokhod.D 1 ℝ × C(↑(Set.Icc 0 1), ℝ)), F (restrictPair ⋯ z) ∂↑(excLaw θ) = ∫ (z : Skorokhod.D ↑1 ℝ × C(↑(Set.Icc 0 ↑1), ℝ)), F (restrictPair ⋯ z) * gammaA θ (↑a) (evalEnd a (restrictPair ⋯ z).1) ∂↑(tailExcLaw θ 1)

Joint Γ identity (source-facing form), bounded measurable signed tests of the pair prefix on [0,a], 0 < a < 1, with both integrands integrable.

Endpoints and the Brownian case

theorem BGW.StableTrees.excLaw_height_endpoints_pos {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (z : Skorokhod.D 1 ℝ × C(↑(Set.Icc 0 1), ℝ)) ∂↑(excLaw θ), z.2 ⟨0, ⋯⟩ = 0 ∧ z.2 ⟨1, ⋯⟩ = 0 ∧ ∀ (t : ↑(Set.Icc 0 1)), 0 < ↑t → ↑t < 1 → 0 < z.2 t

Under excLaw θ the height vanishes at 0 and 1 and is positive on (0,1), all times at once.

theorem BGW.StableTrees.excLaw_height_eq_path_two : ∀ᵐ (z : Skorokhod.D 1 ℝ × C(↑(Set.Icc 0 1), ℝ)) ∂↑(excLaw 2), ∀ (t : ↑(Set.Icc 0 1)), z.2 t = z.1 t

Brownian specialization (θ = 2, Laplace exponent λ²): under excLaw 2 the height equals the path at every time, almost surely.