The minimum of the stable bridge and continuity of the Vervaat transform

Strict prefixes of the closed stable bridge are absolutely continuous with respect to the stable process. The unique continuous interior minimum theorem therefore applies to every dyadic prefix. A countable intersection of these events gives uniqueness, interiority and continuity of the global generalized minimum of the bridge. The deterministic Vervaat continuity theorem then applies, and strict positivity away from the endpoints follows from uniqueness of the minimizing time (L. Chaumont, Excursion normalisée, méandre et pont pour les processus de Lévy stables, Bull. Sci. Math. 121 (1997), 377–403; W. Vervaat, A relation between Brownian bridge and Brownian excursion, Ann. Probab. 7 (1979), 143–149).

Deterministic adapters between a path and its restriction to [0,a]

theorem BGW.StableTrees.leftLim_restrict_eq {T a : ℝ} (ha : 0 ≤ a) (haT : a ≤ T) (f : Skorokhod.D T ℝ) (t : ↑(Set.Icc 0 a)) : Function.leftLim (⇑(Skorokhod.restrict haT f)) t = Function.leftLim ⇑f ⟨↑t, ⋯⟩

Left limits in the restriction agree with those of the original path (also at t = a, since only a left neighbourhood is used; at t = 0 both are the value).

theorem BGW.StableTrees.continuousAt_of_continuousAt_restrict {T a : ℝ} (ha : 0 ≤ a) (haT : a ≤ T) (f : Skorokhod.D T ℝ) {t : ↑(Set.Icc 0 a)} (ht : ↑t < a) (h : ContinuousAt (⇑(Skorokhod.restrict haT f)) t) : ContinuousAt ⇑f ⟨↑t, ⋯⟩

Continuity of the restriction at an interior time t < a gives continuity of the original.

theorem BGW.StableTrees.iInf_restrict_eq_of_genMin {T a : ℝ} (ha : 0 ≤ a) (haT : a ≤ T) (f : Skorokhod.D T ℝ) {g : ↑(Set.Icc 0 T)} (hg : IsGenMinimizer f g) (hga : ↑g ≤ a) : ⨅ (t : ↑(Set.Icc 0 a)), (Skorokhod.restrict haT f) t = ⨅ (t : ↑(Set.Icc 0 T)), f t

If a generalized minimizer g of f lies in [0,a], the prefix infimum is the global one.

theorem BGW.StableTrees.not_isGenMinimizer_endpoints {f : Skorokhod.D 1 ℝ} (h0 : f ⟨0, ⋯⟩ = 0) (h1 : f ⟨1, ⋯⟩ = 0) (hl : Function.leftLim ⇑f ⟨1, ⋯⟩ = 0) (hneg : ⨅ (t : ↑(Set.Icc 0 1)), f t < 0) : ¬IsGenMinimizer f ⟨0, ⋯⟩ ∧ ¬IsGenMinimizer f ⟨1, ⋯⟩

Endpoints are not generalized minimizers of a bridge path with negative infimum.

Probabilistic transfers to bridge prefixes

theorem BGW.StableTrees.stableBridgeLaw_ae_iInf_neg {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.D 1 ℝ) ∂↑(stableBridgeLaw θ), ⨅ (t : ↑(Set.Icc 0 1)), f t < 0

The bridge takes a negative value: the infimum is < 0 (regularity of 0 through a prefix, plus f 0 = 0 a.s.).

theorem BGW.StableTrees.stableBridgeLaw_ae_prefix_unique_continuous_minimum {θ a : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (ha : 0 < a) (ha1 : a < 1) : ∀ᵐ (f : Skorokhod.D 1 ℝ) ∂↑(stableBridgeLaw θ), ∃ (g : ↑(Set.Icc 0 a)), 0 < ↑g ∧ ↑g < a ∧ ContinuousAt (⇑(Skorokhod.restrict ⋯ f)) g ∧ min (Function.leftLim (⇑(Skorokhod.restrict ⋯ f)) g) ((Skorokhod.restrict ⋯ f) g) = ⨅ (t : ↑(Set.Icc 0 a)), (Skorokhod.restrict ⋯ f) t ∧ ∀ (s : ↑(Set.Icc 0 a)), min (Function.leftLim (⇑(Skorokhod.restrict ⋯ f)) s) ((Skorokhod.restrict ⋯ f) s) = ⨅ (t : ↑(Set.Icc 0 a)), (Skorokhod.restrict ⋯ f) t → s = g

The unique continuous minimum theorem on each strict prefix [0,a], 0 < a < 1, transferred through the absolutely continuous prefix law.

The minimum of the bridge

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

Unique continuous interior minimum of the bridge. Under the closed stable bridge law, almost surely the infimum is negative and the generalized minimizer, vervaatTime f, is unique, interior, and a continuity point of f.

theorem BGW.StableTrees.stableBridgeLaw_ae_existsUnique_continuous_minimizer {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.D 1 ℝ) ∂↑(stableBridgeLaw θ), ⨅ (t : ↑(Set.Icc 0 1)), f t < 0 ∧ ∃ (g : ↑(Set.Icc 0 1)), 0 < ↑g ∧ ↑g < 1 ∧ ContinuousAt (⇑f) g ∧ IsGenMinimizer f g ∧ ∀ (s : ↑(Set.Icc 0 1)), IsGenMinimizer f s → s = g

The same in ∃-form with IsGenMinimizer.

Continuity of the Vervaat transform at the bridge

theorem BGW.StableTrees.stableBridgeLaw_ae_continuousAt_vervaatD {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.D 1 ℝ) ∂↑(stableBridgeLaw θ), ContinuousAt Skorokhod.vervaatD f

Vervaat continuity. Under the bridge law, the càdlàg Vervaat map is almost surely continuous at the path.

theorem BGW.StableTrees.stableBridgeLaw_ae_vervaat_endpoints {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.D 1 ℝ) ∂↑(stableBridgeLaw θ), (Skorokhod.vervaatD f) ⟨0, ⋯⟩ = 0 ∧ (Skorokhod.vervaatD f) ⟨1, ⋯⟩ = 0 ∧ ContinuousAt ⇑(Skorokhod.vervaatD f) ⟨1, ⋯⟩ ∧ ContinuousAt (⇑(Skorokhod.vervaatD f)) (Set.projIcc 0 1 ⋯ (1 - ↑(Skorokhod.vervaatTime f)))

Vervaat endpoints. Almost surely the Vervaat image starts and ends at 0, is continuous at 1, and is continuous at the wrap point 1 - vervaatTime f.

theorem BGW.StableTrees.stableBridgeLaw_ae_vervaatD_pos {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.D 1 ℝ) ∂↑(stableBridgeLaw θ), ∀ (t : ↑(Set.Icc 0 1)), 0 < ↑t → ↑t < 1 → 0 < (Skorokhod.vervaatD f) t

Strict positivity of the Vervaat image. Almost surely the Vervaat transform of the bridge path is strictly positive on (0, 1) (the excursion property).