Height approximations and reversal

The height approximation uses future interval infima. Reversal is extended constantly beyond its horizon, with the left-limit convention of reverseIncrements.

This module supplies the deterministic and measurability part of H02. The occupation-limit, ancestral, support, positive-erasure and restart theorems of the H02 contract remain open.

noncomputable def BGW.StableTrees.futureInf (f : Skorokhod.DLoc) (t s : NNReal) : ℝ

The interval infimum I^s_t = inf_{[s ∧ t, t]} X.

Equations

• BGW.StableTrees.futureInf f t s = ⨅ (u : ↑(Set.Icc (min s t) t)), ↑f ↑u

noncomputable def BGW.StableTrees.heightApprox (ε : ℝ) (f : Skorokhod.DLoc) (t : NNReal) : ℝ

Minimal-exploration occupation approximation ε⁻¹ Leb{s ≤ t | X_s < I^s_t + ε}.

Equations

• BGW.StableTrees.heightApprox ε f t = ε⁻¹ * (MeasureTheory.volume {s : ℝ | 0 ≤ s ∧ s ≤ ↑t ∧ ↑f s.toNNReal < BGW.StableTrees.futureInf f t s.toNNReal + ε}).toReal

noncomputable def BGW.StableTrees.reversedPath (t : NNReal) (f : Skorokhod.DLoc) : NNReal → ℝ

The time-reversed process at t: u ↦ X_t - X_{(t - u ∧ t)-} (constant after t).

Equations

• BGW.StableTrees.reversedPath t f u = ↑f t - Function.leftLim (↑f) (t - min u t)

theorem BGW.StableTrees.isCadlag_reversedPath (t : NNReal) (f : Skorokhod.DLoc) : IsCadlag (reversedPath t f)

The reversed path is càdlàg (so reversedAt is never junk).

noncomputable def BGW.StableTrees.reversedAt (t : NNReal) (f : Skorokhod.DLoc) : Skorokhod.DLoc

The reversed process at t as a DLoc element (junk DLoc.zero never occurs).

Equations

• BGW.StableTrees.reversedAt t f = if h : IsCadlag (BGW.StableTrees.reversedPath t f) then ⟨BGW.StableTrees.reversedPath t f, h⟩ else BGW.Skorokhod.DLoc.zero

theorem BGW.StableTrees.reversedAt_apply (t : NNReal) (f : Skorokhod.DLoc) (u : NNReal) : ↑(reversedAt t f) u = reversedPath t f u

The reversal fallback is excluded at every path and horizon.

theorem BGW.StableTrees.restrict_reversedAt (t : NNReal) (f : Skorokhod.DLoc) : Skorokhod.DLoc.restrict t (reversedAt t f) = Skorokhod.reverseIncrements ⋯ (Skorokhod.DLoc.restrict t f)

On [0,t] the reversed path is the sealed reverseIncrements of the restriction.

theorem BGW.StableTrees.measurable_reversedAt_uncurry : Measurable fun (p : NNReal × Skorokhod.DLoc) => reversedAt p.1 p.2

(t, f) ↦ reversedAt t f is jointly measurable.

theorem BGW.StableTrees.map_restrict_reversedAt_stableLocalLaw {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {t : NNReal} (ht : 0 < t) : MeasureTheory.Measure.map (fun (f : Skorokhod.DLoc) => Skorokhod.DLoc.restrict t (reversedAt t f)) ↑(stableLocalLaw θ) = MeasureTheory.Measure.map (Skorokhod.DLoc.restrict t) ↑(stableLocalLaw θ)

Law of the reversed prefix: for each t > 0, reversal at t preserves the law of the prefix [0,t] (sealed map_reverseIncrements_stableProcessLaw, transferred to DLoc).

noncomputable def BGW.StableTrees.height (θ : ℝ) (f : Skorokhod.DLoc) (t : NNReal) : ℝ

The height H_t = M_t(reversed process at t): the H01 supremum local time of the time-reversed process.

Equations

• BGW.StableTrees.height θ f t = BGW.StableTrees.supLocalTime θ (BGW.StableTrees.reversedAt t f) t

noncomputable def BGW.StableTrees.heightRaw (θ : ℝ) (f : Skorokhod.DLoc) (t : NNReal) : ENNReal

The raw (extended-real) height: liminf of the approximations along supEps θ.

Equations

• BGW.StableTrees.heightRaw θ f t = Filter.liminf (fun (k : ℕ) => ENNReal.ofReal (BGW.StableTrees.heightApprox (BGW.StableTrees.supEps θ k) f t)) Filter.atTop

theorem BGW.StableTrees.measurable_height_uncurry (θ : ℝ) : Measurable fun (p : NNReal × Skorokhod.DLoc) => height θ p.2 p.1

Joint measurability of the chosen version (t, f) ↦ H_t(f).

theorem BGW.StableTrees.measurable_height_section (θ : ℝ) (f : Skorokhod.DLoc) : Measurable fun (s : NNReal) => height θ f s

For every fixed path f, s ↦ H_s(f) is measurable (so exploration is not junk).

noncomputable def BGW.StableTrees.futureInfFun (f : Skorokhod.DLoc) (t : NNReal) (x : ℝ) : ℝ

x ↦ I^{x⁺}_t as a function on ℝ.

Equations

• BGW.StableTrees.futureInfFun f t x = BGW.StableTrees.futureInf f t x.toNNReal

noncomputable def BGW.StableTrees.explorationStieltjes (f : Skorokhod.DLoc) (t : NNReal) : StieltjesFunction ℝ

The Stieltjes function of x ↦ I^{x⁺}_t (junk zero only if the spec failed).

Equations

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

noncomputable def BGW.StableTrees.exploration (θ : ℝ) (f : Skorokhod.DLoc) (t : NNReal) : MeasureTheory.Measure NNReal

The minimal exploration measure ρ_t = ∫_{(0,t]} 1{H_s ∈ ·} d_s I^s_t, a measure on heights ((·).toNNReal of the real height; heights are a.s. nonnegative).

Equations

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

theorem BGW.StableTrees.measurable_exploration_heightMap (θ : ℝ) (f : Skorokhod.DLoc) : Measurable fun (s : ℝ) => (height θ f s.toNNReal).toNNReal

Guard against the Measure.map fallback: the height section is measurable on ℝ.

noncomputable def BGW.StableTrees.topHeight (ρ : MeasureTheory.Measure NNReal) : NNReal

Top of the support of a measure on heights (junk 0 for the zero measure).

Equations

• BGW.StableTrees.topHeight ρ = sSup {h : NNReal | ∀ (ε : ℝ), 0 < ε → 0 < ρ (Metric.ball h ε)}

noncomputable def BGW.StableTrees.eraseCut (m : ENNReal) (ρ : MeasureTheory.Measure NNReal) : NNReal

Cut level for removing the top m units of mass of ρ.

Equations

• BGW.StableTrees.eraseCut m ρ = sInf {h : NNReal | ρ (Set.Ioi h) ≤ m}

noncomputable def BGW.StableTrees.eraseMass (m : ENNReal) (ρ : MeasureTheory.Measure NNReal) : MeasureTheory.Measure NNReal

Remove the top m units of mass: for m = 0 nothing is removed; otherwise keep ρ strictly below the cut, and put the remaining part of the mass of ρ(Ici cut) as an atom at the cut. (For m > 0 and finite ρ the cut set is nonempty; without the m = 0 branch an unbounded support would give junk cut 0.)

Equations

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

noncomputable def BGW.StableTrees.concatAbove (ρ ν : MeasureTheory.Measure NNReal) : MeasureTheory.Measure NNReal

Append ν above the support of ρ: heights of ν are shifted by topHeight ρ. PRECONDITION: this represents the source concatenation only when ρ has BOUNDED support (topHeight is an sSup in ℝ≥0, junk 0 for unbounded support); characterization lemmas must carry that hypothesis.

Equations

• BGW.StableTrees.concatAbove ρ ν = ρ + MeasureTheory.Measure.map (fun (x : NNReal) => x + BGW.StableTrees.topHeight ρ) ν

theorem BGW.StableTrees.eraseMass_zero (ρ : MeasureTheory.Measure NNReal) : eraseMass 0 ρ = ρ

Erasing zero mass leaves every measure unchanged.

theorem BGW.StableTrees.measurable_height_prefix (θ : ℝ) (t : NNReal) : Measurable fun (f : Skorokhod.DLoc) => height θ f t

Raw-prefix measurability: H_t is measurable for the σ-algebra generated by DLoc.restrict t.

theorem BGW.StableTrees.futureInf_bddBelow (f : Skorokhod.DLoc) (t s : NNReal) : BddBelow (Set.range fun (u : ↑(Set.Icc (min s t) t)) => ↑f ↑u)

Interval infima of a local càdlàg path have a genuine finite lower bound.

theorem BGW.StableTrees.futureInf_le_eval (f : Skorokhod.DLoc) (t s u : NNReal) (hu : u ∈ Set.Icc (min s t) t) : futureInf f t s ≤ ↑f u

An interval infimum bounds each value in its interval.

theorem BGW.StableTrees.futureInf_self (f : Skorokhod.DLoc) (t : NNReal) : futureInf f t t = ↑f t

The infimum at its terminal time is the terminal value.

theorem BGW.StableTrees.monotone_futureInf (f : Skorokhod.DLoc) (t : NNReal) : Monotone (futureInf f t)

The future infimum is nondecreasing in its starting time.

theorem BGW.StableTrees.futureInf_eq_runningInf_shift (f : Skorokhod.DLoc) (t s : NNReal) : futureInf f t s = ↑f (min s t) + runningInfLoc (Skorokhod.DLoc.shift (min s t) f) (t - min s t)

A future interval infimum is the running infimum of the centered shifted interval.

theorem BGW.StableTrees.measurable_futureInf_uncurry : Measurable fun (p : (NNReal × NNReal) × Skorokhod.DLoc) => futureInf p.2 p.1.1 p.1.2

The future interval infimum is jointly measurable in its two times and path.

theorem BGW.StableTrees.measurable_heightApprox_uncurry : Measurable fun (p : ℝ × NNReal × Skorokhod.DLoc) => heightApprox p.1 p.2.2 p.2.1

Joint measurability of the approximation in (ε, t, f).

theorem BGW.StableTrees.measurable_heightRaw (θ : ℝ) (t : NNReal) : Measurable fun (f : Skorokhod.DLoc) => heightRaw θ f t

heightRaw is measurable in f for each t.

theorem BGW.StableTrees.explorationStieltjes_spec (f : Skorokhod.DLoc) (t : NNReal) : Monotone (futureInfFun f t) ∧ ∀ (x : ℝ), ContinuousWithinAt (futureInfFun f t) (Set.Ici x) x

For every path, x ↦ I^x_t is monotone and right-continuous.

theorem BGW.StableTrees.exploration_univ (θ : ℝ) (f : Skorokhod.DLoc) (t : NNReal) : (exploration θ f t) Set.univ = ENNReal.ofReal (↑f t - futureInf f t 0)

Total mass ρ_t(ℝ≥0) = X_t - I_t for every path (the atom at s = t is kept).

theorem BGW.StableTrees.supRunning_reversedAt_window (f : Skorokhod.DLoc) {t s : NNReal} (hst : s ≤ t) (hf : ∀ (r : NNReal), Function.leftLim (↑f) r ≤ ↑f r) (hs : Function.leftLim (↑f) s = ↑f s) : supRunning (reversedAt t f) (t - s) = ↑f t - futureInf f t s

Reversal turns a terminal window infimum into a prefix supremum at a continuity time.

theorem BGW.StableTrees.supReflected_reversedAt_window (f : Skorokhod.DLoc) {t s : NNReal} (hst : s ≤ t) (hf : ∀ (r : NNReal), Function.leftLim (↑f) r ≤ ↑f r) (hs : Function.leftLim (↑f) s = ↑f s) : supReflected (reversedAt t f) (t - s) = ↑f s - futureInf f t s

Reflection of the reversal equals the future-infimum gap at continuity times.