Constraining the dying subtrees alongside the surviving ones

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

The extra factors constraining the dying subtrees: a letter naming a child outside the surviving pattern carries the set indexed by that letter, and the letters naming no child carry nothing.

Equations

• BranchingProcess.dyingOnly j S B none = Set.univ
• BranchingProcess.dyingOnly j S B (some i) = if i ∈ S then Set.univ else if ↑i < j then B ↑i else Set.univ

@[simp]

theorem BranchingProcess.dyingOnly_none {N : ℕ} (j : ℕ) (S : Finset (Fin N)) (B : ℕ → Set (Word N → ℕ)) : dyingOnly j S B none = Set.univ

@[simp]

theorem BranchingProcess.dyingOnly_some {N : ℕ} (j : ℕ) (S : Finset (Fin N)) (B : ℕ → Set (Word N → ℕ)) (i : Fin N) : dyingOnly j S B (some i) = if i ∈ S then Set.univ else if ↑i < j then B ↑i else Set.univ

theorem BranchingProcess.split_preimage_dyingOnly {N : ℕ} (j : ℕ) (S : Finset (Fin N)) (B : ℕ → Set (Word N → ℕ)) : split ⁻¹' Set.univ.pi (dyingOnly j S B) = {c : Word N → ℕ | ∀ i ∉ S, ↑i < j → (fun (w : Word N) => c (i :: w)) ∈ B ↑i}

The extra factors, read through the splitting.

def BranchingProcess.jointBox {N : ℕ} (j : ℕ) (S : Finset (Fin N)) (A B : ℕ → Set (Word N → ℕ)) (i : Option (Fin N)) : Set (Branch N i → ℕ)

The joint product event: the root has j children, those named by S found infinite subtrees and lie in the sets indexed by their rank, and the remaining children die and lie in the sets indexed by their letter.

Equations

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

@[simp]

theorem BranchingProcess.jointBox_none {N : ℕ} (j : ℕ) (S : Finset (Fin N)) (A B : ℕ → Set (Word N → ℕ)) : jointBox j S A B none = {u : Branch N none → ℕ | u rootIdx = j}

@[simp]

theorem BranchingProcess.jointBox_some {N : ℕ} (j : ℕ) (S : Finset (Fin N)) (A B : ℕ → Set (Word N → ℕ)) (i : Fin N) : jointBox j S A B (some i) = if i ∈ S then {c : Word N → ℕ | Survives c} ∩ A (rankOf S i) else if ↑i < j then {c : Word N → ℕ | ¬Survives c} ∩ B ↑i else Set.univ

theorem BranchingProcess.measurableSet_jointBox {N : ℕ} (j : ℕ) (S : Finset (Fin N)) {A B : ℕ → Set (Word N → ℕ)} (hA : ∀ (m : ℕ), MeasurableSet (A m)) (hB : ∀ (m : ℕ), MeasurableSet (B m)) (i : Option (Fin N)) : MeasurableSet (jointBox j S A B i)

theorem BranchingProcess.jointBox_eq_inter {N : ℕ} (j : ℕ) (S : Finset (Fin N)) (A B : ℕ → Set (Word N → ℕ)) (i : Option (Fin N)) : jointBox j S A B i = skelBox j S i ∩ bushesOnly S A i ∩ dyingOnly j S B i

The three product events cut out the joint one.

theorem BranchingProcess.split_preimage_jointBox {N j : ℕ} {S : Finset (Fin N)} (hS : S ⊆ childSet N j) (A B : ℕ → Set (Word N → ℕ)) : split ⁻¹' Set.univ.pi (jointBox j S A B) = {c : Word N → ℕ | c [] = j} ∩ {c : Word N → ℕ | survivors c = S} ∩ {c : Word N → ℕ | ∀ m < S.card, bushOf S m c ∈ A m} ∩ {c : Word N → ℕ | ∀ i ∉ S, ↑i < j → (fun (w : Word N) => c (i :: w)) ∈ B ↑i}

The joint product event constrains both families of subtrees.

theorem BranchingProcess.prod_ite_joint {N j : ℕ} {S : Finset (Fin N)} (hS : S ⊆ childSet N j) (X : ℕ → ENNReal) (Y : Fin N → ENNReal) : (∏ i : Fin N, if i ∈ S then X (rankOf S i) else if ↑i < j then Y i else 1) = (∏ m ∈ Finset.range S.card, X m) * ∏ i ∈ childSet N j \ S, Y i

The product over the children of a root with j children of a factor indexed by the rank at a surviving child, by the letter at a dying one, and trivial at a letter naming no child.

theorem BranchingProcess.sampleMeasure_root_joint {J N : ℕ} (θ : Offspring J) (hJN : J ≤ N) (hq : θ.extinction < 1) (hq0 : 0 < θ.extinction) {j : ℕ} (hj : j ≤ N) {S : Finset (Fin N)} (hS : S ⊆ childSet N j) {A B : ℕ → Set (Word N → ℕ)} (hA : ∀ (m : ℕ), MeasurableSet (A m)) (hB : ∀ (m : ℕ), MeasurableSet (B m)) : (sampleMeasure θ) ({c : Word N → ℕ | c [] = j} ∩ {c : Word N → ℕ | survivors c = S} ∩ {c : Word N → ℕ | ∀ m < S.card, bushOf S m c ∈ A m} ∩ {c : Word N → ℕ | ∀ i ∉ S, ↑i < j → (fun (w : Word N) => c (i :: w)) ∈ B ↑i}) = (ENNReal.ofReal (θ.mass j) * ENNReal.ofReal (1 - θ.extinction) ^ S.card * ENNReal.ofReal θ.extinction ^ (j - S.card) * ∏ m ∈ Finset.range S.card, (survivalMeasure θ) (A m)) * ∏ i ∈ childSet N j \ S, (bushMeasure θ) (B ↑i)

The mass of a survival pattern with both families of subtrees constrained. The splitting makes the subtrees independent: a surviving one contributes the conditioned mass of the set of its rank, a dying one the bush mass of the set of its letter.

One surviving child

theorem BranchingProcess.measurableSet_forall_dying {N : ℕ} (j : ℕ) (S : Finset (Fin N)) {B : Set (Word N → ℕ)} (hB : MeasurableSet B) : MeasurableSet {c : Word N → ℕ | ∀ i ∉ S, ↑i < j → (fun (w : Word N) => c (i :: w)) ∈ B}

The dying constraint is an event: one condition per letter.

theorem BranchingProcess.sampleMeasure_root_one_survivor {J N : ℕ} (θ : Offspring J) (hJN : J ≤ N) (hq : θ.extinction < 1) (hq0 : 0 < θ.extinction) {j : ℕ} (hj : j ≤ N) {A B : Set (Word N → ℕ)} (hA : MeasurableSet A) (hB : MeasurableSet B) : (sampleMeasure θ) ({c : Word N → ℕ | c [] = j} ∩ {c : Word N → ℕ | skeletonDegree c = 1} ∩ {c : Word N → ℕ | bushAt c 0 ∈ A} ∩ {c : Word N → ℕ | ∀ i ∉ survivors c, ↑i < j → (fun (w : Word N) => c (i :: w)) ∈ B}) = ENNReal.ofReal (θ.mass j * ↑j * (1 - θ.extinction) * θ.extinction ^ (j - 1)) * (survivalMeasure θ) A * (bushMeasure θ) B ^ (j - 1)

The neck step of the Harris decomposition: the root has j children of which exactly one survives, its subtree lying in A and every dying subtree in B. The surviving child can be any of the j letters, which is the factor j.

theorem BranchingProcess.survivalMeasure_root_one_survivor {J N : ℕ} (θ : Offspring J) (hJN : J ≤ N) (hq : θ.extinction < 1) (hq0 : 0 < θ.extinction) {j : ℕ} (hj : j ≤ N) {A B : Set (Word N → ℕ)} (hA : MeasurableSet A) (hB : MeasurableSet B) : (survivalMeasure θ) ({c : Word N → ℕ | c [] = j} ∩ {c : Word N → ℕ | skeletonDegree c = 1} ∩ {c : Word N → ℕ | bushAt c 0 ∈ A} ∩ {c : Word N → ℕ | ∀ i ∉ survivors c, ↑i < j → (fun (w : Word N) => c (i :: w)) ∈ B}) = ENNReal.ofReal (θ.mass j * ↑j * θ.extinction ^ (j - 1)) * (survivalMeasure θ) A * (bushMeasure θ) B ^ (j - 1)

The neck step under the conditioned law: the same event, conditioned on survival, its mass the reduced weight θ_j j q^{j-1} times the conditioned mass of the surviving subtree and the bush masses of the dying ones.