Documentation

BGW.ContinuumTrees.CodingMeasure

Root and mass measure of a continuously coded tree #

The root is the image of time zero. The mass measure is the pushforward of Mathlib's Lebesgue probability measure on the unit interval through the continuous projection. The coding quotient receives its Borel structure once, and the actual pushforward is bundled as a probability measure and as the project's compact measured and rooted measured spaces.

These constructions are defined for every continuous real coding function. For a nonnegative function vanishing at zero, distance from the root is its value. If it also vanishes at one, the two endpoint times project to the same root. Nonnegativity is retained in this last claim: equal zero endpoint values alone do not exclude a negative interior minimum.

source
@[instance_reducible]
noncomputable instance BGW.ContinuumTrees.Coding.instMeasurableSpaceSpace (g : C(↑unitInterval, ℝ)) :
MeasurableSpace (Space g)
Equations
source
instance BGW.ContinuumTrees.Coding.instBorelSpaceSpace (g : C(↑unitInterval, ℝ)) :
BorelSpace (Space g)
source
noncomputable def BGW.ContinuumTrees.Coding.root (g : C(↑unitInterval, ℝ)) :
Space g

The distinguished point represented by time zero.

Equations
Instances For
    source
    theorem BGW.ContinuumTrees.Coding.measurable_projection (g : C(↑unitInterval, ℝ)) :
    Measurable (projection g)
    source
    noncomputable def BGW.ContinuumTrees.Coding.mass (g : C(↑unitInterval, ℝ)) :
    MeasureTheory.ProbabilityMeasure (Space g)

    The pushforward of Lebesgue probability on the unit interval.

    Equations
    Instances For
      source
      @[simp]
      theorem BGW.ContinuumTrees.Coding.coe_mass (g : C(↑unitInterval, ℝ)) :
      ↑(mass g) = MeasureTheory.Measure.map (projection g) MeasureTheory.volume
      source
      theorem BGW.ContinuumTrees.Coding.mass_apply (g : C(↑unitInterval, ℝ)) {A : Set (Space g)} (hA : MeasurableSet A) :
      ↑(mass g) A = MeasureTheory.volume (projection g ⁻¹' A)

      The mass measure is the genuine pushforward, with measurable projection.

      source
      noncomputable def BGW.ContinuumTrees.Coding.compactMeasuredSpace (g : C(↑unitInterval, ℝ)) :
      MetricMeasure.CompactMeasuredSpace

      The coded tree with its natural probability mass measure, on the whole metric carrier.

      Equations
      Instances For
        source
        noncomputable def BGW.ContinuumTrees.Coding.rootedCompactMeasuredSpace (g : C(↑unitInterval, ℝ)) :
        MetricMeasure.RootedCompactMeasuredSpace

        The coded compact measured tree rooted at the image of time zero.

        Equations
        Instances For
          source
          theorem BGW.ContinuumTrees.Coding.dist_root_projection (g : C(↑unitInterval, ℝ)) (hg : ∀ (t : ↑unitInterval), 0 ≤ g t) (h0 : g 0 = 0) (t : ↑unitInterval) :
          dist (root g) (projection g t) = g t

          A nonnegative coding function vanishing at zero gives distance from the root directly.

          source
          theorem BGW.ContinuumTrees.Coding.projection_zero_eq_one (g : C(↑unitInterval, ℝ)) (hg : ∀ (t : ↑unitInterval), 0 ≤ g t) (h0 : g 0 = 0) (h1 : g 1 = 0) :
          projection g 0 = projection g 1

          The endpoint times coincide in the quotient for a nonnegative function with zero endpoints.