Excursion support of the reflected stable process

The positive set is exactly the union of the passage-jump intervals, simultaneously on one full-probability event. Their starts are continuous, their endpoints identify every excursion candidate, and their complement has zero Lebesgue measure (J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapter VII).

theorem BGW.StableTrees.ae_jump_window_inf {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ x ∈ passageJumpSet f, 0 < passageTimeMinus x f ∧ Function.leftLim (↑f) (passageTimeMinus x f) = -↑x ∧ ∀ (r q : ℚ≥0), ↑r < passageTimeMinus x f → passageTimeMinus x f < ↑q → ↑q < passageTime x f → ⨅ (u : ↑(Set.Icc ↑r ↑q)), ↑f ↑u = -↑x

Window minima from plateau inequalities (no uniqueness needed). Simultaneously for every jump level x: X has left limit -x at T_{x-}, T_{x-} > 0, and over every rational window r < T_{x-} < q < T_x the infimum of X is -x.

theorem BGW.StableTrees.ae_jump_intervals_disjoint {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ x ∈ passageJumpSet f, ∀ y ∈ passageJumpSet f, x < y → passageTime x f < passageTimeMinus y f

Distinct jump levels give disjoint intervals and distinct starts.

theorem BGW.StableTrees.ae_passageJumpSet_countable {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), (passageJumpSet f).Countable

Jump levels are countable (monotone càdlàg T).

theorem BGW.StableTrees.ae_continuousAt_jumpStart {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ x ∈ passageJumpSet f, ContinuousAt (↑f) (passageTimeMinus x f) ∧ ↑f (passageTimeMinus x f) = -↑x ∧ ↑(reflectedFrom 0 f) (passageTimeMinus x f) = 0

No jump start: a.s., at every jump level the path is continuous at T_{x-}, takes the value -x there, and R (T_{x-}) = 0.

theorem BGW.StableTrees.ae_isExcursionCandidate_of_jump {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ x ∈ passageJumpSet f, 0 < passageTimeMinus x f ∧ localTime f (passageTimeMinus x f) = ↑x ∧ localTime f (passageTime x f) = ↑x ∧ IsExcursionCandidate f (passageTimeMinus x f) (passageTime x f)

Simultaneous excursion-candidate supplier. A.s., for every positive jump label x simultaneously, g = T_{x-} > 0, d = T_x, L_g = L_d = x and (g,d) is an IsExcursionCandidate; strict interior positivity of R comes from uniqueness of the minimum on rational windows.

theorem BGW.StableTrees.ae_isExcursionInterval_of_jump {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ x ∈ passageJumpSet f, IsExcursionInterval f (passageTimeMinus x f) (passageTime x f)

Excursion intervals from jump levels. The previous statement with the stronger IsExcursionInterval (continuous start, R(T_{x-}) = 0, via minimum continuity on rational windows).

theorem BGW.StableTrees.ae_isExcursionInterval_of_isExcursionCandidate {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ (g d : NNReal), IsExcursionCandidate f g d → IsExcursionInterval f g d

No jump starts, a.s.: every excursion candidate is an excursion interval (R g = 0).

theorem BGW.StableTrees.ae_exists_jump_of_isExcursionCandidate {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ (g d : NNReal), IsExcursionCandidate f g d → ∃ x ∈ passageJumpSet f, g = passageTimeMinus x f ∧ d = passageTime x f ∧ ↑x = localTime f g

Converse for candidates. A.s., every excursion candidate (g,d) of the reflected path is (T_{x-}, T_x) for the unique level x = L_g > 0, which is a jump level; in particular 0 < g (no candidate starts at 0).

theorem BGW.StableTrees.ae_isExcursionInterval_iff {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ (g d : NNReal), IsExcursionInterval f g d ↔ ∃ x ∈ passageJumpSet f, g = passageTimeMinus x f ∧ d = passageTime x f

Characterization of excursion intervals (iff).

theorem BGW.StableTrees.ae_isExcursionCandidate_iff {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ (g d : NNReal), IsExcursionCandidate f g d ↔ ∃ x ∈ passageJumpSet f, g = passageTimeMinus x f ∧ d = passageTime x f

Characterization of excursion candidates (iff).

theorem BGW.StableTrees.ae_pos_set_eq_iUnion_jump_intervals {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), {t : NNReal | 0 < ↑(reflectedFrom 0 f) t} = ⋃ x ∈ passageJumpSet f, Set.Ioo (passageTimeMinus x f) (passageTime x f)

The reflected process is positive exactly on the union of the excursion intervals (a.s., an equality of sets, not merely up to a null set): {R > 0} = ⋃_{x ∈ jump levels} (T_{x-}, T_x); equivalently R vanishes off the union, and the zero set is the Lebesgue-null complement of ae_zeroSet_volume_zero.

theorem BGW.StableTrees.ae_volume_compl_iUnion_jump_intervals {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), MeasureTheory.volume (NNReal.toReal '' (⋃ x ∈ passageJumpSet f, Set.Ioo (passageTimeMinus x f) (passageTime x f))ᶜ) = 0

Lebesgue-almost every time lies in an excursion interval (consequence of the two previous statements).