Conditioning on size and finitely many degree counts

The conditioning event consists of finite trees with the prescribed size and degree counts. The finite-size restriction is explicit: no count of all vertices of an infinite tree is totalized to a natural number. The law, atoms and cyclic bridge mass retain all zero-event and lattice restrictions through the actual event mass.

def BGW.LocallyFinite.degreeSizeEvent (n r : ℕ) (ks cs : Fin r → ℕ) : Set Tree

Finite trees with size n and the indicated finitely many outdegree counts.

Equations

• BGW.LocallyFinite.degreeSizeEvent n r ks cs = BGW.PlaneTree.toLocallyFinite '' {t : BGW.PlaneTree | t.size = n ∧ ∀ (j : Fin r), t.degreeCount (ks j) = cs j}

theorem BGW.LocallyFinite.toLocallyFinite_mem_degreeSizeEvent_iff (t : PlaneTree) (n r : ℕ) (ks cs : Fin r → ℕ) : t.toLocallyFinite ∈ degreeSizeEvent n r ks cs ↔ t.size = n ∧ ∀ (j : Fin r), t.degreeCount (ks j) = cs j

theorem BGW.LocallyFinite.measurableSet_degreeSizeEvent (n r : ℕ) (ks cs : Fin r → ℕ) : MeasurableSet (degreeSizeEvent n r ks cs)

theorem BGW.LocallyFinite.degreeSizeEvent_subset (n r : ℕ) (ks cs : Fin r → ℕ) : degreeSizeEvent n r ks cs ⊆ sizeEvent n

@[simp]

theorem BGW.LocallyFinite.degreeSizeEvent_no_marks (n : ℕ) (ks cs : Fin 0 → ℕ) : degreeSizeEvent n 0 ks cs = sizeEvent n

With no degree constraints the event is exactly the original size event.

@[simp]

theorem BGW.LocallyFinite.degreeSizeEvent_zero (r : ℕ) (ks cs : Fin r → ℕ) : degreeSizeEvent 0 r ks cs = ∅

theorem BGW.LocallyFinite.bienaymeLaw_degreeSizeEvent (μ : MeasureTheory.Measure ℕ) [MeasureTheory.IsProbabilityMeasure μ] (n r : ℕ) (ks cs : Fin r → ℕ) : (bienaymeLaw μ) (degreeSizeEvent n r ks cs) = ∑' (t : { t : PlaneTree // t.size = n }), PlaneTree.weight (fun (d : ℕ) => μ {d}) ↑t * if ∀ (j : Fin r), (↑t).degreeCount (ks j) = cs j then 1 else 0

The mass of the marked size class is its finite-tree weight sum.

theorem BGW.LocallyFinite.natCast_mul_bienaymeLaw_degreeSizeEvent (μ : MeasureTheory.Measure ℕ) [MeasureTheory.IsProbabilityMeasure μ] (n r : ℕ) (ks cs : Fin r → ℕ) : ↑n * (bienaymeLaw μ) (degreeSizeEvent n r ks cs) = (MeasureTheory.Measure.pi fun (x : Fin n) => μ) (countBridges n ∩ {ω : Fin n → ℕ | ∀ (j : Fin r), List.count (ks j) (List.ofFn ω) = cs j})

The degree-marked Kemperman identity in the actual offspring product law.

theorem BGW.LocallyFinite.isProbabilityMeasure_cond_degreeSizeEvent (μ : MeasureTheory.Measure ℕ) [MeasureTheory.IsProbabilityMeasure μ] {n r : ℕ} {ks cs : Fin r → ℕ} (h : (bienaymeLaw μ) (degreeSizeEvent n r ks cs) ≠ 0) : MeasureTheory.IsProbabilityMeasure (bienaymeLaw μ)[|degreeSizeEvent n r ks cs]

theorem BGW.LocallyFinite.cond_degreeSizeEvent_singleton (μ : MeasureTheory.Measure ℕ) [MeasureTheory.IsProbabilityMeasure μ] (n r : ℕ) (ks cs : Fin r → ℕ) (t : PlaneTree) : (bienaymeLaw μ)[{t.toLocallyFinite} | degreeSizeEvent n r ks cs] = if t.size = n ∧ ∀ (j : Fin r), t.degreeCount (ks j) = cs j then PlaneTree.weight (fun (d : ℕ) => μ {d}) t / (bienaymeLaw μ) (degreeSizeEvent n r ks cs) else 0

Marked conditional atoms, including zero conditioning mass.