Contour paths and mirror symmetry on the locally finite carrier

Finite trees carry their interpolated contour, and infinite trees carry the zero path.

theorem BGW.StableTrees.ExactContour.continuous_contourLin (t : PlaneTree) : Continuous t.contourLin

The finite-tree contour interpolation is continuous on the real line.

theorem BGW.StableTrees.ExactContour.countable_finiteVertices : {τ : LocallyFinite.Tree | LocallyFinite.FiniteVertices τ}.Countable

The locally finite carrier has only countably many finite trees.

noncomputable def BGW.StableTrees.ExactContour.treeMirror (τ : LocallyFinite.Tree) : LocallyFinite.Tree

Mirror on the locally finite carrier: the mirror of the decoded finite tree, and the identity on infinite trees.

Equations

• BGW.StableTrees.ExactContour.treeMirror τ = if h : BGW.LocallyFinite.FiniteVertices τ then (BGW.PlaneTree.equivFiniteVertices.symm ⟨τ, h⟩).mirror.toLocallyFinite else τ

theorem BGW.StableTrees.ExactContour.measurable_treeMirror : Measurable treeMirror

Mirroring on the locally finite carrier is measurable.

theorem BGW.StableTrees.ExactContour.treeMirror_toLocallyFinite (t : PlaneTree) : treeMirror t.toLocallyFinite = t.mirror.toLocallyFinite

Mirroring a finite tree commutes with its encoding.

theorem BGW.StableTrees.ExactContour.treeMirror_treeMirror (τ : LocallyFinite.Tree) : treeMirror (treeMirror τ) = τ

Mirroring on the locally finite carrier is an involution.

theorem BGW.StableTrees.ExactContour.map_treeMirror_exactTreeLaw (μ : PMF ℕ) (n : ℕ) : (DiscreteForest.exactTreeLaw μ n).map treeMirror = DiscreteForest.exactTreeLaw μ n

Mirror invariance of the exact-size conditioned law, for every n (size and weight are preserved; the Dirac leaf of the junk branch is mirror invariant).