Countability of finite plane trees and the discrete measurable structure

Finite plane trees form a countable type, through an injective code into the natural numbers. They carry the discrete σ-algebra, so every set of trees is measurable. Their laws are therefore ordinary probability measures determined by point masses.

The discrete MeasurableSpace PlaneTree instance and the outdegree sequence degSeq are defined in PoissonDeclumping.Statements.Defs (from the upstream statement contract).

@[irreducible]

def PoissonDeclumping.PlaneTree.code : PlaneTree → ℕ

Injective numerical code of a plane tree: encode the list of child codes.

Equations

• (PoissonDeclumping.PlaneTree.node ts).code = Encodable.encode (List.map (fun (U : { x : PoissonDeclumping.PlaneTree // x ∈ ts }) => (↑U).code) ts.attach)

theorem PoissonDeclumping.PlaneTree.code_node (ts : List PlaneTree) : (node ts).code = Encodable.encode (List.map code ts)

theorem PoissonDeclumping.PlaneTree.code_injective : Function.Injective code

instance PoissonDeclumping.PlaneTree.instCountable : Countable PlaneTree

instance PoissonDeclumping.PlaneTree.instDiscreteMeasurableSpace : DiscreteMeasurableSpace PlaneTree

theorem PoissonDeclumping.PlaneTree.degSeq_node (ts : List PlaneTree) : (node ts).degSeq = ts.length :: List.flatMap degSeq ts

theorem PoissonDeclumping.PlaneTree.length_degSeq (T : PlaneTree) : T.degSeq.length = T.vertexCount