Documentation

BGW.StableTrees.StableBridgeUniformMinimumDiscrete

Uniform finite-grid minimum indices of the stable bridge #

Strict-prefix absolute continuity excludes equal values at distinct grid times. Cyclic increment exchangeability then makes the unique grid minimum index uniform.

Reference: J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapter VIII (Vervaat's transformation and the uniform law of the minimum time); L. Chaumont, Excursion normalisée, méandre et pont pour les processus de Lévy stables, Bull. Sci. Math. 121 (1997), 377–403.

source
theorem BGW.StableTrees.stableBridgeLaw_ae_eval_ne {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (s t : ↑(Set.Icc 0 1)) (hst : s < t) (ht1 : ↑t < 1) :
∀ᵐ (f : Skorokhod.D 1 ℝ) ∂↑(stableBridgeLaw θ), f t ≠ f s

The bridge has unequal values at two distinct deterministic strict-prefix times.

source
theorem BGW.StableTrees.strictMono_bridgeGridTime (M : ℕ) :
StrictMono fun (i : Fin (M + 1)) => gridTime M ↑i

Distinct times in the grid excluding time one are strictly ordered.

source
theorem BGW.StableTrees.stableBridgeLaw_ae_bridgeGridValues_injective {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (M : ℕ) :
∀ᵐ (f : Skorokhod.D 1 ℝ) ∂↑(stableBridgeLaw θ), Function.Injective (bridgeGridValues M f)

Grid values excluding the duplicate terminal endpoint are almost surely distinct.

source
noncomputable def BGW.StableTrees.bridgeGridMinIndex (M : ℕ) (f : Skorokhod.D 1 ℝ) :
Fin (M + 1)

The first minimum index on the finite bridge grid.

Equations
Instances For
    source
    theorem BGW.StableTrees.measurable_bridgeGridMinIndex (M : ℕ) :
    Measurable (bridgeGridMinIndex M)

    The finite-grid minimum index is measurable, including paths with ties.

    source
    theorem BGW.StableTrees.bridgeGridValues_centered_shift {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (M : ℕ) (k : Fin (M + 1)) :
    MeasureTheory.Measure.map (fun (f : Skorokhod.D 1 ℝ) (i : Fin (M + 1)) => bridgeGridValues M f (i + k) - bridgeGridValues M f k) ↑(stableBridgeLaw θ) = MeasureTheory.Measure.map (fun (f : Skorokhod.D 1 ℝ) (i : Fin (M + 1)) => bridgeGridValues M f i - bridgeGridValues M f 0) ↑(stableBridgeLaw θ)

    Centered cyclic relabeling preserves the law of the grid values.

    source
    theorem BGW.StableTrees.bridgeGridMinIndex_sub_invariant {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (M : ℕ) (k : Fin (M + 1)) :
    MeasureTheory.Measure.map (fun (f : Skorokhod.D 1 ℝ) => bridgeGridMinIndex M f - k) ↑(stableBridgeLaw θ) = MeasureTheory.Measure.map (bridgeGridMinIndex M) ↑(stableBridgeLaw θ)

    Translating the minimum index cyclically preserves its law.

    source
    theorem BGW.StableTrees.stableBridgeLaw_bridgeGridMinIndex_eq {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (M : ℕ) (k : Fin (M + 1)) :
    ↑(stableBridgeLaw θ) {f : Skorokhod.D 1 ℝ | bridgeGridMinIndex M f = k} = (↑(M + 1))⁻¹

    Every index has probability exactly the reciprocal of the grid size.