Finite minimum indices and cyclic increments

The first minimum is a measurable finite-valued function. A cyclic increment vector recovers its potential up to an additive constant by summation.

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.

theorem BGW.StableTrees.finiteMin_nonempty (M : ℕ) (v : Fin (M + 1) → ℝ) : {i : Fin (M + 1) | ∀ (j : Fin (M + 1)), v i ≤ v j}.Nonempty

A nonempty finite real vector has a minimizing coordinate.

noncomputable def BGW.StableTrees.finiteMinIndex (M : ℕ) (v : Fin (M + 1) → ℝ) : Fin (M + 1)

The first minimizing index of a nonempty finite real vector.

Equations

• BGW.StableTrees.finiteMinIndex M v = {i : Fin (M + 1) | ∀ (j : Fin (M + 1)), v i ≤ v j}.min' ⋯

theorem BGW.StableTrees.finiteMinIndex_le (M : ℕ) (v : Fin (M + 1) → ℝ) (j : Fin (M + 1)) : v (finiteMinIndex M v) ≤ v j

The selected coordinate minimizes the vector.

theorem BGW.StableTrees.finiteMinIndex_eq_iff (M : ℕ) (v : Fin (M + 1) → ℝ) (k : Fin (M + 1)) : finiteMinIndex M v = k ↔ (∀ (j : Fin (M + 1)), v k ≤ v j) ∧ ∀ j < k, v k < v j

A Borel characterization of the first minimum, including ties.

theorem BGW.StableTrees.measurable_finiteMinIndex (M : ℕ) : Measurable (finiteMinIndex M)

The first minimizing index is measurable.

theorem BGW.StableTrees.finiteMinIndex_eq_of_min (M : ℕ) {v : Fin (M + 1) → ℝ} (hv : Function.Injective v) {k : Fin (M + 1)} (hk : ∀ (j : Fin (M + 1)), v k ≤ v j) : finiteMinIndex M v = k

An injective vector has a unique minimizing coordinate.

def BGW.StableTrees.cyclicDiff (M : ℕ) (v : Fin (M + 1) → ℝ) (i : Fin (M + 1)) : ℝ

A cyclic vector of adjacent differences.

Equations

• BGW.StableTrees.cyclicDiff M v i = v (i + 1) - v i

def BGW.StableTrees.cyclicPrimitive (M : ℕ) (x : Fin (M + 1) → ℝ) (i : Fin (M + 1)) : ℝ

The partial-sum potential of a cyclic increment vector, normalized to zero at zero.

Equations

• BGW.StableTrees.cyclicPrimitive M x i = ∑ j ∈ Finset.range ↑i, x ↑j

theorem BGW.StableTrees.cyclicPrimitive_diff (M : ℕ) (v : Fin (M + 1) → ℝ) (i : Fin (M + 1)) : cyclicPrimitive M (cyclicDiff M v) i = v i - v 0

Finite summation recovers a potential from its cyclic differences.

theorem BGW.StableTrees.measurable_cyclicPrimitive (M : ℕ) : Measurable (cyclicPrimitive M)

Partial-sum vectors are measurable functions of the increments.

theorem BGW.StableTrees.finiteMinIndex_sub_const (M : ℕ) (v : Fin (M + 1) → ℝ) (c : ℝ) : (finiteMinIndex M fun (i : Fin (M + 1)) => v i - c) = finiteMinIndex M v

Translating every coordinate leaves the first minimum unchanged.

theorem BGW.StableTrees.finiteMinIndex_shift (M : ℕ) {v : Fin (M + 1) → ℝ} (hv : Function.Injective v) (k : Fin (M + 1)) : (finiteMinIndex M fun (i : Fin (M + 1)) => v (i + k)) = finiteMinIndex M v - k

Cyclically relabeling distinct values relabels their minimum by subtraction.

theorem BGW.StableTrees.cyclicPrimitive_shift_diff (M : ℕ) (v : Fin (M + 1) → ℝ) (k i : Fin (M + 1)) : cyclicPrimitive M (fun (j : Fin (M + 1)) => cyclicDiff M v (j + k)) i = v (i + k) - v k

Partial summation of shifted cyclic differences recovers the shifted potential.