Geometric offspring and uniform plane trees

Mathlib's geometricMeasure p uses the success parameter p: its masses are p * (1 - p) ^ k when p ≠ 0. A finite tree of size n therefore has weight p ^ n * (1 - p) ^ (n - 1). For 0 < p < 1, conditioning on size gives the uniform measure on that finite size class, independently of p and of the offspring mean.

This is the geometric/uniform specialization of the BGW roadmap. Its parameter α equals 1 - p. The endpoint p = 0 is excluded: Mathlib defines geometricMeasure 0 to be dirac 0, rather than the zero sequence suggested by the formula. At size zero both the conditioned and the uniform measures are zero; positive sizes are admissible when p is strictly between zero and one.

theorem BGW.PlaneTree.weight_geometric (p : ↑unitInterval) (hp : p ≠ 0) (t : PlaneTree) : weight (fun (k : ℕ) => (ProbabilityTheory.geometricMeasure p) {k}) t = ENNReal.ofReal ↑p ^ t.size * ENNReal.ofReal (1 - ↑p) ^ (t.size - 1)

Under geometric offspring, the weight of a finite tree depends only on its size.

theorem BGW.LocallyFinite.finite_sizeEvent (n : ℕ) : (sizeEvent n).Finite

A fixed finite size class contains only finitely many locally finite trees.

theorem BGW.LocallyFinite.bienaymeLaw_sizeEvent_geometric_ne_zero_iff (p : ↑unitInterval) (hp0 : p ≠ 0) (hp1 : p ≠ 1) (n : ℕ) : (bienaymeLaw (ProbabilityTheory.geometricMeasure p)) (sizeEvent n) ≠ 0 ↔ 0 < n

For an interior geometric parameter, exactly the positive sizes are admissible.

theorem BGW.LocallyFinite.cond_sizeEvent_geometric_eq_uniform (p : ↑unitInterval) (hp0 : p ≠ 0) (hp1 : p ≠ 1) (n : ℕ) : (bienaymeLaw (ProbabilityTheory.geometricMeasure p))[|sizeEvent n] = MeasureTheory.Measure.uniformOfFinset ⋯.toFinset

A geometric BGW tree conditioned on size is uniform on that size class. This is an equality of zero measures when n = 0, and of probability measures otherwise.