Documentation

BGW.ContinuumTrees.Vervaat

The deterministic Vervaat transformation #

A continuous real function on the unit interval has a first global minimizer. This canonical choice is measurable, including for functions with several minimizers: its sublevel sets are the closed sets on which the minimum over an initial interval equals the global minimum.

For a continuous loop, rotating time to this minimizer and subtracting the minimum gives a continuous nonnegative function with both endpoints zero. The resulting map on the subtype of continuous loops is measurable. Uniqueness of a Brownian bridge's minimizer, strict interior positivity, and identification of the transformed law with a Brownian excursion are separate probabilistic statements, not conclusions of this deterministic construction.

source
theorem BGW.ContinuumTrees.Vervaat.exists_firstMinimum (g : C(↑unitInterval, ℝ)) :
∃ (r : ↑unitInterval), IsLeast {t : ↑unitInterval | g t = Coding.intervalMin g 0 1} r

The set of global minimizers has a least element, with both endpoint times included.

source
noncomputable def BGW.ContinuumTrees.Vervaat.firstMinimum (g : C(↑unitInterval, ℝ)) :
↑unitInterval

The first global minimizer, defined on all continuous real paths.

Equations
Instances For
    source
    theorem BGW.ContinuumTrees.Vervaat.isLeast_firstMinimum (g : C(↑unitInterval, ℝ)) :
    IsLeast {t : ↑unitInterval | g t = Coding.intervalMin g 0 1} (firstMinimum g)
    source
    theorem BGW.ContinuumTrees.Vervaat.firstMinimum_le_iff (g : C(↑unitInterval, ℝ)) (a : ↑unitInterval) :
    firstMinimum g ≤ a ↔ Coding.intervalMin g 0 a = Coding.intervalMin g 0 1

    The first minimum is at most a precisely when the initial interval already attains it.

    source
    theorem BGW.ContinuumTrees.Vervaat.measurable_firstMinimum :
    Measurable firstMinimum

    The canonical first minimizer is Borel measurable without a uniqueness assumption.

    source
    noncomputable def BGW.ContinuumTrees.Vervaat.rotate (g : C(↑unitInterval, ℝ)) (hloop : g 0 = g 1) (r : ↑unitInterval) :
    C(↑unitInterval, ℝ)

    Circular rotation of a continuous loop; the loop condition removes the jump of fract.

    Equations
    Instances For
      source
      @[simp]
      theorem BGW.ContinuumTrees.Vervaat.rotate_apply (g : C(↑unitInterval, ℝ)) (hloop : g 0 = g 1) (r t : ↑unitInterval) :
      (rotate g hloop r) t = g (Coding.circularShift r t)
      source
      @[simp]
      theorem BGW.ContinuumTrees.Vervaat.rotate_zero (g : C(↑unitInterval, ℝ)) (hloop : g 0 = g 1) (r : ↑unitInterval) :
      g (Coding.circularShift r 0) = g r
      source
      @[simp]
      theorem BGW.ContinuumTrees.Vervaat.rotate_one (g : C(↑unitInterval, ℝ)) (hloop : g 0 = g 1) (r : ↑unitInterval) :
      g (Coding.circularShift r 1) = g r
      source
      noncomputable def BGW.ContinuumTrees.Vervaat.vervaat (g : { g : C(↑unitInterval, ℝ) // g 0 = g 1 }) :
      C(↑unitInterval, ℝ)

      Rotate a continuous loop at its first global minimum and subtract that minimum.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem BGW.ContinuumTrees.Vervaat.vervaat_apply (g : { g : C(↑unitInterval, ℝ) // g 0 = g 1 }) (t : ↑unitInterval) :
        (vervaat g) t = ↑g (Coding.circularShift (firstMinimum ↑g) t) - Coding.intervalMin (↑g) 0 1
        source
        theorem BGW.ContinuumTrees.Vervaat.vervaat_nonneg (g : { g : C(↑unitInterval, ℝ) // g 0 = g 1 }) (t : ↑unitInterval) :
        0 ≤ (vervaat g) t
        source
        @[simp]
        theorem BGW.ContinuumTrees.Vervaat.vervaat_zero (g : { g : C(↑unitInterval, ℝ) // g 0 = g 1 }) :
        ↑g (Coding.circularShift (firstMinimum ↑g) 0) - Coding.intervalMin (↑g) 0 1 = 0
        source
        @[simp]
        theorem BGW.ContinuumTrees.Vervaat.vervaat_one (g : { g : C(↑unitInterval, ℝ) // g 0 = g 1 }) :
        ↑g (Coding.circularShift (firstMinimum ↑g) 1) - Coding.intervalMin (↑g) 0 1 = 0
        source
        theorem BGW.ContinuumTrees.Vervaat.measurable_vervaat :
        Measurable vervaat

        Measurability of the Vervaat transformation on the subtype of continuous loops.