Documentation

BGW.ContinuumTrees.VervaatBridge

The Vervaat image of the constructed Brownian bridge #

The anchored Brownian bridge gives a measurable continuous loop for every outcome on the constructed source probability space. Applying the deterministic Vervaat transformation gives an actual probability law on nonnegative continuous paths with zero endpoints.

The rooted measured tree law is the genuine image under coding by twice this path. Its root is represented by time zero, and its mass is the existing Lebesgue pushforward from the coding construction. The normalization is therefore explicitly T_(2e).

These are laws of the constructed Vervaat path and its coded tree. Almost-sure uniqueness of the bridge minimizer, strict interior positivity, and identification with the standard Brownian excursion and classical Brownian CRT laws are separate, unproved probabilistic statements.

source
noncomputable def BGW.ContinuumTrees.VervaatBridge.path (ω : NNReal → ℝ) :
C(↑unitInterval, ℝ)

The deterministic Vervaat transform of the anchored Brownian bridge path.

Equations
Instances For
    source
    theorem BGW.ContinuumTrees.VervaatBridge.measurable_path :
    Measurable path
    source
    theorem BGW.ContinuumTrees.VervaatBridge.path_nonneg (ω : NNReal → ℝ) (t : ↑unitInterval) :
    0 ≤ (path ω) t
    source
    @[simp]
    theorem BGW.ContinuumTrees.VervaatBridge.path_zero (ω : NNReal → ℝ) :
    (path ω) 0 = 0
    source
    @[simp]
    theorem BGW.ContinuumTrees.VervaatBridge.path_one (ω : NNReal → ℝ) :
    (path ω) 1 = 0
    source
    noncomputable def BGW.ContinuumTrees.VervaatBridge.law :
    MeasureTheory.ProbabilityMeasure C(↑unitInterval, ℝ)

    The actual Vervaat path law on the continuous-path space.

    Equations
    Instances For
      source
      @[simp]
      theorem BGW.ContinuumTrees.VervaatBridge.coe_law :
      ↑law = MeasureTheory.Measure.map path ProbabilityTheory.gaussianLimit
      source
      theorem BGW.ContinuumTrees.VervaatBridge.law_apply {A : Set C(↑unitInterval, ℝ)} (hA : MeasurableSet A) :
      ↑law A = ProbabilityTheory.gaussianLimit (path ⁻¹' A)
      source
      theorem BGW.ContinuumTrees.VervaatBridge.hasLaw_path :
      ProbabilityTheory.HasLaw path (↑law) ProbabilityTheory.gaussianLimit
      source
      noncomputable def BGW.ContinuumTrees.VervaatBridge.tree (ω : NNReal → ℝ) :
      MetricMeasure.RootedMeasuredGHSpace

      The rooted measured isometry class coded by twice the constructed Vervaat path.

      Equations
      Instances For
        source
        theorem BGW.ContinuumTrees.VervaatBridge.measurable_tree :
        Measurable tree
        source
        theorem BGW.ContinuumTrees.VervaatBridge.isRealTree (ω : NNReal → ℝ) :
        RealTree.IsRealTree (Coding.Space (2 • path ω))

        Each underlying coded carrier is a genuine compact real tree by the deterministic coding API.

        source
        noncomputable def BGW.ContinuumTrees.VervaatBridge.treeLaw :
        MeasureTheory.ProbabilityMeasure MetricMeasure.RootedMeasuredGHSpace

        The genuine probability law of the rooted measured tree coded by 2 • path.

        Equations
        Instances For
          source
          @[simp]
          theorem BGW.ContinuumTrees.VervaatBridge.coe_treeLaw :
          ↑treeLaw = MeasureTheory.Measure.map tree ProbabilityTheory.gaussianLimit
          source
          theorem BGW.ContinuumTrees.VervaatBridge.treeLaw_apply {A : Set MetricMeasure.RootedMeasuredGHSpace} (hA : MeasurableSet A) :
          ↑treeLaw A = ProbabilityTheory.gaussianLimit (tree ⁻¹' A)
          source
          theorem BGW.ContinuumTrees.VervaatBridge.hasLaw_tree :
          ProbabilityTheory.HasLaw tree (↑treeLaw) ProbabilityTheory.gaussianLimit
          source
          theorem BGW.ContinuumTrees.VervaatBridge.treeLaw_eq_map :
          treeLaw = law.map fun (e : C(↑unitInterval, ℝ)) => Coding.rootedMeasuredGHSpace (2 • e)

          Coding the actual path law agrees with the direct image of the source probability measure.