Documentation

BGW.ContinuumTrees.Coding

The pseudodistance coded by a continuous function #

For a continuous real function g on the unit interval, intervalMin g s t is its minimum between s and t, and codingDist g s t = g s + g t - 2 * intervalMin g s t. We prove attainment of the minimum, its order properties, the pseudometric identities, and continuity in the two time variables. No sign or endpoint condition is needed for these results.

These are the deterministic distance formulas of milestone C1. The metric quotient and its compactness are separate from the further proofs that it is a real tree and carries the excursion's root and mass measure.

source
noncomputable def BGW.ContinuumTrees.Coding.intervalMin (g : C(↑unitInterval, ℝ)) (s t : ↑unitInterval) :
ℝ

The minimum of the coding function on the unordered closed interval between two times.

Equations
Instances For
    source
    theorem BGW.ContinuumTrees.Coding.exists_intervalMin (g : C(↑unitInterval, ℝ)) (s t : ↑unitInterval) :
    ∃ r ∈ Set.uIcc s t, intervalMin g s t = g r

    The infimum in intervalMin is attained on its nonempty compact interval.

    source
    theorem BGW.ContinuumTrees.Coding.intervalMin_le (g : C(↑unitInterval, ℝ)) (s t : ↑unitInterval) {r : ↑unitInterval} (hr : r ∈ Set.uIcc s t) :
    intervalMin g s t ≤ g r
    source
    theorem BGW.ContinuumTrees.Coding.le_intervalMin (g : C(↑unitInterval, ℝ)) (s t : ↑unitInterval) {a : ℝ} (ha : ∀ r ∈ Set.uIcc s t, a ≤ g r) :
    a ≤ intervalMin g s t

    Any lower bound on the coding function along the interval bounds its minimum.

    source
    @[simp]
    theorem BGW.ContinuumTrees.Coding.intervalMin_self (g : C(↑unitInterval, ℝ)) (s : ↑unitInterval) :
    intervalMin g s s = g s
    source
    theorem BGW.ContinuumTrees.Coding.intervalMin_comm (g : C(↑unitInterval, ℝ)) (s t : ↑unitInterval) :
    intervalMin g s t = intervalMin g t s
    source
    theorem BGW.ContinuumTrees.Coding.intervalMin_le_left (g : C(↑unitInterval, ℝ)) (s t : ↑unitInterval) :
    intervalMin g s t ≤ g s
    source
    theorem BGW.ContinuumTrees.Coding.intervalMin_le_right (g : C(↑unitInterval, ℝ)) (s t : ↑unitInterval) :
    intervalMin g s t ≤ g t
    source
    theorem BGW.ContinuumTrees.Coding.min_intervalMin_le (g : C(↑unitInterval, ℝ)) (s t u : ↑unitInterval) :
    min (intervalMin g s t) (intervalMin g t u) ≤ intervalMin g s u

    Splitting at an arbitrary third time gives the lower bound needed for the triangle inequality.

    source
    noncomputable def BGW.ContinuumTrees.Coding.codingDist (g : C(↑unitInterval, ℝ)) (s t : ↑unitInterval) :
    ℝ

    The real-valued pseudodistance coded by g.

    Equations
    Instances For
      source
      theorem BGW.ContinuumTrees.Coding.codingDist_nonneg (g : C(↑unitInterval, ℝ)) (s t : ↑unitInterval) :
      0 ≤ codingDist g s t
      source
      @[simp]
      theorem BGW.ContinuumTrees.Coding.codingDist_self (g : C(↑unitInterval, ℝ)) (s : ↑unitInterval) :
      codingDist g s s = 0
      source
      theorem BGW.ContinuumTrees.Coding.codingDist_comm (g : C(↑unitInterval, ℝ)) (s t : ↑unitInterval) :
      codingDist g s t = codingDist g t s
      source
      theorem BGW.ContinuumTrees.Coding.codingDist_triangle (g : C(↑unitInterval, ℝ)) (s t u : ↑unitInterval) :
      codingDist g s u ≤ codingDist g s t + codingDist g t u
      source
      theorem BGW.ContinuumTrees.Coding.continuous_intervalMin (g : C(↑unitInterval, ℝ)) :
      Continuous fun (p : ↑unitInterval × ↑unitInterval) => intervalMin g p.1 p.2

      The interval minimum is continuous as both endpoints vary.

      source
      theorem BGW.ContinuumTrees.Coding.continuous_codingDist (g : C(↑unitInterval, ℝ)) :
      Continuous fun (p : ↑unitInterval × ↑unitInterval) => codingDist g p.1 p.2

      The coding pseudodistance is continuous in the original topology of the time interval.