The first long tree

The iid block law and a finite first-success decomposition identify the first block with size at least the cutoff. Its selection uses the whole block.

theorem BGW.StableTrees.DiscreteForest.measurableSet_sizeGeEvent (n : ℕ) : MeasurableSet (Attraction.sizeGeEvent n)

The inclusive size-tail event, including infinite trees, is measurable.

theorem BGW.StableTrees.DiscreteForest.toLocallyFinite_mem_sizeGe (t : PlaneTree) (n : ℕ) : t.toLocallyFinite ∈ Attraction.sizeGeEvent n ↔ n ≤ t.size

On a finite tree, the inclusive tail event is the ordinary size inequality.

theorem BGW.StableTrees.DiscreteForest.ae_exists_long_block (μ : PMF ℕ) (hc : IsCritical μ) (hne : μ 1 ≠ 1) (n : ℕ) : ∀ᵐ (ω : ℕ → ℕ) ∂↑(offspringSeqLaw μ), ∃ (r : ℕ), n ≤ ladderTime ω (r + 1) - ladderTime ω r

Existence of a long block a.s. (block sizes are iid with unbounded support).

theorem BGW.StableTrees.DiscreteForest.firstLongTree_law (μ : PMF ℕ) (hc : IsCritical μ) (hne : μ 1 ≠ 1) (n : ℕ) : (offspringSeqLaw μ).map (firstLongTree n) = tailTreeLaw μ n

The first long block is a BGW tree conditioned on size ≥ n.