The exact uniform-vertex fringe identity

At an admissible size n, a tree with the size-conditioned law has n vertices. Averaging a fringe observable over its certified DFS addresses is therefore the uniform-vertex average. The theorem expresses this expectation through finite-tree atoms, without adding a measurable structure on PlaneTree. Indicator observables give Corollary cor:cyclicshift of Kortchemski–Vetter (source lines 777–824). The remainder walk ends at zero and its time is guarded by the fringe size being at most n.

The identity holds for arbitrary nonnegative extended observables and every size. At an inadmissible size both sides are zero, including when the observable takes the value infinity: the weighted numerator is then zero, so the totalized quotient is 0 / 0 = 0.

theorem BGW.LocallyFinite.cond_uniformFringe_eq_tsum (μ : MeasureTheory.Measure ℕ) [MeasureTheory.IsProbabilityMeasure μ] (n : ℕ) (G : PlaneTree → ENNReal) : ∑' (t : { t : PlaneTree // t.size = n }), (bienaymeLaw μ)[{(↑t).toLocallyFinite} | sizeEvent n] * ((↑n)⁻¹ * PlaneTree.fringeSum G ↑t) = (∑' (s : PlaneTree), if s.size ≤ n then PlaneTree.weight (fun (d : ℕ) => μ {d}) s * G s * (MeasureTheory.Measure.pi fun (x : Fin (n - s.size)) => μ) (countForestBridges 0 (n - s.size)) else 0) / (MeasureTheory.Measure.pi fun (x : Fin n) => μ) (countBridges n)

Atomic form of the uniform-vertex fringe formula, valid for every offspring probability measure. At admissible sizes the left side is the expected fringe observable at a uniform vertex.