Uniqueness of generalized minima of stable Lévy paths

A generalized minimizer of a càdlàg path is a time at which the value or the left limit equals the infimum. Under a stable Lévy law it is almost surely unique: two distinct minimizers are separated by rational windows whose generalized minima differ by an atom-free increment independent of both (P. W. Millar, Zero-one laws and the minimum of a Markov process, Trans. Amer. Math. Soc. 226 (1977), 365–391; J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapter VI).

noncomputable def BGW.StableTrees.genVal {T : ℝ} (f : Skorokhod.D T ℝ) (s : ↑(Set.Icc 0 T)) : ℝ

Generalized value of f at s: the minimum of the left limit and the value.

Equations

• BGW.StableTrees.genVal f s = min (Function.leftLim (⇑f) s) (f s)

noncomputable def BGW.StableTrees.genMin {T : ℝ} (f : Skorokhod.D T ℝ) (J : Set ↑(Set.Icc 0 T)) : ℝ

Generalized minimum over a set of times.

Equations

• BGW.StableTrees.genMin f J = ⨅ (s : ↑J), BGW.StableTrees.genVal f ↑s

def BGW.StableTrees.window (T a b : ℝ) : Set ↑(Set.Icc 0 T)

The window [a,b] of times.

Equations

• BGW.StableTrees.window T a b = {s : ↑(Set.Icc 0 T) | a ≤ ↑s ∧ ↑s ≤ b}

def BGW.StableTrees.IsGenMinimizer {T : ℝ} (f : Skorokhod.D T ℝ) (g : ↑(Set.Icc 0 T)) : Prop

g is a generalized minimizer of f.

Equations

• BGW.StableTrees.IsGenMinimizer f g = (BGW.StableTrees.genVal f g = ⨅ (t : ↑(Set.Icc 0 T)), f t)

theorem BGW.StableTrees.exists_isGenMinimizer {T : ℝ} (hT : 0 ≤ T) (f : Skorokhod.D T ℝ) : ∃ (g : ↑(Set.Icc 0 T)), IsGenMinimizer f g

Existence of a generalized minimizer (wrapper of exists_min_leftLim).

theorem BGW.StableTrees.iInf_le_genVal {T : ℝ} (f : Skorokhod.D T ℝ) (s : ↑(Set.Icc 0 T)) : ⨅ (t : ↑(Set.Icc 0 T)), f t ≤ genVal f s

The generalized value is bounded below by the global infimum.

theorem BGW.StableTrees.genMin_eq_iInf_of_mem {T : ℝ} (f : Skorokhod.D T ℝ) {J : Set ↑(Set.Icc 0 T)} {g : ↑(Set.Icc 0 T)} (hg : IsGenMinimizer f g) (hgJ : g ∈ J) : genMin f J = ⨅ (t : ↑(Set.Icc 0 T)), f t

A generalized minimizer in a window gives the window the global minimum.

theorem BGW.StableTrees.exists_rat_separation {T : ℝ} {f : Skorokhod.D T ℝ} {g₁ g₂ : ↑(Set.Icc 0 T)} (h₁ : IsGenMinimizer f g₁) (h₂ : IsGenMinimizer f g₂) (hne : g₁ ≠ g₂) : ∃ (b : ℚ) (c : ℚ), 0 ≤ ↑b ∧ ↑b < ↑c ∧ ↑c ≤ T ∧ genMin f (window T 0 ↑b) = genMin f (window T (↑c) T)

Separation: two distinct generalized minimizers are separated by rationals b < c, and the windows [0,b], [c,T] have equal generalized minima.

theorem BGW.StableTrees.exists_rat_pair_of_not_existsUnique {T : ℝ} (hT : 0 ≤ T) {f : Skorokhod.D T ℝ} (h : ¬∃! g : ↑(Set.Icc 0 T), IsGenMinimizer f g) : ∃ (b : ℚ) (c : ℚ), 0 ≤ ↑b ∧ ↑b < ↑c ∧ ↑c ≤ T ∧ genMin f (window T 0 ↑b) = genMin f (window T (↑c) T)

If a path has a generalized minimizer but not a unique one, some rational pair separates.

theorem BGW.StableTrees.measurable_genMinOn {T : ℝ} (a b : ℝ) : Measurable fun (f : Skorokhod.D T ℝ) => genMin f (window T a b)

Measurability of window generalized minima (via rational infima / measurable_iInf_eval).

theorem BGW.StableTrees.genMin_window_eq_restrict {T a b : ℝ} (ha : 0 ≤ a) (hab : a ≤ b) (hbT : b ≤ T) (f : Skorokhod.D T ℝ) : genMin f (window T a b) = genMin (Skorokhod.restrict hbT f) (window b a b)

The window minimum on [a,b] only depends on the restriction to [0,b].

theorem BGW.StableTrees.genMin_window_eq_of_continuousAt {T c d : ℝ} (hc : 0 ≤ c) (hcd : c ≤ d) (hdT : d ≤ T) (f : Skorokhod.D T ℝ) (hcT : c ≤ T) (hf : ContinuousAt ⇑f ⟨c, ⋯⟩) : genMin f (window T c d) = f ⟨c, ⋯⟩ + genMin (Skorokhod.shiftIncrement hc hcT f) (window (T - c) 0 (d - c))

On {ContinuousAt f c} the window minimum on [c,d] is f c plus the window minimum of the shifted increment path on [0, d-c].

theorem BGW.StableTrees.IsStableLevyLaw.measure_increment_eq {θ T : ℝ} {P : MeasureTheory.ProbabilityMeasure (Skorokhod.D T ℝ)} (hθ : 1 < θ ∧ θ ≤ 2) (hP : IsStableLevyLaw θ T P) {s u : ℝ} (hs : 0 ≤ s) (hsu : s < u) (huT : u ≤ T) (x : ℝ) : ↑P {f : Skorokhod.D T ℝ | f ⟨u, ⋯⟩ - f ⟨s, ⋯⟩ = x} = 0

Increments of a stable Lévy law have no atoms.

theorem BGW.StableTrees.IsStableLevyLaw.indepFun_increment_restrict_shiftIncrement {θ T : ℝ} {P : MeasureTheory.ProbabilityMeasure (Skorokhod.D T ℝ)} (hP : IsStableLevyLaw θ T P) {b c : ℝ} (hb : 0 ≤ b) (hbc : b < c) (hcT : c ≤ T) : ProbabilityTheory.IndepFun (fun (f : Skorokhod.D T ℝ) => f ⟨c, ⋯⟩ - f ⟨b, ⋯⟩) (fun (f : Skorokhod.D T ℝ) => (Skorokhod.restrict ⋯ f, Skorokhod.shiftIncrement ⋯ hcT f)) ↑P

Three-way independence: for 0 ≤ b < c ≤ T, the increment f c - f b is independent of the pair (past restricted to [0,b], increment path after c), for the product σ-algebra.

theorem BGW.StableTrees.IsStableLevyLaw.measure_genMin_window_eq_zero {θ T : ℝ} {P : MeasureTheory.ProbabilityMeasure (Skorokhod.D T ℝ)} (hθ : 1 < θ ∧ θ ≤ 2) (hT : 0 < T) (hP : IsStableLevyLaw θ T P) {a b c d : ℝ} (ha : 0 ≤ a) (hab : a ≤ b) (hbc : b < c) (hcd : c ≤ d) (hdT : d ≤ T) : ↑P {f : Skorokhod.D T ℝ | genMin f (window T a b) = genMin f (window T c d)} = 0

Key lemma: for separated windows [a,b], [c,d] (0 ≤ a ≤ b < c ≤ d ≤ T), the generalized minima over them coincide with probability zero. Proof: write them as A and X_b + Z + M with Z = X_c - X_b atom-free and independent of (past through b, increment path after c) (IsStableLevyLaw.indepFun_restrict_shiftIncrement at b, c, the three-way independence lemma IsStableLevyLaw.indepFun_increment_restrict_shiftIncrement, and the two measurability adapters genMin_window_eq_restrict, genMin_window_eq_of_continuousAt; ae_continuousAt at c).

theorem BGW.StableTrees.IsStableLevyLaw.ae_existsUnique_generalizedMinimizer {θ 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), min (Function.leftLim (⇑f) g) (f g) = ⨅ (t : ↑(Set.Icc 0 T)), f t

Main theorem: almost surely there is exactly one generalized minimizer.

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

The same for the canonical stable process law.

theorem BGW.StableTrees.ae_existsUnique_generalizedMinimizer_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), IsGenMinimizer f g

Transfer to any measure absolutely continuous w.r.t. a stable Lévy law.

theorem BGW.StableTrees.IsStableLevyLaw.ae_existsUnique_windowMinimizer {θ T : ℝ} {P : MeasureTheory.ProbabilityMeasure (Skorokhod.D T ℝ)} (hθ : 1 < θ ∧ θ ≤ 2) (hT : 0 < T) (hP : IsStableLevyLaw θ T P) {b : ℝ} (hb : 0 < b) (hbT : b ≤ T) : ∀ᵐ (f : Skorokhod.D T ℝ) ∂↑P, ∃! g : ↑(Set.Icc 0 T), ↑g ≤ b ∧ genVal f g = genMin f (window T 0 b)

Window-relative uniqueness: a.s. there is a unique time g ≤ b whose generalized value is the generalized minimum over [0,b].

theorem BGW.StableTrees.ae_existsUnique_windowMinimizer_of_absolutelyContinuous {θ T : ℝ} {P : MeasureTheory.ProbabilityMeasure (Skorokhod.D T ℝ)} (hθ : 1 < θ ∧ θ ≤ 2) (hT : 0 < T) (hP : IsStableLevyLaw θ T P) {b : ℝ} (hb : 0 < b) (hbT : b ≤ T) {μ : MeasureTheory.Measure (Skorokhod.D T ℝ)} (hμ : μ.AbsolutelyContinuous ↑P) : ∀ᵐ (f : Skorokhod.D T ℝ) ∂μ, ∃! g : ↑(Set.Icc 0 T), ↑g ≤ b ∧ genVal f g = genMin f (window T 0 b)

Transfer of window-relative uniqueness to measures absolutely continuous with respect to a stable Lévy law.