Size-conditioned Bienaymé trees and admissible sizes

Source lines 699–700: 𝒯^n is a μ-Bienaymé tree conditioned to have n vertices, for the admissible sizes n, i.e. those with 𝐏(|𝒯| = n) > 0. We prove:

• conditioned_isProbabilityMeasure: at an admissible size the conditioned law is a probability measure (for every offspring law), and it is the zero measure otherwise;
• conditioned_apply_singleton: 𝐏(𝒯^n = T) = 𝐏_μ(T) / 𝐏_μ(|𝒯| = n) if |T| = n, else 0;
• infinite_setOf_admissible, nonempty_setOf_admissible: for critical μ with μ_1 ≠ 1, the admissible sizes form an infinite set containing 1 (sizes m j + 1 are admissible for any j ≥ 2 with μ_j > 0);
• the filter admissibleAtTop μ of large admissible sizes, which is proper for critical μ with μ_1 ≠ 1 (admissibleAtTop_neBot), and along which the conditioned laws are eventually probability measures.

No aperiodicity is assumed: periodic offspring laws have admissible sizes in a lattice.

theorem PoissonDeclumping.PlaneTree.bienayme_vertexCount_eq (μ : PMF ℕ) (n : ℕ) : (bienayme μ) {T : PlaneTree | T.vertexCount = n} = ∑' (T : PlaneTree), if T.vertexCount = n then weight μ T else 0

The law of the size: 𝐏_μ(|T| = n) = ∑_{|T| = n} ∏_{u∈T} μ_{k_u(T)}.

theorem PoissonDeclumping.PlaneTree.admissible_iff {μ : PMF ℕ} {n : ℕ} : Admissible μ n ↔ ∃ (T : PlaneTree), T.vertexCount = n ∧ weight μ T ≠ 0

A size is admissible iff some tree of that size has positive weight.

theorem PoissonDeclumping.PlaneTree.admissible_vertexCount {μ : PMF ℕ} {T : PlaneTree} (h : weight μ T ≠ 0) : Admissible μ T.vertexCount

The conditioned laws

theorem PoissonDeclumping.PlaneTree.conditioned_isProbabilityMeasure {μ : PMF ℕ} {n : ℕ} (h : Admissible μ n) : MeasureTheory.IsProbabilityMeasure (conditioned μ n)

At an admissible size, the conditioned law is a probability measure (for every offspring law; criticality is not needed since bienayme μ is finite).

theorem PoissonDeclumping.PlaneTree.conditioned_eq_zero_of_not_admissible {μ : PMF ℕ} {n : ℕ} (h : ¬Admissible μ n) : conditioned μ n = 0

At an inadmissible size, the conditioned "law" is the zero measure.

theorem PoissonDeclumping.PlaneTree.conditioned_apply (μ : PMF ℕ) (n : ℕ) (s : Set PlaneTree) : (conditioned μ n) s = ((bienayme μ) {T : PlaneTree | T.vertexCount = n})⁻¹ * (bienayme μ) ({T : PlaneTree | T.vertexCount = n} ∩ s)

theorem PoissonDeclumping.PlaneTree.conditioned_apply_singleton_of_vertexCount_eq {μ : PMF ℕ} {n : ℕ} {T : PlaneTree} (hT : T.vertexCount = n) : (conditioned μ n) {T} = weight μ T / (bienayme μ) {T : PlaneTree | T.vertexCount = n}

𝐏(𝒯^n = T) = 𝐏_μ(T) / 𝐏_μ(|𝒯| = n) for a tree T with n vertices.

theorem PoissonDeclumping.PlaneTree.conditioned_apply_singleton_of_vertexCount_ne {μ : PMF ℕ} {n : ℕ} {T : PlaneTree} (hT : T.vertexCount ≠ n) : (conditioned μ n) {T} = 0

𝐏(𝒯^n = T) = 0 for a tree T whose size is not n.

theorem PoissonDeclumping.PlaneTree.conditioned_apply_singleton (μ : PMF ℕ) (n : ℕ) (T : PlaneTree) : (conditioned μ n) {T} = if T.vertexCount = n then weight μ T / (bienayme μ) {T : PlaneTree | T.vertexCount = n} else 0

theorem PoissonDeclumping.PlaneTree.conditioned_vertexCount {μ : PMF ℕ} {n : ℕ} (h : Admissible μ n) : (conditioned μ n) {T : PlaneTree | T.vertexCount = n} = 1

The conditioned tree has n vertices almost surely.

Admissible sizes

theorem PoissonDeclumping.PlaneTree.admissible_one {μ : PMF ℕ} (h0 : μ 0 ≠ 0) : Admissible μ 1

Size 1 (the single-vertex tree) is admissible when μ_0 ≠ 0.

theorem PoissonDeclumping.PlaneTree.admissible_mul_add_one {μ : PMF ℕ} (h0 : μ 0 ≠ 0) {j : ℕ} (hj : 1 ≤ j) (hμj : μ j ≠ 0) (m : ℕ) : Admissible μ (m * j + 1)

If μ_0 ≠ 0 and μ_j ≠ 0 with j ≥ 1, every size m j + 1 is admissible.

theorem PoissonDeclumping.PlaneTree.infinite_setOf_admissible {μ : PMF ℕ} (hc : IsCritical μ) (hne : μ 1 ≠ 1) : {n : ℕ | Admissible μ n}.Infinite

For a critical μ with μ_1 ≠ 1, there are infinitely many admissible sizes.

theorem PoissonDeclumping.PlaneTree.nonempty_setOf_admissible {μ : PMF ℕ} (hc : IsCritical μ) (hne : μ 1 ≠ 1) : {n : ℕ | Admissible μ n}.Nonempty

The set of admissible sizes is nonempty (it contains 1).

def PoissonDeclumping.PlaneTree.admissibleAtTop (μ : PMF ℕ) : Filter ℕ

The filter "n → ∞ along admissible sizes".

Equations

• PoissonDeclumping.PlaneTree.admissibleAtTop μ = Filter.atTop ⊓ Filter.principal {n : ℕ | PoissonDeclumping.PlaneTree.Admissible μ n}

theorem PoissonDeclumping.PlaneTree.eventually_admissible (μ : PMF ℕ) : ∀ᶠ (n : ℕ) in admissibleAtTop μ, Admissible μ n

theorem PoissonDeclumping.PlaneTree.admissibleAtTop_le_atTop (μ : PMF ℕ) : admissibleAtTop μ ≤ Filter.atTop

theorem PoissonDeclumping.PlaneTree.eventually_isProbabilityMeasure_conditioned (μ : PMF ℕ) : ∀ᶠ (n : ℕ) in admissibleAtTop μ, MeasureTheory.IsProbabilityMeasure (conditioned μ n)

theorem PoissonDeclumping.PlaneTree.admissibleAtTop_neBot {μ : PMF ℕ} (hc : IsCritical μ) (hne : μ 1 ≠ 1) : (admissibleAtTop μ).NeBot

For a critical μ with μ_1 ≠ 1, the filter of admissible sizes is proper, so limits along it are meaningful.

instance PoissonDeclumping.PlaneTree.isProbabilityMeasure_conditioned_subtype {μ : PMF ℕ} (n : { n : ℕ // Admissible μ n }) : MeasureTheory.IsProbabilityMeasure (conditioned μ ↑n)

Subtype-indexed form: the conditioned law at an admissible size is a probability measure.