The continuous excursion obtained by changing the root

Circular time shift uses the representative in [0, 1). This time map is measurable, but is neither continuous nor surjective on the closed unit interval in general. Composing with the coding projection closes the endpoints and gives a continuous surjection onto the tree. Distance from the point represented by the chosen root time then gives a nonnegative continuous coding function with zero endpoints.

This is the construction in Le Gall, Random trees and applications, Lemma 2.3, pp. 273–274, https://arxiv.org/pdf/math/0511515v1. The exact distance identity is proved from attained interval minima, treating both sides of the circular cut and intervals crossing it. It descends to a surjective isometry sending the new root to the chosen vertex. Circular time shift preserves Lebesgue probability, by translation invariance of Haar measure on the unit additive circle. Consequently this same isometry preserves the actual mass measure.

noncomputable def BGW.ContinuumTrees.Coding.circularShift (r t : ↑unitInterval) : ↑unitInterval

Circular time shift with its value represented in [0, 1).

Equations

• BGW.ContinuumTrees.Coding.circularShift r t = ⟨Int.fract (↑r + ↑t), ⋯⟩

theorem BGW.ContinuumTrees.Coding.measurable_circularShift (r : ↑unitInterval) : Measurable (circularShift r)

noncomputable def BGW.ContinuumTrees.Coding.circularProjection (g : C(↑unitInterval, ℝ)) (r : ↑unitInterval) (hg : ∀ (t : ↑unitInterval), 0 ≤ g t) (h0 : g 0 = 0) (h1 : g 1 = 0) : C(↑unitInterval, Space g)

The circular traversal of the coded tree, continuous because its endpoint images agree.

Equations

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

@[simp]

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

theorem BGW.ContinuumTrees.Coding.circularProjection_surjective (g : C(↑unitInterval, ℝ)) (r : ↑unitInterval) (hg : ∀ (t : ↑unitInterval), 0 ≤ g t) (h0 : g 0 = 0) (h1 : g 1 = 0) : Function.Surjective ⇑(circularProjection g r hg h0 h1)

Although circular time shift omits time one, its image under the coding projection is full.

@[simp]

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

@[simp]

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

noncomputable def BGW.ContinuumTrees.Coding.reroot (g : C(↑unitInterval, ℝ)) (r : ↑unitInterval) (hg : ∀ (t : ↑unitInterval), 0 ≤ g t) (h0 : g 0 = 0) (h1 : g 1 = 0) : C(↑unitInterval, ℝ)

The continuous function recording distance from the new root during circular traversal.

Equations

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

@[simp]

theorem BGW.ContinuumTrees.Coding.reroot_apply (g : C(↑unitInterval, ℝ)) (r : ↑unitInterval) (hg : ∀ (t : ↑unitInterval), 0 ≤ g t) (h0 : g 0 = 0) (h1 : g 1 = 0) (t : ↑unitInterval) : (reroot g r hg h0 h1) t = codingDist g r (circularShift r t)

The construction is exactly the interval-minimum rerooting formula.

theorem BGW.ContinuumTrees.Coding.reroot_nonneg (g : C(↑unitInterval, ℝ)) (r : ↑unitInterval) (hg : ∀ (t : ↑unitInterval), 0 ≤ g t) (h0 : g 0 = 0) (h1 : g 1 = 0) (t : ↑unitInterval) : 0 ≤ (reroot g r hg h0 h1) t

@[simp]

theorem BGW.ContinuumTrees.Coding.reroot_zero (g : C(↑unitInterval, ℝ)) (r : ↑unitInterval) (hg : ∀ (t : ↑unitInterval), 0 ≤ g t) (h0 : g 0 = 0) (h1 : g 1 = 0) : codingDist g r (circularShift r 0) = 0

@[simp]

theorem BGW.ContinuumTrees.Coding.reroot_one (g : C(↑unitInterval, ℝ)) (r : ↑unitInterval) (hg : ∀ (t : ↑unitInterval), 0 ≤ g t) (h0 : g 0 = 0) (h1 : g 1 = 0) : codingDist g r (circularShift r 1) = 0

theorem BGW.ContinuumTrees.Coding.codingDist_reroot (g : C(↑unitInterval, ℝ)) (r : ↑unitInterval) (hg : ∀ (t : ↑unitInterval), 0 ≤ g t) (h0 : g 0 = 0) (h1 : g 1 = 0) (s t : ↑unitInterval) : codingDist (reroot g r hg h0 h1) s t = codingDist g (circularShift r s) (circularShift r t)

Changing the root preserves all coded distances after the circular change of time.

noncomputable def BGW.ContinuumTrees.Coding.rerootMap (g : C(↑unitInterval, ℝ)) (r : ↑unitInterval) (hg : ∀ (t : ↑unitInterval), 0 ≤ g t) (h0 : g 0 = 0) (h1 : g 1 = 0) : Space (reroot g r hg h0 h1) → Space g

The map on coding quotients induced by circular traversal of the original tree.

Equations

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

theorem BGW.ContinuumTrees.Coding.rerootMap_isometry (g : C(↑unitInterval, ℝ)) (r : ↑unitInterval) (hg : ∀ (t : ↑unitInterval), 0 ≤ g t) (h0 : g 0 = 0) (h1 : g 1 = 0) : Isometry (rerootMap g r hg h0 h1)

theorem BGW.ContinuumTrees.Coding.rerootMap_surjective (g : C(↑unitInterval, ℝ)) (r : ↑unitInterval) (hg : ∀ (t : ↑unitInterval), 0 ≤ g t) (h0 : g 0 = 0) (h1 : g 1 = 0) : Function.Surjective (rerootMap g r hg h0 h1)

noncomputable def BGW.ContinuumTrees.Coding.rerootIsometry (g : C(↑unitInterval, ℝ)) (r : ↑unitInterval) (hg : ∀ (t : ↑unitInterval), 0 ≤ g t) (h0 : g 0 = 0) (h1 : g 1 = 0) : Space (reroot g r hg h0 h1) ≃ᵢ Space g

The surjective isometry from the rerooted coding quotient to the original tree.

Equations

• BGW.ContinuumTrees.Coding.rerootIsometry g r hg h0 h1 = { toEquiv := Equiv.ofBijective (BGW.ContinuumTrees.Coding.rerootMap g r hg h0 h1) ⋯, isometry_toFun := ⋯ }

@[simp]

theorem BGW.ContinuumTrees.Coding.rerootIsometry_projection (g : C(↑unitInterval, ℝ)) (r : ↑unitInterval) (hg : ∀ (t : ↑unitInterval), 0 ≤ g t) (h0 : g 0 = 0) (h1 : g 1 = 0) (t : ↑unitInterval) : (rerootIsometry g r hg h0 h1) (projection (reroot g r hg h0 h1) t) = projection g (circularShift r t)

@[simp]

theorem BGW.ContinuumTrees.Coding.rerootIsometry_root (g : C(↑unitInterval, ℝ)) (r : ↑unitInterval) (hg : ∀ (t : ↑unitInterval), 0 ≤ g t) (h0 : g 0 = 0) (h1 : g 1 = 0) : (rerootIsometry g r hg h0 h1) (root (reroot g r hg h0 h1)) = projection g r

The new coding root is sent to the chosen vertex, rather than necessarily to the old root.

theorem BGW.ContinuumTrees.Coding.measurePreserving_circularShift (r : ↑unitInterval) : MeasureTheory.MeasurePreserving (circularShift r) MeasureTheory.volume MeasureTheory.volume

Circular time shift preserves Lebesgue probability, including the endpoint convention.

theorem BGW.ContinuumTrees.Coding.map_mass_rerootIsometry (g : C(↑unitInterval, ℝ)) (r : ↑unitInterval) (hg : ∀ (t : ↑unitInterval), 0 ≤ g t) (h0 : g 0 = 0) (h1 : g 1 = 0) : MeasureTheory.Measure.map ⇑(rerootIsometry g r hg h0 h1) ↑(mass (reroot g r hg h0 h1)) = ↑(mass g)

The rerooting isometry carries the genuine pushforward mass to the original mass measure.

theorem BGW.ContinuumTrees.Coding.measuredIsometry_reroot (g : C(↑unitInterval, ℝ)) (r : ↑unitInterval) (hg : ∀ (t : ↑unitInterval), 0 ≤ g t) (h0 : g 0 = 0) (h1 : g 1 = 0) : (rootedCompactMeasuredSpace (reroot g r hg h0 h1)).MeasuredIsometry { space := compactMeasuredSpace g, root := projection g r }

The rerooted coding is measured-isometric to the original tree rooted at time r.