Reflection of finite plane trees

Mirroring reverses the children at every vertex, preserving sizes and offspring weights.

def BGW.PlaneTree.mirror : PlaneTree → PlaneTree

Mirror image of a plane tree: the children of every vertex in reverse order (mirror (node ts) = node (ts.map mirror).reverse).

Equations

• BGW.PlaneTree.mirror = BGW.PlaneTree.fold fun (ts : List BGW.PlaneTree) => BGW.PlaneTree.node ts.reverse

theorem BGW.PlaneTree.mirror_node (ts : List PlaneTree) : (node ts).mirror = node (List.map mirror ts).reverse

Mirroring a node reverses its children after mirroring each child.

theorem BGW.PlaneTree.mirror_mirror (t : PlaneTree) : t.mirror.mirror = t

The mirror is an involution.

theorem BGW.PlaneTree.size_mirror (t : PlaneTree) : t.mirror.size = t.size

The mirror preserves the size.

theorem BGW.PlaneTree.weight_mirror (p : ℕ → ENNReal) (t : PlaneTree) : weight p t.mirror = weight p t

The mirror preserves the offspring-product weight (same multiset of outdegrees).

theorem BGW.PlaneTree.contour_mirror (t : PlaneTree) : t.mirror.contour = t.contour.reverse

The entire contour word is reversed by mirroring.

theorem BGW.PlaneTree.contourAt_mirror (t : PlaneTree) {m : ℕ} (hm : m ≤ 2 * (t.size - 1)) : t.mirror.contourAt m = t.contourAt (2 * (t.size - 1) - m)

Contour of the mirror: C_mirror(m) = C(2(z-1) - m) for m ≤ 2(z-1).

theorem BGW.PlaneTree.contourLin_cell (t : PlaneTree) (k : ℕ) {s : ℝ} (hs : s ∈ Set.Icc (↑k) (↑k + 1)) : t.contourLin s = (1 - (s - ↑k)) * ↑(t.contourAt k) + (s - ↑k) * ↑(t.contourAt (k + 1))

On a closed integer cell, contour interpolation is affine between its endpoints.

theorem BGW.PlaneTree.contourLin_mirror (t : PlaneTree) {s : ℝ} (hs0 : 0 ≤ s) (hs : s ≤ 2 * (↑t.size - 1)) : t.mirror.contourLin s = t.contourLin (2 * (↑t.size - 1) - s)

Interpolated contour of the mirror: C_mirror(s) = C(2(z-1) - s) on [0, 2(z-1)].