The dying subtrees, re-addressed by rank

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

The m-th dying subtree of the root: the dying children are the children outside the survivors, and dyingAt c m reads the subtree of the m-th of them in letter order, as bushAt does for the surviving children.

Equations

• BranchingProcess.dyingAt c m = BranchingProcess.bushOf (BranchingProcess.childSet N (c []) \ BranchingProcess.survivors c) m c

theorem BranchingProcess.measurable_dyingAt {N : ℕ} (m : ℕ) : Measurable fun (c : Word N → ℕ) => dyingAt c m

The dying subtrees are measurable: the root count and the pattern of survivors take countably many values, and on each of the corresponding events the subtree is a shift.

theorem BranchingProcess.measurableSet_forall_dyingAt {N : ℕ} (k : ℕ) {B : ℕ → Set (Word N → ℕ)} (hB : ∀ (m : ℕ), MeasurableSet (B m)) : MeasurableSet {c : Word N → ℕ | ∀ m < k, dyingAt c m ∈ B m}

Constraining the first k dying subtrees is a measurable event.

def BranchingProcess.rankSets {N : ℕ} (D : Finset (Fin N)) (B : ℕ → Set (Word N → ℕ)) : ℕ → Set (Word N → ℕ)

A rank-indexed family read at a letter: the set of the rank of the letter in D, and everything off the alphabet.

Equations

• BranchingProcess.rankSets D B i = if h : i < N then B (BranchingProcess.rankOf D ⟨i, h⟩) else Set.univ

theorem BranchingProcess.measurableSet_rankSets {N : ℕ} (D : Finset (Fin N)) {B : ℕ → Set (Word N → ℕ)} (hB : ∀ (m : ℕ), MeasurableSet (B m)) (i : ℕ) : MeasurableSet (rankSets D B i)

theorem BranchingProcess.rankSets_coe {N : ℕ} (D : Finset (Fin N)) (B : ℕ → Set (Word N → ℕ)) (i : Fin N) : rankSets D B ↑i = B (rankOf D i)

At a letter of the alphabet the rank-indexed family reads the rank.

The decoration of one skeleton vertex

def BranchingProcess.decorationEvent {N : ℕ} (j k : ℕ) (B : ℕ → Set (Word N → ℕ)) : Set (Word N → ℕ)

The decoration of the root: j children of which k survive, the dying subtrees constrained by their rank.

Equations

• One or more equations did not get rendered due to their size.

theorem BranchingProcess.measurableSet_decorationEvent {N : ℕ} (j k : ℕ) {B : ℕ → Set (Word N → ℕ)} (hB : ∀ (m : ℕ), MeasurableSet (B m)) : MeasurableSet (decorationEvent j k B)

noncomputable def BranchingProcess.decorationMass {J N : ℕ} (θ : Offspring J) (j k : ℕ) (B : ℕ → Set (Word N → ℕ)) : ENNReal

The weight of a decoration: the count law tilted by the survival pattern, normalised by survival, times one bush mass per dying child.

Equations

• One or more equations did not get rendered due to their size.

The joint root step

theorem BranchingProcess.sampleMeasure_root_decorated {J N : ℕ} (θ : Offspring J) (hJN : J ≤ N) (hq : θ.extinction < 1) (hq0 : 0 < θ.extinction) {j : ℕ} (hj : j ≤ N) (k : ℕ) {A B : ℕ → Set (Word N → ℕ)} (hA : ∀ (m : ℕ), MeasurableSet (A m)) (hB : ∀ (m : ℕ), MeasurableSet (B m)) : (sampleMeasure θ) ({c : Word N → ℕ | c [] = j} ∩ {c : Word N → ℕ | skeletonDegree c = k} ∩ {c : Word N → ℕ | ∀ m < k, bushAt c m ∈ A m} ∩ {c : Word N → ℕ | ∀ m < j - k, dyingAt c m ∈ B m}) = (ENNReal.ofReal (θ.mass j * ↑(j.choose k) * (1 - θ.extinction) ^ k * θ.extinction ^ (j - k)) * ∏ m ∈ Finset.range k, (survivalMeasure θ) (A m)) * ∏ m ∈ Finset.range (j - k), (bushMeasure θ) (B m)

The mass of a root count and survivor count with both families of subtrees constrained by rank: the survival patterns are summed, each contributing the mass of sampleMeasure_root_joint, the dying product freed of the pattern by the rank re-indexing.

theorem BranchingProcess.survivalMeasure_root_decorated {J N : ℕ} (θ : Offspring J) (hJN : J ≤ N) (hq : θ.extinction < 1) (hq0 : 0 < θ.extinction) {j k : ℕ} (hj : j ≤ N) (hk : k ≠ 0) {A B : ℕ → Set (Word N → ℕ)} (hA : ∀ (m : ℕ), MeasurableSet (A m)) (hB : ∀ (m : ℕ), MeasurableSet (B m)) : (survivalMeasure θ) (decorationEvent j k B ∩ {c : Word N → ℕ | ∀ m < k, bushAt c m ∈ A m}) = decorationMass θ j k B * ∏ m ∈ Finset.range k, (survivalMeasure θ) (A m)

The joint root step under the conditioned law: the decoration of the root carries the weight decorationMass, and the surviving subtrees are independent conditioned samples.

A prefix-closed set of addresses, decomposed at the root

noncomputable def BranchingProcess.consSub {N : ℕ} (i : Fin N) (F : Finset (Word N)) : Finset (Word N)

The addresses continuing a first letter.

Equations

• BranchingProcess.consSub i F = F.preimage (fun (x : BranchingProcess.Word N) => i :: x) ⋯

@[simp]

theorem BranchingProcess.mem_consSub {N : ℕ} {i : Fin N} {F : Finset (Word N)} {u : Word N} : u ∈ consSub i F ↔ i :: u ∈ F

theorem BranchingProcess.finset_cons_decomp {N : ℕ} [DecidableEq (Word N)] {F : Finset (Word N)} (h : [] ∈ F) : F = insert [] (Finset.univ.biUnion fun (i : Fin N) => Finset.image (fun (x : List (Fin N)) => i :: x) (consSub i F))

A prefix-closed finite set of addresses containing the root is the root together with its continuations.

theorem BranchingProcess.prod_cons_decomp {N : ℕ} {M : Type u_1} [CommMonoid M] {F : Finset (Word N)} (h : [] ∈ F) (g : Word N → M) : ∏ u ∈ F, g u = g [] * ∏ i : Fin N, ∏ u ∈ consSub i F, g (i :: u)

The product over a prefix-closed finite set of addresses, decomposed at the root.

The joint Harris decomposition

theorem BranchingProcess.survivalMeasure_decorations {J N : ℕ} (θ : Offspring J) (hJN : J ≤ N) (hq : θ.extinction < 1) (hq0 : 0 < θ.extinction) (n : ℕ) (F : Finset (Word N)) : (∀ v ∈ F, List.length v ≤ n) → (∀ v ∈ F, ∀ (p : Word N), p <+: v → p ∈ F) → ∀ (j k : Word N → ℕ) (B : Word N → ℕ → Set (Word N → ℕ)), (∀ u ∈ F, j u ≤ N) → (∀ u ∈ F, k u ≠ 0) → (∀ u ∈ F, ∀ (i : Fin N), u ++ [i] ∈ F → ↑i < k u) → (∀ (u : Word N) (m : ℕ), MeasurableSet (B u m)) → (survivalMeasure θ) (⋂ u ∈ F, {c : Word N → ℕ | skelSub c u ∈ decorationEvent (j u) (k u) (B u)}) = ∏ u ∈ F, decorationMass θ (j u) (k u) (B u)

The joint Harris decomposition. Conditioned on survival, probe the skeleton on a finite prefix-closed set of skeleton addresses, prescribing at each probed vertex its offspring count, its number of surviving children, and constraints on its dying subtrees. The mass factorises into one decorationMass per probed vertex: the decorations are independent, and each carries its dying subtrees as independent conjugate samples. The letters of an address name surviving children, which is the compatibility hypothesis hcomp.

The skeleton degree pattern

Marginalising the offspring counts and the dying subtrees out of the joint decomposition leaves the reduced-law half of the decomposition at general bounded support in its probabilistic form: probed on a finite prefix-closed set of skeleton addresses, the skeleton degrees are independent with the reduced law.

theorem BranchingProcess.skelSub_root_cases {N : ℕ} (c : Word N → ℕ) (u : Word N) : (∃ (v : Word N), skelSub c u [] = c v) ∨ skelSub c u [] = 0

The root count of a skeleton subfield is a coordinate of the field, or zero.

theorem BranchingProcess.survivalMeasure_coord_gt {J N : ℕ} (θ : Offspring J) (hJN : J ≤ N) (v : Word N) : (survivalMeasure θ) {c : Word N → ℕ | N < c v} = 0

Coordinates above the support bound are null under the conditioned law.

theorem BranchingProcess.survivalMeasure_skelSub_root_gt {J N : ℕ} (θ : Offspring J) (hJN : J ≤ N) (u : Word N) : (survivalMeasure θ) {c : Word N → ℕ | N < skelSub c u []} = 0

A skeleton subfield with root count above the support bound is null.

theorem BranchingProcess.survivalMeasure_skelField_pattern {J N : ℕ} (θ : Offspring J) (hJN : J ≤ N) (hq : θ.extinction < 1) (hq0 : 0 < θ.extinction) (n : ℕ) (F : Finset (Word N)) (hlen : ∀ v ∈ F, List.length v ≤ n) (hpc : ∀ v ∈ F, ∀ (p : Word N), p <+: v → p ∈ F) (k : Word N → ℕ) (hk : ∀ u ∈ F, k u ≠ 0) (hcomp : ∀ u ∈ F, ∀ (i : Fin N), u ++ [i] ∈ F → ↑i < k u) : (survivalMeasure θ) (⋂ u ∈ F, {c : Word N → ℕ | skeletonDegree (skelSub c u) = k u}) = ∏ u ∈ F, ENNReal.ofReal (θ.skeletonWeight (k u))

The skeleton degree pattern, the Harris decomposition at general bounded support in its probabilistic form: probed on a finite prefix-closed set of skeleton addresses whose letters name surviving children, the skeleton degrees are independent, each with the reduced law.

The decorations as laws on trees

theorem BranchingProcess.bushMeasure_sample_preimage {J N : ℕ} (θ : Offspring J) (hJN : J ≤ N) (hq0 : 0 < θ.extinction) {𝒯 : Set (Subtree N)} (h𝒯 : MeasurableSet 𝒯) : (bushMeasure θ) (sample ⁻¹' 𝒯) = (treeLaw (θ.conjugate hq0)) 𝒯

A dying subtree probed through its sampled tree carries the conjugate tree law.

theorem BranchingProcess.survivalMeasure_decorations_treeLaw {J N : ℕ} (θ : Offspring J) (hJN : J ≤ N) (hq : θ.extinction < 1) (hq0 : 0 < θ.extinction) (n : ℕ) (F : Finset (Word N)) (hlen : ∀ v ∈ F, List.length v ≤ n) (hpc : ∀ v ∈ F, ∀ (p : Word N), p <+: v → p ∈ F) (j k : Word N → ℕ) (𝒯 : Word N → ℕ → Set (Subtree N)) (hj : ∀ u ∈ F, j u ≤ N) (hk : ∀ u ∈ F, k u ≠ 0) (hcomp : ∀ u ∈ F, ∀ (i : Fin N), u ++ [i] ∈ F → ↑i < k u) (h𝒯 : ∀ (u : Word N) (m : ℕ), MeasurableSet (𝒯 u m)) : (survivalMeasure θ) (⋂ u ∈ F, {c : Word N → ℕ | skelSub c u ∈ decorationEvent (j u) (k u) fun (m : ℕ) => sample ⁻¹' 𝒯 u m}) = ∏ u ∈ F, ENNReal.ofReal (θ.mass (j u) * ↑((j u).choose (k u)) * (1 - θ.extinction) ^ k u * θ.extinction ^ (j u - k u) / (1 - θ.extinction)) * ∏ m ∈ Finset.range (j u - k u), (treeLaw (θ.conjugate hq0)) (𝒯 u m)

The joint Harris decomposition, as an identity of laws on trees. Conditioned on survival and conditionally on the skeleton, probed on a finite prefix-closed set of skeleton addresses with its degrees, the decorations are independent, and the dying subtrees of each probed vertex are independent Galton-Watson trees with the conjugate law.