Documentation

BGW.ContinuumTrees.BrownianBridgeGrid

Finite grids of the Brownian bridge #

The grid has n + 1 times i / (n + 1), including zero and excluding one. Its centered cyclic rotations have the same law, as proved directly from the Gaussian finite-dimensional distributions. Distinct grid values are almost surely unequal. Thus the probability that all grid values are nonnegative is 1 / (n + 1), which proves that the continuous bridge has negative minimum.

No assertion about uniqueness of the continuous minimum, or identification of the Vervaat image with the classical excursion law, is used here.

source
noncomputable def BGW.ContinuumTrees.BrownianBridge.gridTime (n : ℕ) (i : Fin (n + 1)) :
↑unitInterval

An equally spaced grid including zero and excluding the duplicate endpoint one.

Equations
Instances For
    source
    @[simp]
    theorem BGW.ContinuumTrees.BrownianBridge.coe_gridTime (n : ℕ) (i : Fin (n + 1)) :
    ↑(gridTime n i) = ↑↑i / ↑(n + 1)
    source
    @[simp]
    theorem BGW.ContinuumTrees.BrownianBridge.gridTime_zero (n : ℕ) :
    gridTime n 0 = 0
    source
    theorem BGW.ContinuumTrees.BrownianBridge.gridTime_lt_one (n : ℕ) (i : Fin (n + 1)) :
    ↑(gridTime n i) < 1
    source
    theorem BGW.ContinuumTrees.BrownianBridge.gridTime_injective (n : ℕ) :
    Function.Injective (gridTime n)
    source
    noncomputable def BGW.ContinuumTrees.BrownianBridge.gridValues (n : ℕ) (f : C(↑unitInterval, ℝ)) (i : Fin (n + 1)) :
    ℝ

    Evaluation of a continuous path on the finite grid.

    Equations
    Instances For
      source
      theorem BGW.ContinuumTrees.BrownianBridge.measurable_gridValues (n : ℕ) :
      Measurable (gridValues n)
      source
      theorem BGW.ContinuumTrees.BrownianBridge.identDistrib_grid_rotation (n : ℕ) (k : Fin (n + 1)) :
      ProbabilityTheory.IdentDistrib (fun (f : C(↑unitInterval, ℝ)) (i : Fin (n + 1)) => gridValues n f (i + k) - gridValues n f k) (gridValues n) ↑law ↑law

      Centered cyclic rotations of the grid have the same law. This invariance is derived from Gaussian means and covariances; it is not an assumption on the bridge.

      source
      theorem BGW.ContinuumTrees.BrownianBridge.ae_gridValues_injective (n : ℕ) :
      ∀ᵐ (f : C(↑unitInterval, ℝ)) ∂↑law, Function.Injective (gridValues n f)

      All distinct values on the grid are almost surely unequal.

      source
      theorem BGW.ContinuumTrees.BrownianBridge.ae_existsUnique_gridMinimum (n : ℕ) :
      ∀ᵐ (f : C(↑unitInterval, ℝ)) ∂↑law, ∃! k : Fin (n + 1), ∀ (i : Fin (n + 1)), gridValues n f k ≤ gridValues n f i

      The grid has a unique minimizing index almost surely, including the one-point grid.

      source
      theorem BGW.ContinuumTrees.BrownianBridge.measure_grid_nonnegative (n : ℕ) :
      ↑law {f : C(↑unitInterval, ℝ) | ∀ (i : Fin (n + 1)), 0 ≤ gridValues n f i} = (↑(n + 1))⁻¹

      Exact finite-grid positivity probability; the duplicate value at time one is excluded.

      source
      theorem BGW.ContinuumTrees.BrownianBridge.ae_intervalMin_neg :
      ∀ᵐ (f : C(↑unitInterval, ℝ)) ∂↑law, Coding.intervalMin f 0 1 < 0

      The continuous bridge has a strictly negative global minimum almost surely. The conclusion excludes both deterministic zero endpoints as minimizers.