Killed stable paths and excursion futures

The killed stable kernel uses strict downward passage of the driving process. The excursion future is uncentred, and its lifetime is read by the last positive time.

Reference: J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapter IV.

Definitions

noncomputable def BGW.StableTrees.Excursion.valueNN (e : Excursion) (t : NNReal) : NNReal

The value of an excursion at time t, as a nonnegative real ((e t).toNNReal; the path is nonnegative so nothing is lost).

Equations

• e.valueNN t = (↑e.path t).toNNReal

noncomputable def BGW.StableTrees.stopLocAt : WithTop NNReal → Skorokhod.DLoc → Skorokhod.DLoc

Stop a path at an extended time: ⊤ leaves it unchanged, ↑a is stopLoc a.

Equations

• BGW.StableTrees.stopLocAt none x✝ = x✝
• BGW.StableTrees.stopLocAt (some a) x✝ = BGW.StableTrees.stopLoc a x✝

noncomputable def BGW.StableTrees.killedPath (y : NNReal) (f : Skorokhod.DLoc) : Skorokhod.DLoc

The killed path started at y: s ↦ y + X_{s ∧ T_y} with T_y = firstPassageBelow y (uncentred, frozen after the first passage below -y, where it equals 0 a.s.).

Equations

• BGW.StableTrees.killedPath y f = ⟨fun (s : NNReal) => ↑y + ↑(BGW.StableTrees.stopLocAt (BGW.StableTrees.firstPassageBelow y f) f) s, ⋯⟩

noncomputable def BGW.StableTrees.futureFrom (t : NNReal) (e : Excursion) : Skorokhod.DLoc

Uncentred future of an excursion after age t: s ↦ e(t + s).

Equations

• BGW.StableTrees.futureFrom t e = ⟨fun (s : NNReal) => ↑e.path t + ↑(BGW.Skorokhod.DLoc.shift t e.path) s, ⋯⟩

noncomputable def BGW.StableTrees.killedStableKernel (θ : ℝ) : ProbabilityTheory.Kernel NNReal Skorokhod.DLoc

The killed stable kernel y ↦ Law_P(killedPath y), a kernel ℝ≥0 → DLoc, with the zero path absorbing (killedStableKernel_zero).

Equations

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

noncomputable def BGW.StableTrees.lastPositiveTime (g : Skorokhod.DLoc) : WithTop NNReal

Last positive time of a path: sup {t | g t > 0} (⊥ = 0 if none). Measurable (measurable_lastPositiveTime), unlike weak first hitting of a closed set.

Equations

• BGW.StableTrees.lastPositiveTime g = ⨆ (t : { t : NNReal // 0 < ↑g t }), ↑↑t

theorem BGW.StableTrees.measurable_lastPositiveTime : Measurable lastPositiveTime

lastPositiveTime is measurable: {L > s} = ⋃_{q ∈ ℚ, q > s} {g q > 0} by right-continuity of g.

theorem BGW.StableTrees.futureFrom_apply (t : NNReal) (e : Excursion) (s : NNReal) : ↑(futureFrom t e) s = ↑e.path (t + s)

Evaluation of the future: (futureFrom t e)(s) = e(t + s).

theorem BGW.StableTrees.measurable_futureFrom (t : NNReal) : Measurable (futureFrom t)

futureFrom t is measurable.

theorem BGW.StableTrees.killedPath_apply_of_lt_top {y : NNReal} {f : Skorokhod.DLoc} {τ : NNReal} (h : firstPassageBelow y f = ↑τ) (s : NNReal) : ↑(killedPath y f) s = ↑y + ↑f (min s τ)

Evaluation of the killed path when the passage time is finite.

theorem BGW.StableTrees.killedPath_apply_of_eq_top {y : NNReal} {f : Skorokhod.DLoc} (h : firstPassageBelow y f = ⊤) (s : NNReal) : ↑(killedPath y f) s = ↑y + ↑f s

Evaluation of the killed path when there is no passage.

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

Joint measurability of (y, f) ↦ killedPath y f (from measurable_firstPassageBelow_uncurry and DLoc.measurable_eval₂).

theorem BGW.StableTrees.killedStableKernel_apply (θ : ℝ) (y : NNReal) : (killedStableKernel θ) y = MeasureTheory.Measure.map (killedPath y) ↑(stableLocalLaw θ)

The kernel is the law of the killed path: K_y = P.map (killedPath y).

theorem BGW.StableTrees.isMarkovKernel_killedStableKernel (θ : ℝ) : ProbabilityTheory.IsMarkovKernel (killedStableKernel θ)

The killed kernel is a Markov kernel (probability measures).

theorem BGW.StableTrees.ae_killedPath_spec {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (y : NNReal) (hy : 0 < y) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ↑(killedPath y f) 0 = ↑y ∧ (∀ (s : NNReal), 0 ≤ ↑(killedPath y f) s) ∧ (∀ (s : NNReal), ↑s < firstPassageBelow y f → 0 < ↑(killedPath y f) s) ∧ ∀ (s : NNReal), firstPassageBelow y f ≤ ↑s → ↑(killedPath y f) s = 0

Killed paths are nonnegative and absorbed at zero: for each fixed positive starting level y, a.s. under P the killed path starts at y, is ≥ 0, positive before T_y and is 0 from the passage time on. (y is fixed BEFORE ∀ᵐ: simultaneous strict positivity over all levels is false, at passage-jump levels X_{T_{y-}} = -y.)

theorem BGW.StableTrees.ae_killedPath_spec_simultaneous {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ (y : NNReal), 0 < y → ↑(killedPath y f) 0 = ↑y ∧ (∀ (s : NNReal), 0 ≤ ↑(killedPath y f) s) ∧ ∀ (s : NNReal), firstPassageBelow y f ≤ ↑s → ↑(killedPath y f) s = 0

Simultaneous version (start, nonnegativity, zero after strict passage; NO strict pre-passage positivity, which fails simultaneously over levels).

theorem BGW.StableTrees.ae_firstPassageBelow_zero {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), firstPassageBelow 0 f = 0

T_0 = 0 a.s.: sealed supplier is ae_passageTime_eq_firstPassageBelow (second clause passageTime 0 f = 0, with firstPassageBelow 0 f its finite reading), itself from ae_strictPassage_zero_stableLocalLaw (regularity, StableRegularity.lean).

theorem BGW.StableTrees.killedStableKernel_zero {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : (killedStableKernel θ) 0 = MeasureTheory.Measure.dirac zeroLoc

Zero is absorbing: K_0 = δ_{zeroLoc} as measures (T_0 = 0 a.s. by regularity of (-∞,0) at 0).

Supporting exports

theorem BGW.StableTrees.measurable_excursion_valueNN (t : NNReal) : Measurable fun (e : Excursion) => e.valueNN t

valueNN is measurable.

theorem BGW.StableTrees.measurable_excursion_valueNN_uncurry : Measurable fun (p : Excursion × NNReal) => p.1.valueNN p.2

valueNN is jointly measurable in (e, t).

theorem BGW.StableTrees.Excursion.coe_valueNN (e : Excursion) (t : NNReal) : ↑(e.valueNN t) = ↑e.path t

Real-value bridge: the carrier requires nonnegativity, so nothing is truncated.

theorem BGW.StableTrees.ae_valueNN_pos {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (t : NNReal) (ht : 0 < t) : ∀ᵐ (e : Excursion) ∂(excursionMeasure θ).restrict {e : Excursion | t < e.lifetime}, 0 < e.valueNN t

Strict positivity of the value before death: for 0 < t, N-a.e. excursion alive at age t has e(t) > 0 (ae_excursionMeasure_support).

theorem BGW.StableTrees.isFiniteMeasure_excursionMeasure_survival {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (t : NNReal) (ht : 0 < t) : MeasureTheory.IsFiniteMeasure ((excursionMeasure θ).restrict {e : Excursion | t < e.lifetime})

The survival restriction of N is finite (excursionMeasure_lifetime_slab_lt_top); σ-finiteness is sigmaFinite_excursionMeasure.

theorem BGW.StableTrees.ae_lastPositiveTime_futureFrom {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (t : NNReal) (ht : 0 < t) : ∀ᵐ (e : Excursion) ∂(excursionMeasure θ).restrict {e : Excursion | t < e.lifetime}, lastPositiveTime (futureFrom t e) = ↑(e.lifetime - t)

Remaining lifetime as a functional of the future: for 0 < t, on {t < ζ} N-a.e., lastPositiveTime (futureFrom t e) = ζ - t.

theorem BGW.StableTrees.ae_lastPositiveTime_killedPath {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (y : NNReal) (hy : 0 < y) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), lastPositiveTime (killedPath y f) = firstPassageBelow y f

For each fixed y > 0, a.s. the last positive time of the killed path is the strict passage time T_y (strict passage of the driving process, not of the killed path).

theorem BGW.StableTrees.measurable_stopLocAt_stopped {τ : Skorokhod.DLoc → WithTop NNReal} (hτ : MeasureTheory.IsStoppingTime Skorokhod.DLoc.filtration τ) : Measurable fun (f : Skorokhod.DLoc) => stopLocAt (τ f) f

The whole stopped path is measurable for the stopped sigma-algebra, everywhere, including paths on which the stopping time is infinite.

noncomputable def BGW.StableTrees.selectedAgePrefix (t : NNReal) (τ : Skorokhod.DLoc → WithTop NNReal) (f : Skorokhod.DLoc) : Skorokhod.D ↑t ℝ

The age-t prefix selected by a clock τ, computed from the path stopped at τ. It is defined on all paths and agrees with the excursion prefix excursionRestrict t on the cut (selectedAgePrefix_eq_excursionRestrict).

Equations

• BGW.StableTrees.selectedAgePrefix t τ f = BGW.Skorokhod.DLoc.restrict t (BGW.Skorokhod.DLoc.shift (WithTop.untopD 0 (τ f) - t) (BGW.StableTrees.stopLocAt (τ f) f))

theorem BGW.StableTrees.measurable_selectedAgePrefix (t : NNReal) {τ : Skorokhod.DLoc → WithTop NNReal} (hτ : MeasureTheory.IsStoppingTime Skorokhod.DLoc.filtration τ) : Measurable (selectedAgePrefix t τ)

The selected prefix is measurable in the stopped sigma-algebra.

theorem BGW.StableTrees.selectedAgePrefix_eq_excursionRestrict {t g d : NNReal} {τ : Skorokhod.DLoc → WithTop NNReal} {f : Skorokhod.DLoc} (hτ : τ f = ↑(g + t)) (hv : cutValid g d f) (htd : g + t < d) : selectedAgePrefix t τ f = excursionRestrict t (excursionCut g d f)

At an age crossing inside a valid excursion cut, the selected stopped-path prefix is exactly the excursion prefix.

theorem BGW.StableTrees.lintegral_past_shiftAt {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {α : Type u_1} [MeasurableSpace α] {τ : Skorokhod.DLoc → WithTop NNReal} (hτ : MeasureTheory.IsStoppingTime Skorokhod.DLoc.filtration τ) {A : Set Skorokhod.DLoc} (hA : MeasurableSet A) (hAτ : A ⊆ {f : Skorokhod.DLoc | τ f < ⊤}) {Z : Skorokhod.DLoc → α} (hZ : Measurable Z) {H : α × Skorokhod.DLoc → ENNReal} (hH : Measurable H) : ∫⁻ (f : Skorokhod.DLoc) in A, H (Z f, Skorokhod.DLoc.shiftAt τ f) ∂↑(stableLocalLaw θ) = ∫⁻ (f : Skorokhod.DLoc) in A, ∫⁻ (g : Skorokhod.DLoc), H (Z f, g) ∂↑(stableLocalLaw θ) ∂↑(stableLocalLaw θ)

Nonnegative state-dependent strong Markov integration, with the entire stopped past allowed as the state variable.

theorem BGW.StableTrees.futureFrom_excursionCut_eq_killedPath {t g d x : NNReal} {f : Skorokhod.DLoc} (hv : cutValid g d f) (hT : firstPassageBelow x f = ↑d) (hg : ↑f g = -↑x) (htd : g + t < d) : futureFrom t (excursionCut g d f) = killedPath ((excursionCut g d f).valueNN t) (Skorokhod.DLoc.shift (g + t) f)

The uncentred future of a valid excursion cut is the killed shifted driving path, when the right endpoint is the strict passage below its starting infimum.