The surviving children of the root

noncomputable def BranchingProcess.survivors {N : ℕ} (c : Word N → ℕ) : Finset (Fin N)

The children of the root that found an infinite subtree: the letters i below the offspring count at the root whose shifted field survives.

Equations

• BranchingProcess.survivors c = {i : Fin N | ↑i < c [] ∧ BranchingProcess.Survives fun (w : BranchingProcess.Word N) => c (i :: w)}

theorem BranchingProcess.mem_survivors {N : ℕ} {c : Word N → ℕ} {i : Fin N} : i ∈ survivors c ↔ ↑i < c [] ∧ Survives fun (w : Word N) => c (i :: w)

Membership in survivors, unfolded.

noncomputable def BranchingProcess.skeletonDegree {N : ℕ} (c : Word N → ℕ) : ℕ

The arity of the root in the skeleton: the number of children of the root whose own subtree is infinite. Under the conditioning this is the quantity the Harris-Sevastyanov transform is the law of.

Equations

• BranchingProcess.skeletonDegree c = (BranchingProcess.survivors c).card

theorem BranchingProcess.survives_iff_exists_child {N : ℕ} {c : Word N → ℕ} : Survives c ↔ ∃ (i : Fin N), ↑i < c [] ∧ Survives fun (w : Word N) => c (i :: w)

Survival is survival of a child. One direction is the pigeonhole exists_infinite_child_of_infinite; the other is the injection of a child subtree into the sample.

theorem BranchingProcess.survives_iff_skeletonDegree_ne_zero {N : ℕ} {c : Word N → ℕ} : Survives c ↔ skeletonDegree c ≠ 0

Survival is a positive skeleton degree at the root.

theorem BranchingProcess.not_survives_iff_survivors_eq_empty {N : ℕ} {c : Word N → ℕ} : ¬Survives c ↔ survivors c = ∅

Extinction is the absence of a surviving child.

theorem BranchingProcess.mem_survivors_iff_mem_skeleton {N : ℕ} {c : Word N → ℕ} {i : Fin N} : i ∈ survivors c ↔ [i] ∈ skeleton c

The surviving children are the skeleton children of the root: the branching property identifies the shifted field with the residual subtree.

Measurability of the skeleton degree

theorem BranchingProcess.measurable_shift {N : ℕ} (i : Fin N) : Measurable fun (c : Word N → ℕ) (w : Word N) => c (i :: w)

The offspring field of a child subtree is a measurable function of the field.

theorem BranchingProcess.measurableSet_mem_survivors {N : ℕ} (i : Fin N) : MeasurableSet {c : Word N → ℕ | i ∈ survivors c}

A single letter belonging to the surviving children is a measurable event: the offspring count at the root is a coordinate, and survival of the child subtree is measurableSet_survives pulled back along measurable_shift.

theorem BranchingProcess.measurableSet_survivors_eq {N : ℕ} (S : Finset (Fin N)) : MeasurableSet {c : Word N → ℕ | survivors c = S}

The surviving children form a prescribed set on a measurable event: a finite intersection, one condition per letter.

theorem BranchingProcess.measurableSet_skeletonDegree_eq {N : ℕ} (k : ℕ) : MeasurableSet {c : Word N → ℕ | skeletonDegree c = k}

The skeleton degree is measurable at each value: the event is the union, over the finitely many candidate sets of surviving children, of the events of measurableSet_survivors_eq.

theorem BranchingProcess.measurable_skeletonDegree {N : ℕ} : Measurable skeletonDegree

The skeleton degree is a measurable function.

The letters naming a child

def BranchingProcess.childSet (N j : ℕ) : Finset (Fin N)

The letters naming a child of a root with j children.

Equations

• BranchingProcess.childSet N j = {i : Fin N | ↑i < j}

@[simp]

theorem BranchingProcess.mem_childSet {N j : ℕ} {i : Fin N} : i ∈ childSet N j ↔ ↑i < j

theorem BranchingProcess.card_childSet {N j : ℕ} (hj : j ≤ N) : (childSet N j).card = j

An alphabet wide enough to carry j children names exactly j of them.

theorem BranchingProcess.survivors_subset {N : ℕ} (c : Word N → ℕ) : survivors c ⊆ childSet N (c [])

The surviving children are children.

theorem BranchingProcess.prod_ite_survivors {N j : ℕ} (hj : j ≤ N) {S : Finset (Fin N)} (hS : S ⊆ childSet N j) (A B : ENNReal) : (∏ i : Fin N, if i ∈ S then A else if ↑i < j then B else 1) = A ^ S.card * B ^ (j - S.card)

The product over the children of a root with j children of a factor that is A at a surviving child, B at a dying one and 1 at a letter naming no child.

The survival pattern of the children as a product event

def BranchingProcess.skelBox {N : ℕ} (j : ℕ) (S : Finset (Fin N)) (i : Option (Fin N)) : Set (Branch N i → ℕ)

The product event at the root: the root has j children, those named by S found infinite subtrees, and the remaining children die.

Equations

• One or more equations did not get rendered due to their size.
• BranchingProcess.skelBox j S none = {u : BranchingProcess.Branch N none → ℕ | u BranchingProcess.rootIdx = j}

@[simp]

theorem BranchingProcess.skelBox_none {N : ℕ} (j : ℕ) (S : Finset (Fin N)) : skelBox j S none = {u : Branch N none → ℕ | u rootIdx = j}

@[simp]

theorem BranchingProcess.skelBox_some {N : ℕ} (j : ℕ) (S : Finset (Fin N)) (i : Fin N) : skelBox j S (some i) = if i ∈ S then {c : Word N → ℕ | Survives c} else if ↑i < j then {c : Word N → ℕ | ¬Survives c} else Set.univ

theorem BranchingProcess.measurableSet_skelBox {N : ℕ} (j : ℕ) (S : Finset (Fin N)) (i : Option (Fin N)) : MeasurableSet (skelBox j S i)

theorem BranchingProcess.split_preimage_skelBox {N : ℕ} (j : ℕ) (S : Finset (Fin N)) (hS : S ⊆ childSet N j) : split ⁻¹' Set.univ.pi (skelBox j S) = {c : Word N → ℕ | c [] = j} ∩ {c : Word N → ℕ | survivors c = S}

The product event is the survival pattern. The root has j children with S the set of those founding an infinite subtree exactly when the offspring count at the root is j, the subtrees under S survive and the remaining ones below j die.

theorem BranchingProcess.infinitePi_root_apply {J N : ℕ} (θ : Offspring J) (j : ℕ) : (MeasureTheory.Measure.infinitePi fun (x : Branch N none) => θ.law) {u : Branch N none → ℕ | u rootIdx = j} = ENNReal.ofReal (θ.mass j)

The root factor of the product: the offspring count at the root has the offspring law.

theorem BranchingProcess.sampleMeasure_root_survivors {J N : ℕ} (θ : Offspring J) (hJN : J ≤ N) {j : ℕ} (hj : j ≤ N) {S : Finset (Fin N)} (hS : S ⊆ childSet N j) : (sampleMeasure θ) ({c : Word N → ℕ | c [] = j} ∩ {c : Word N → ℕ | survivors c = S}) = ENNReal.ofReal (θ.mass j) * ENNReal.ofReal (1 - θ.extinction) ^ S.card * ENNReal.ofReal θ.extinction ^ (j - S.card)

The mass of a survival pattern. The root has j children of which exactly those named by S survive with probability θ_j (1-q)^{|S|} q^{j-|S|}: the splitting makes the subtrees independent, each surviving with probability 1-q.

The binomial count over the surviving children

noncomputable def BranchingProcess.Offspring.surviveWeight {J : ℕ} (θ : Offspring J) (k : ℕ) : ℝ

The surviving-children weights ∑_j θ_j C(j,k) (1-q)^k q^{j-k}: the law of the number of children of the root founding an infinite subtree, before the conditioning.

Equations

• θ.surviveWeight k = ∑ j ∈ Finset.range (J + 1), θ.mass j * ↑(j.choose k) * (1 - θ.extinction) ^ k * θ.extinction ^ (j - k)

theorem BranchingProcess.Offspring.surviveWeight_nonneg {J : ℕ} (θ : Offspring J) (k : ℕ) : 0 ≤ θ.surviveWeight k

Each weight is nonnegative.

theorem BranchingProcess.Offspring.surviveWeight_zero {J : ℕ} (θ : Offspring J) : θ.surviveWeight 0 = θ.extinction

No surviving child is extinction: the weight at k = 0 is f(q) = q, which is what the conditioning removes.

noncomputable def BranchingProcess.Offspring.skeletonWeight {J : ℕ} (θ : Offspring J) (k : ℕ) : ℝ

The skeleton law at the root, the Harris-Sevastyanov transform: the surviving-children weights renormalised by the survival probability 1-q, and zero at k = 0.

Equations

• θ.skeletonWeight k = if k = 0 then 0 else θ.surviveWeight k / (1 - θ.extinction)

theorem BranchingProcess.Offspring.skeletonWeight_of_ne_zero {J : ℕ} (θ : Offspring J) {k : ℕ} (hk : k ≠ 0) : θ.skeletonWeight k = θ.surviveWeight k / (1 - θ.extinction)

Off zero the skeleton law is the quotient.

@[simp]

theorem BranchingProcess.Offspring.skeletonWeight_zero {J : ℕ} (θ : Offspring J) : θ.skeletonWeight 0 = 0

theorem BranchingProcess.sampleMeasure_root_skeletonDegree {J N : ℕ} (θ : Offspring J) (hJN : J ≤ N) {j : ℕ} (hj : j ≤ N) (k : ℕ) : (sampleMeasure θ) ({c : Word N → ℕ | c [] = j} ∩ {c : Word N → ℕ | skeletonDegree c = k}) = ENNReal.ofReal (θ.mass j * ↑(j.choose k) * (1 - θ.extinction) ^ k * θ.extinction ^ (j - k))

The one-root count. The root has j children of which k survive with probability θ_j C(j,k) (1-q)^k q^{j-k}: the survival patterns of j children with k survivors are the k-element subsets of the j letters, and each carries the mass of sampleMeasure_root_survivors.

theorem BranchingProcess.sampleMeasure_skeletonDegree {J N : ℕ} (θ : Offspring J) (hJN : J ≤ N) (k : ℕ) : (sampleMeasure θ) {c : Word N → ℕ | skeletonDegree c = k} = ENNReal.ofReal (θ.surviveWeight k)

The law of the skeleton degree. Summing the one-root count over the offspring count at the root, the number of surviving children of the root is k with probability ∑_j θ_j C(j,k) (1-q)^k q^{j-k}.

The law conditioned on survival

noncomputable def BranchingProcess.survivalMeasure {J N : ℕ} (θ : Offspring J) : MeasureTheory.Measure (Word N → ℕ)

The law conditioned on survival, the measure ℙ* the paper works under: the sample law conditioned on the event that the tree is infinite.

Equations

• BranchingProcess.survivalMeasure θ = (BranchingProcess.sampleMeasure θ)[|{c : BranchingProcess.Word N → ℕ | BranchingProcess.Survives c}]

theorem BranchingProcess.sampleMeasure_survives_ne_zero {J N : ℕ} (θ : Offspring J) (hJN : J ≤ N) (hq : θ.extinction < 1) : (sampleMeasure θ) {c : Word N → ℕ | Survives c} ≠ 0

The conditioning event has positive mass exactly for q < 1.

theorem BranchingProcess.isProbabilityMeasure_survivalMeasure {J N : ℕ} (θ : Offspring J) (hJN : J ≤ N) (hq : θ.extinction < 1) : MeasureTheory.IsProbabilityMeasure (survivalMeasure θ)

The conditioned law is a probability measure once the tree survives with positive probability.

theorem BranchingProcess.survivalMeasure_apply {J N : ℕ} (θ : Offspring J) (t : Set (Word N → ℕ)) : (survivalMeasure θ) t = ((sampleMeasure θ) {c : Word N → ℕ | Survives c})⁻¹ * (sampleMeasure θ) ({c : Word N → ℕ | Survives c} ∩ t)

The conditioned law, unfolded: the mass of the intersection with the survival event, divided by the survival probability.

theorem BranchingProcess.survivalMeasure_survives {J N : ℕ} (θ : Offspring J) (hJN : J ≤ N) (hq : θ.extinction < 1) : (survivalMeasure θ) {c : Word N → ℕ | Survives c} = 1

The conditioned law is carried by survival.

theorem BranchingProcess.survivalMeasure_skeletonDegree {J N : ℕ} (θ : Offspring J) (hJN : J ≤ N) (hq : θ.extinction < 1) (k : ℕ) : (survivalMeasure θ) {c : Word N → ℕ | skeletonDegree c = k} = ENNReal.ofReal (θ.skeletonWeight k)

The skeleton law at the root, the skeleton half of the Harris decomposition for the arity of the root: conditioned on survival, the number of surviving children of the root is k with probability θ̃_k, the surviving-children weight renormalised by the survival probability 1-q. The value k = 0 is what the conditioning removes.

The conjugate law of a dying subtree

noncomputable def BranchingProcess.bushMeasure {J N : ℕ} (θ : Offspring J) : MeasureTheory.Measure (Word N → ℕ)

The law conditioned on extinction, the law of a bush: the sample law conditioned on the event that the tree is finite.

Equations

• BranchingProcess.bushMeasure θ = (BranchingProcess.sampleMeasure θ)[|{c : BranchingProcess.Word N → ℕ | ¬BranchingProcess.Survives c}]

theorem BranchingProcess.bushMeasure_root {J N : ℕ} (θ : Offspring J) (hJN : J ≤ N) (hq : 0 < θ.extinction) {j : ℕ} (hj : j ≤ N) : (bushMeasure θ) {c : Word N → ℕ | c [] = j} = ENNReal.ofReal (θ.mass j * θ.extinction ^ j / θ.extinction)

The conjugate law, the bush half of the Harris decomposition: conditioned on dying, the root of a subtree has j children with probability θ_j q^{j-1}, the law tilted by the extinction probability. The quotient carries the case j = 0.