Continuity and interior location of the stable minimum

Regularity after the countably many jump stopping times transfers from the local stable law to compact horizons. Reversal of increments then excludes generalized minimizers at jump times, and regularity at zero excludes the two endpoints. Together with uniqueness of generalized minimizers, this gives a unique continuously attained interior minimum (P. W. Millar, Zero-one laws and the minimum of a Markov process, Trans. Amer. Math. Soc. 226 (1977), 365–391).

theorem BGW.StableTrees.ae_regular_after_jumps_stableLocalLaw {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ (t : NNReal), 0 < t → ↑f t ≠ Function.leftLim (↑f) t → ∀ (ε : NNReal), 0 < ε → (∃ (s : NNReal), 0 < s ∧ s < ε ∧ ↑f (t + s) < ↑f t) ∧ ∃ (s : NNReal), 0 < s ∧ s < ε ∧ ↑f t < ↑f (t + s)

On DLoc: almost surely, immediately after every jump time t > 0 the path takes values strictly below and strictly above its post-jump value f t (strong Markov property at the jump stopping times and regularity of 0).

theorem BGW.StableTrees.IsStableLevyLaw.ae_regular_after_jumps {θ T : ℝ} {P : MeasureTheory.ProbabilityMeasure (Skorokhod.D T ℝ)} (hθ : 1 < θ ∧ θ ≤ 2) (hT : 0 < T) (hP : IsStableLevyLaw θ T P) : ∀ᵐ (f : Skorokhod.D T ℝ) ∂↑P, ∀ (t : ↑(Set.Icc 0 T)), ↑t < T → f t ≠ Function.leftLim (⇑f) t → ∀ (ε : ℝ), 0 < ε → (∃ (s : ↑(Set.Icc 0 T)), ↑t < ↑s ∧ ↑s < ↑t + ε ∧ f s < f t) ∧ ∃ (s : ↑(Set.Icc 0 T)), ↑t < ↑s ∧ ↑s < ↑t + ε ∧ f t < f s

Regularity after jumps on a compact horizon: for a stable Lévy law on [0,T], almost surely at every jump time t < T the path takes values both below and above f t in (t, t + ε), for every ε > 0.

theorem BGW.StableTrees.IsStableLevyLaw.ae_regular_at_zero {θ T : ℝ} {P : MeasureTheory.ProbabilityMeasure (Skorokhod.D T ℝ)} (hθ : 1 < θ ∧ θ ≤ 2) (hT : 0 < T) (hP : IsStableLevyLaw θ T P) : ∀ᵐ (f : Skorokhod.D T ℝ) ∂↑P, ∀ (ε : ℝ), 0 < ε → (∃ (s : ↑(Set.Icc 0 T)), 0 < ↑s ∧ ↑s < ε ∧ f s < f ⟨0, ⋯⟩) ∧ ∃ (s : ↑(Set.Icc 0 T)), 0 < ↑s ∧ ↑s < ε ∧ f ⟨0, ⋯⟩ < f s

Regularity on a compact horizon: almost surely, 0 is regular for both half-lines.

theorem BGW.StableTrees.continuousAt_of_eq_leftLim {T : ℝ} (f : Skorokhod.D T ℝ) {t : ↑(Set.Icc 0 T)} (h : f t = Function.leftLim (⇑f) t) : ContinuousAt (⇑f) t

Deterministic: a path is continuous at t as soon as f t = leftLim f t (right-continuity is automatic; at t = 0 the left limit is f 0).

theorem BGW.StableTrees.reverseIncrements_max_at_upward_jump {T : ℝ} (hT : 0 < T) (f : Skorokhod.D T ℝ) {t : ↑(Set.Icc 0 T)} (ht0 : 0 < ↑t) (htT : ↑t < T) (hup : Function.leftLim (⇑f) t < f t) (hg : IsGenMinimizer f t) : (∀ (s : ↑(Set.Icc 0 T)), (Skorokhod.reverseIncrements ⋯ f) s ≤ (Skorokhod.reverseIncrements ⋯ f) ⟨T - ↑t, ⋯⟩) ∧ Function.leftLim ⇑(Skorokhod.reverseIncrements ⋯ f) ⟨T - ↑t, ⋯⟩ < (Skorokhod.reverseIncrements ⋯ f) ⟨T - ↑t, ⋯⟩

Deterministic reversal step. If 0 < t < T is a generalized minimizer at which f jumps up (leftLim f t < f t), then the reversed path reverseIncrements f attains its global maximum at T - t and jumps up there: its left limit at T - t is f T - f t, strictly below the maximum value f T - leftLim f t.

theorem BGW.StableTrees.IsStableLevyLaw.ae_not_isGenMinimizer_of_jump {θ T : ℝ} {P : MeasureTheory.ProbabilityMeasure (Skorokhod.D T ℝ)} (hθ : 1 < θ ∧ θ ≤ 2) (hT : 0 < T) (hP : IsStableLevyLaw θ T P) : ∀ᵐ (f : Skorokhod.D T ℝ) ∂↑P, ∀ (t : ↑(Set.Icc 0 T)), f t ≠ Function.leftLim (⇑f) t → ¬IsGenMinimizer f t

Almost surely no generalized minimizer is a jump time (upward jumps via reversal of increments, downward jumps via regularity after jumps; the terminal time is not a jump time a.s.).

theorem BGW.StableTrees.IsStableLevyLaw.ae_continuousAt_of_isGenMinimizer {θ T : ℝ} {P : MeasureTheory.ProbabilityMeasure (Skorokhod.D T ℝ)} (hθ : 1 < θ ∧ θ ≤ 2) (hT : 0 < T) (hP : IsStableLevyLaw θ T P) : ∀ᵐ (f : Skorokhod.D T ℝ) ∂↑P, ∀ (g : ↑(Set.Icc 0 T)), IsGenMinimizer f g → ContinuousAt (⇑f) g

Consequence: every generalized minimizer is a continuity point.

theorem BGW.StableTrees.IsStableLevyLaw.ae_not_isGenMinimizer_zero {θ T : ℝ} {P : MeasureTheory.ProbabilityMeasure (Skorokhod.D T ℝ)} (hθ : 1 < θ ∧ θ ≤ 2) (hT : 0 < T) (hP : IsStableLevyLaw θ T P) : ∀ᵐ (f : Skorokhod.D T ℝ) ∂↑P, ¬IsGenMinimizer f ⟨0, ⋯⟩

The minimizer is not at 0: the path starts at 0 and takes negative values immediately.

theorem BGW.StableTrees.IsStableLevyLaw.ae_not_isGenMinimizer_top {θ T : ℝ} {P : MeasureTheory.ProbabilityMeasure (Skorokhod.D T ℝ)} (hθ : 1 < θ ∧ θ ≤ 2) (hT : 0 < T) (hP : IsStableLevyLaw θ T P) : ∀ᵐ (f : Skorokhod.D T ℝ) ∂↑P, ¬IsGenMinimizer f ⟨T, ⋯⟩

The minimizer is not at T: there is no jump at T (ae_continuousAt), and the reversed path (same law) is positive immediately after 0, whereas a minimum at T would force it to be ≤ 0.

theorem BGW.StableTrees.IsStableLevyLaw.ae_unique_continuous_minimum {θ T : ℝ} {P : MeasureTheory.ProbabilityMeasure (Skorokhod.D T ℝ)} (hθ : 1 < θ ∧ θ ≤ 2) (hT : 0 < T) (hP : IsStableLevyLaw θ T P) : ∀ᵐ (f : Skorokhod.D T ℝ) ∂↑P, ∃ (g : ↑(Set.Icc 0 T)), 0 < ↑g ∧ ↑g < T ∧ ContinuousAt (⇑f) g ∧ min (Function.leftLim (⇑f) g) (f g) = ⨅ (t : ↑(Set.Icc 0 T)), f t ∧ ∀ (s : ↑(Set.Icc 0 T)), min (Function.leftLim (⇑f) s) (f s) = ⨅ (t : ↑(Set.Icc 0 T)), f t → s = g

Unique continuous interior minimum. For fixed T > 0, the minimum, as a value or a left limit, has exactly one minimizing time, this time is interior, and the path is continuous there.

theorem BGW.StableTrees.stableProcessLaw_ae_unique_continuous_minimum {θ T : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (hT : 0 < T) : ∀ᵐ (f : Skorokhod.D T ℝ) ∂↑(stableProcessLaw θ T), ∃ (g : ↑(Set.Icc 0 T)), 0 < ↑g ∧ ↑g < T ∧ ContinuousAt (⇑f) g ∧ min (Function.leftLim (⇑f) g) (f g) = ⨅ (t : ↑(Set.Icc 0 T)), f t ∧ ∀ (s : ↑(Set.Icc 0 T)), min (Function.leftLim (⇑f) s) (f s) = ⨅ (t : ↑(Set.Icc 0 T)), f t → s = g

The same for the canonical stable process law.

theorem BGW.StableTrees.ae_unique_continuous_minimum_of_absolutelyContinuous {θ T : ℝ} {P : MeasureTheory.ProbabilityMeasure (Skorokhod.D T ℝ)} (hθ : 1 < θ ∧ θ ≤ 2) (hT : 0 < T) (hP : IsStableLevyLaw θ T P) {μ : MeasureTheory.Measure (Skorokhod.D T ℝ)} (hμ : μ.AbsolutelyContinuous ↑P) : ∀ᵐ (f : Skorokhod.D T ℝ) ∂μ, ∃ (g : ↑(Set.Icc 0 T)), 0 < ↑g ∧ ↑g < T ∧ ContinuousAt (⇑f) g ∧ min (Function.leftLim (⇑f) g) (f g) = ⨅ (t : ↑(Set.Icc 0 T)), f t ∧ ∀ (s : ↑(Set.Icc 0 T)), min (Function.leftLim (⇑f) s) (f s) = ⨅ (t : ↑(Set.Icc 0 T)), f t → s = g

Transfer to any measure absolutely continuous with respect to a stable Lévy law (for instance bridge prefixes).