The compact metric quotient of a continuous coding function

Point g is a fresh copy of the time interval carrying the coding pseudometric. Its topology is the one supplied by that pseudometric; no metric or topology on unitInterval is replaced. Space g uses Mathlib's separation quotient and its canonical metric, identifying exactly the pairs of times at coding distance zero. The projection from the usual compact time interval is continuous and onto, so the quotient is compact and nonempty.

These results hold for any continuous real coding function. They do not yet assert the real-tree property, which requires separate proofs of the four-point and midpoint properties.

structure BGW.ContinuumTrees.Coding.Point (g : C(↑unitInterval, ℝ)) : Type

A fresh carrier for the coding pseudometric, distinct from the usual metric time interval.

• time : ↑unitInterval

  The time parameter represented by this point of the coding pseudometric.

instance BGW.ContinuumTrees.Coding.instNonemptyPoint (g : C(↑unitInterval, ℝ)) : Nonempty (Point g)

@[instance_reducible]

noncomputable instance BGW.ContinuumTrees.Coding.instPseudoMetricSpacePoint (g : C(↑unitInterval, ℝ)) : PseudoMetricSpace (Point g)

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev BGW.ContinuumTrees.Coding.Space (g : C(↑unitInterval, ℝ)) : Type

The standard metric quotient of the coding pseudometric. Its metric is supplied by Mathlib.

Equations

• BGW.ContinuumTrees.Coding.Space g = SeparationQuotient (BGW.ContinuumTrees.Coding.Point g)

noncomputable def BGW.ContinuumTrees.Coding.projection (g : C(↑unitInterval, ℝ)) (t : ↑unitInterval) : Space g

The canonical projection from times, using the ordinary topology on the source interval.

Equations

• BGW.ContinuumTrees.Coding.projection g t = SeparationQuotient.mk { time := t }

theorem BGW.ContinuumTrees.Coding.projection_surjective (g : C(↑unitInterval, ℝ)) : Function.Surjective (projection g)

@[simp]

theorem BGW.ContinuumTrees.Coding.dist_projection (g : C(↑unitInterval, ℝ)) (s t : ↑unitInterval) : dist (projection g s) (projection g t) = codingDist g s t

theorem BGW.ContinuumTrees.Coding.projection_eq_iff (g : C(↑unitInterval, ℝ)) (s t : ↑unitInterval) : projection g s = projection g t ↔ codingDist g s t = 0

The quotient relation is exactly zero coding distance.

theorem BGW.ContinuumTrees.Coding.continuous_projection (g : C(↑unitInterval, ℝ)) : Continuous (projection g)

Continuity uses the usual time topology, not the topology of the coding pseudometric.

instance BGW.ContinuumTrees.Coding.instCompactSpaceSpace (g : C(↑unitInterval, ℝ)) : CompactSpace (Space g)