The tagged excursion carrier

This module defines càdlàg excursions together with a positive lifetime tag. It proves that the carrier is standard Borel, constructs excursion cuts, and establishes space-time scaling and normalization with their measurability and group laws (J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapter IV; L. Chaumont, Excursion normalisée, méandre et pont pour les processus de Lévy stables, Bull. Sci. Math. 121 (1997), 377–403).

theorem BGW.StableTrees.isCadlag_stopLoc (a : NNReal) (f : Skorokhod.DLoc) : IsCadlag fun (t : NNReal) => ↑f (min t a)

Stopping a càdlàg path at a deterministic time is càdlàg.

noncomputable def BGW.StableTrees.stopLoc (a : NNReal) (f : Skorokhod.DLoc) : Skorokhod.DLoc

Stopping a local path at a deterministic time: t ↦ f (min t a).

Equations

• BGW.StableTrees.stopLoc a f = ⟨fun (t : NNReal) => ↑f (min t a), ⋯⟩

noncomputable def BGW.StableTrees.zeroLoc : Skorokhod.DLoc

The constant zero local path.

Equations

• BGW.StableTrees.zeroLoc = ⟨fun (x : NNReal) => 0, BGW.StableTrees.zeroLoc._proof_1⟩

noncomputable def BGW.StableTrees.cutPath (g d : NNReal) (f : Skorokhod.DLoc) : Skorokhod.DLoc

The path of the cut of f between times g and d: t ↦ f (min (g+t) d) - f g (for g ≤ d).

Equations

• BGW.StableTrees.cutPath g d f = BGW.StableTrees.stopLoc (d - g) (BGW.Skorokhod.DLoc.shift g f)

def BGW.StableTrees.IsExcursionTag (p : Skorokhod.DLoc × ↑(Set.Ioi 0)) : Prop

The valid-excursion conditions on a (path, tag) pair: starts at 0, nonnegative, identically zero at and after the tag.

Equations

• BGW.StableTrees.IsExcursionTag p = (↑p.1 0 = 0 ∧ (∀ (t : NNReal), 0 ≤ ↑p.1 t) ∧ ∀ (t : NNReal), ↑p.2 ≤ t → ↑p.1 t = 0)

def BGW.StableTrees.Excursion : Type

The tagged excursion carrier (Borel subtype of DLoc × Ioi 0).

Equations

• BGW.StableTrees.Excursion = { p : BGW.Skorokhod.DLoc × ↑(Set.Ioi 0) // BGW.StableTrees.IsExcursionTag p }

@[instance_reducible]

noncomputable instance BGW.StableTrees.instMeasurableSpaceExcursion : MeasurableSpace Excursion

Equations

• BGW.StableTrees.instMeasurableSpaceExcursion = inferInstance

def BGW.StableTrees.Excursion.path (e : Excursion) : Skorokhod.DLoc

The path coordinate.

Equations

• e.path = (↑e).1

def BGW.StableTrees.Excursion.lifetime (e : Excursion) : NNReal

The tagged lifetime.

Equations

• e.lifetime = ↑(↑e).2

def BGW.StableTrees.Excursion.lifetimePos (e : Excursion) : ↑(Set.Ioi 0)

The tagged lifetime as a positive real.

Equations

• e.lifetimePos = ⟨↑e.lifetime, ⋯⟩

theorem BGW.StableTrees.Excursion.lifetime_pos (e : Excursion) : 0 < e.lifetime

The lifetime tag of an excursion is positive.

def BGW.StableTrees.cutValid (g d : NNReal) (f : Skorokhod.DLoc) : Prop

Cut-validity: between times g < d, f d = f g and f ≥ f g on [g, d].

A valid cut uses the post-jump value f g as the base level (the cut path is f(g + ·) - f g), so excursionCut never represents an excursion that starts with a jump out of the infimum; this is consistent with IsExcursionInterval (in BGW.StableTrees.ReflectedRestart), which requires R g = 0.

Equations

• BGW.StableTrees.cutValid g d f = (g < d ∧ ↑f d = ↑f g ∧ ∀ (t : NNReal), g ≤ t → t ≤ d → ↑f g ≤ ↑f t)

theorem BGW.StableTrees.isExcursionTag_cutPath {g d : NNReal} {f : Skorokhod.DLoc} (h : cutValid g d f) : IsExcursionTag (cutPath g d f, ⟨d - g, ⋯⟩)

The cut of a valid window, with tag d - g, satisfies the excursion-tag conditions.

theorem BGW.StableTrees.measurableSet_isExcursionTag : MeasurableSet {p : Skorokhod.DLoc × ↑(Set.Ioi 0) | IsExcursionTag p}

Measurability of the validity predicate: a Borel subset of DLoc × Ioi 0.

theorem BGW.StableTrees.measurableSet_compatibleFamilies : MeasurableSet {p : (n : ℕ) → Skorokhod.D (↑n + 1) ℝ | ∀ (n : ℕ), Skorokhod.restrict ⋯ (p (n + 1)) = p n}

Compatible families form a Borel set: the integer-horizon compatible families are a measurable subset of the countable product of the spaces D (n+1) ℝ.

instance BGW.StableTrees.instStandardBorelSpaceDLoc : StandardBorelSpace Skorokhod.DLoc

DLoc is standard Borel (measurably equivalent to the Borel set of compatible families in a countable product of standard Borel spaces D (n+1) ℝ).

instance BGW.StableTrees.instStandardBorelSpaceExcursion : StandardBorelSpace Excursion

Standard Borel. The carrier is a standard Borel space (through DLoc.measurableEquivCompatible and the Borel compatible-family subset of the countable product of Polish D (n+1) ℝ; no closedness or J1-completeness is assumed).

noncomputable def BGW.StableTrees.junkExcursion : Excursion

The junk excursion: zero path with tag one.

Equations

• BGW.StableTrees.junkExcursion = ⟨(BGW.StableTrees.zeroLoc, ⟨1, BGW.StableTrees.junkExcursion._proof_2⟩), BGW.StableTrees.junkExcursion._proof_1⟩

theorem BGW.StableTrees.measurable_excursion_path : Measurable Excursion.path

Measurability of the path coordinate.

theorem BGW.StableTrees.measurable_excursion_lifetime : Measurable Excursion.lifetime

Measurability of the tagged lifetime.

theorem BGW.StableTrees.measurable_lifetimePos : Measurable Excursion.lifetimePos

The positive-real lifetime coordinate is measurable.

theorem BGW.StableTrees.measurable_excursion_eval (t : NNReal) : Measurable fun (e : Excursion) => ↑e.path t

Measurability of each coordinate evaluation e ↦ e(t).

theorem BGW.StableTrees.measurable_excursion_eval₂ : Measurable fun (p : Excursion × NNReal) => ↑p.1.path p.2

Joint evaluation (e, t) ↦ e(t) is measurable.

theorem BGW.StableTrees.excursion_path_zero_at_lifetime (e : Excursion) : ↑e.path e.lifetime = 0

e ↦ e(ζ(e)) evaluates to 0 (the path is stopped at the tag), so evaluation at the tag is trivially measurable; kept as the sanity statement that the tag convention is "zero at the tag".

noncomputable def BGW.StableTrees.excursionCut (g d : NNReal) (f : Skorokhod.DLoc) : Excursion

Cutting a path at a window [g, d]: the excursion with path t ↦ f (min (g+t) d) - f g and tag d - g when the cut is valid, the junk excursion otherwise. A valid cut is based at the post-jump value f g, so an excursion starting with a jump out of the infimum is never represented (see cutValid).

Equations

• BGW.StableTrees.excursionCut g d f = if h : BGW.StableTrees.cutValid g d f then ⟨(BGW.StableTrees.cutPath g d f, ⟨d - g, ⋯⟩), ⋯⟩ else BGW.StableTrees.junkExcursion

theorem BGW.StableTrees.excursionCut_of_not_cutValid {g d : NNReal} {f : Skorokhod.DLoc} (h : ¬cutValid g d f) : excursionCut g d f = junkExcursion

Junk branch.

theorem BGW.StableTrees.excursionCut_eval {g d : NNReal} {f : Skorokhod.DLoc} (h : cutValid g d f) (t : NNReal) : ↑(excursionCut g d f).path t = ↑f (min (g + t) d) - ↑f g

Exact evaluation formula for cutting between two finite times with equal values.

theorem BGW.StableTrees.excursionCut_lifetime {g d : NNReal} {f : Skorokhod.DLoc} (h : cutValid g d f) : (excursionCut g d f).lifetime = d - g

The lifetime of a valid cut is the window length.

theorem BGW.StableTrees.measurableSet_cutValid : MeasurableSet {p : NNReal × NNReal × Skorokhod.DLoc | cutValid p.1 p.2.1 p.2.2}

The validity set is jointly measurable in (g, d, f).

theorem BGW.StableTrees.measurable_excursionCut : Measurable fun (p : NNReal × NNReal × Skorokhod.DLoc) => excursionCut p.1 p.2.1 p.2.2

Joint cut measurability: (g, d, f) ↦ excursionCut g d f is measurable jointly (not merely at fixed times).

theorem BGW.StableTrees.isCadlag_scaleLoc (θ : ℝ) (c : ↑(Set.Ioi 0)) (f : Skorokhod.DLoc) : IsCadlag fun (t : NNReal) => ↑c ^ (1 / θ) * ↑f (t / (↑c).toNNReal)

Space-time scaling of a càdlàg path is càdlàg.

noncomputable def BGW.StableTrees.scaleLoc (θ : ℝ) (c : ↑(Set.Ioi 0)) (f : Skorokhod.DLoc) : Skorokhod.DLoc

Scaling of the underlying path: t ↦ c^(1/θ) * f (t / c).

Equations

• BGW.StableTrees.scaleLoc θ c f = ⟨fun (t : NNReal) => ↑c ^ (1 / θ) * ↑f (t / (↑c).toNNReal), ⋯⟩

theorem BGW.StableTrees.isExcursionTag_scale (θ : ℝ) (c : ↑(Set.Ioi 0)) (e : Excursion) : IsExcursionTag (scaleLoc θ c e.path, ⟨(↑c).toNNReal * e.lifetime, ⋯⟩)

Scaling preserves the excursion-tag conditions (with tag c ζ).

noncomputable def BGW.StableTrees.excursionScale (θ : ℝ) (c : ↑(Set.Ioi 0)) (e : Excursion) : Excursion

Excursion scaling S_c: path c^(1/θ) e(t/c), tag c * ζ; the lifetime multiplies by c.

Equations

• BGW.StableTrees.excursionScale θ c e = ⟨(BGW.StableTrees.scaleLoc θ c e.path, ⟨(↑c).toNNReal * e.lifetime, ⋯⟩), ⋯⟩

theorem BGW.StableTrees.excursionScale_lifetime (θ : ℝ) (c : ↑(Set.Ioi 0)) (e : Excursion) : ↑(excursionScale θ c e).lifetime = ↑c * ↑e.lifetime

Scaling multiplies the lifetime by c.

theorem BGW.StableTrees.excursionScale_one (θ : ℝ) (e : Excursion) : excursionScale θ ⟨1, ⋯⟩ e = e

Scale group law (identity).

theorem BGW.StableTrees.excursionScale_mul (θ : ℝ) (c₁ c₂ : ↑(Set.Ioi 0)) (e : Excursion) : excursionScale θ c₁ (excursionScale θ c₂ e) = excursionScale θ ⟨↑c₁ * ↑c₂, ⋯⟩ e

Scale group law (composition).

theorem BGW.StableTrees.measurable_excursionScale (θ : ℝ) (c : ↑(Set.Ioi 0)) : Measurable (excursionScale θ c)

Scaling is measurable at each fixed c.

theorem BGW.StableTrees.measurable_excursionScale_joint (θ : ℝ) : Measurable fun (p : ↑(Set.Ioi 0) × Excursion) => excursionScale θ p.1 p.2

Scaling is jointly measurable in (c, e).

noncomputable def BGW.StableTrees.normalizeExc (θ : ℝ) (e : Excursion) : Excursion

Normalization: rescale to lifetime one, S_{1/ζ} e.

Equations

• BGW.StableTrees.normalizeExc θ e = BGW.StableTrees.excursionScale θ ⟨(↑e.lifetime)⁻¹, ⋯⟩ e

theorem BGW.StableTrees.normalizeExc_lifetime (θ : ℝ) (e : Excursion) : (normalizeExc θ e).lifetime = 1

A normalized excursion has lifetime one.

theorem BGW.StableTrees.measurable_normalizeExc (θ : ℝ) : Measurable (normalizeExc θ)

Measurable normalization (variable positive scaling c = 1/ζ(e); the raw functional need not be J1-continuous).

noncomputable def BGW.StableTrees.excursionRestrict (T : NNReal) (e : Excursion) : Skorokhod.D ↑T ℝ

Restriction of an excursion to the horizon [0, T], as a path in the sealed compact space.

Equations

• BGW.StableTrees.excursionRestrict T e = BGW.Skorokhod.DLoc.restrict T e.path

theorem BGW.StableTrees.measurable_excursionRestrict (T : NNReal) : Measurable (excursionRestrict T)

Restriction is measurable, for the Borel σ-algebra of D T ℝ.

noncomputable def BGW.StableTrees.shapeLifetime (θ : ℝ) (e : Excursion) : ↑(Set.Ioi 0) × Excursion

Lifetime/shape map: e ↦ (ζ(e), normalized e).

Equations

• BGW.StableTrees.shapeLifetime θ e = (e.lifetimePos, BGW.StableTrees.normalizeExc θ e)

noncomputable def BGW.StableTrees.fromShapeLifetime (θ : ℝ) (p : ↑(Set.Ioi 0) × Excursion) : Excursion

Inverse map (ζ, s) ↦ S_ζ s.

Equations

• BGW.StableTrees.fromShapeLifetime θ p = BGW.StableTrees.excursionScale θ p.1 p.2

theorem BGW.StableTrees.measurable_shapeLifetime (θ : ℝ) : Measurable (shapeLifetime θ)

The lifetime/shape decomposition is measurable.

theorem BGW.StableTrees.measurable_fromShapeLifetime (θ : ℝ) : Measurable (fromShapeLifetime θ)

Rebuilding an excursion from its lifetime and unit-lifetime shape is measurable.

theorem BGW.StableTrees.fromShapeLifetime_shapeLifetime (θ : ℝ) (e : Excursion) : fromShapeLifetime θ (shapeLifetime θ e) = e

fromShapeLifetime ∘ shapeLifetime = id on all excursions.

theorem BGW.StableTrees.shapeLifetime_fromShapeLifetime (θ : ℝ) (ζ : ↑(Set.Ioi 0)) (s : Excursion) (hs : s.lifetime = 1) : shapeLifetime θ (fromShapeLifetime θ (ζ, s)) = (ζ, s)

shapeLifetime ∘ fromShapeLifetime = id on (lifetime, unit-lifetime shape) pairs.