Finite grids for the minimum time of the stable bridge

The closed stable bridge has cyclically invariant grid increments and an atomless minimum time. Cyclic invariance follows by composing full reversal with reversal of the strict prefix. These are the finite-grid inputs to the uniform minimum-time law.

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.

noncomputable def BGW.StableTrees.gridTime (M i : ℕ) : ↑(Set.Icc 0 1)

The grid time i/N in [0,1] (N = M + 1, i ≤ N as a natural number).

Equations

• BGW.StableTrees.gridTime M i = Set.projIcc 0 1 BGW.StableTrees.gridTime._proof_1 (↑i / (↑M + 1))

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

Grid increments f((i+1)/N) - f(i/N), i < N.

Equations

• BGW.StableTrees.gridIncr M f i = f (BGW.StableTrees.gridTime M (↑i + 1)) - f (BGW.StableTrees.gridTime M ↑i)

theorem BGW.StableTrees.gridTime_coe (M i : ℕ) (hi : i ≤ M + 1) : ↑(gridTime M i) = ↑i / (↑M + 1)

Grid times have the prescribed coordinates before clipping becomes necessary.

@[simp]

theorem BGW.StableTrees.gridTime_zero (M : ℕ) : gridTime M 0 = ⟨0, ⋯⟩

The first grid time is zero.

@[simp]

theorem BGW.StableTrees.gridTime_last (M : ℕ) : gridTime M (M + 1) = ⟨1, ⋯⟩

The terminal grid time is one.

theorem BGW.StableTrees.measurable_gridIncr (M : ℕ) : Measurable (gridIncr M)

Evaluation of the complete grid-increment vector is measurable.

theorem BGW.StableTrees.sum_gridIncr (M : ℕ) (f : Skorokhod.D 1 ℝ) : ∑ i : Fin (M + 1), gridIncr M f i = f ⟨1, ⋯⟩ - f ⟨0, ⋯⟩

The sum of the grid increments is the terminal displacement.

theorem BGW.StableTrees.stableBridgeLaw_ae_sum_gridIncr {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (M : ℕ) : ∀ᵐ (f : Skorokhod.D 1 ℝ) ∂↑(stableBridgeLaw θ), ∑ i : Fin (M + 1), gridIncr M f i = 0

The bridge increment vector lies on the zero-sum hyperplane almost surely.

theorem BGW.StableTrees.bridge_gridIncr_reverse {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (M : ℕ) : MeasureTheory.Measure.map (fun (f : Skorokhod.D 1 ℝ) (i : Fin (M + 1)) => gridIncr M f i.rev) ↑(stableBridgeLaw θ) = MeasureTheory.Measure.map (gridIncr M) ↑(stableBridgeLaw θ)

Reversing all coordinates preserves the bridge grid-increment law.

theorem BGW.StableTrees.bridge_first_gridIncr_perm {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (M : ℕ) (hM : 0 < M) (e : Equiv.Perm (Fin M)) : MeasureTheory.Measure.map (fun (f : Skorokhod.D 1 ℝ) (i : Fin M) => gridIncr M f (e i).castSucc) ↑(stableBridgeLaw θ) = MeasureTheory.Measure.map (fun (f : Skorokhod.D 1 ℝ) (i : Fin M) => gridIncr M f i.castSucc) ↑(stableBridgeLaw θ)

The increments preceding the terminal grid interval are exchangeable.

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

Exchangeability of the bridge increments under cyclic shifts of the grid.

theorem BGW.StableTrees.stableBridgeLaw_ae_vervaatTime_ne {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (x : ℝ) : ∀ᵐ (f : Skorokhod.D 1 ℝ) ∂↑(stableBridgeLaw θ), ↑(Skorokhod.vervaatTime f) ≠ x

No deterministic time can be the minimum time of the stable bridge.

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

Values on the grid excluding the duplicate terminal endpoint.

Equations

• BGW.StableTrees.bridgeGridValues M f i = f (BGW.StableTrees.gridTime M ↑i)

theorem BGW.StableTrees.measurable_bridgeGridValues (M : ℕ) : Measurable (bridgeGridValues M)

The finite-grid values are measurable.

theorem BGW.StableTrees.gridIncr_eq_cyclicDiff {M : ℕ} {f : Skorokhod.D 1 ℝ} (hf : f ⟨1, ⋯⟩ = f ⟨0, ⋯⟩) : gridIncr M f = cyclicDiff M (bridgeGridValues M f)

On a loop the final grid increment wraps back to the initial value.