The offspring law as a probability mass function

noncomputable def BranchingProcess.Offspring.toPMF {J : ℕ} (θ : Offspring J) : PMF ℕ

The offspring law read as a probability mass function on ℕ: the real masses θ_j transported to ℝ≥0∞. Summability is the finite sum θ.total, the masses above J vanishing.

Equations

• θ.toPMF = ⟨fun (j : ℕ) => ENNReal.ofReal (θ.mass j), ⋯⟩

@[simp]

theorem BranchingProcess.Offspring.toPMF_apply {J : ℕ} (θ : Offspring J) (j : ℕ) : θ.toPMF j = ENNReal.ofReal (θ.mass j)

The mass function of toPMF is the offspring law.

noncomputable def BranchingProcess.Offspring.law {J : ℕ} (θ : Offspring J) : MeasureTheory.Measure ℕ

The one-vertex law: the measure on ℕ with mass θ_j at j.

Equations

• θ.law = θ.toPMF.toMeasure

instance BranchingProcess.Offspring.isProbabilityMeasure_law {J : ℕ} (θ : Offspring J) : MeasureTheory.IsProbabilityMeasure θ.law

@[simp]

theorem BranchingProcess.Offspring.law_singleton {J : ℕ} (θ : Offspring J) (k : ℕ) : θ.law {k} = ENNReal.ofReal (θ.mass k)

The one-vertex law gives mass θ_k to {k}.

The iterates of the generating function

noncomputable def BranchingProcess.Offspring.genIter {J : ℕ} (θ : Offspring J) (n : ℕ) : ℝ

The iterates f^n(0) of the generating function at zero: the probability that the tree dies out by generation n.

Equations

• θ.genIter n = θ.gen^[n] 0

@[simp]

theorem BranchingProcess.Offspring.genIter_zero {J : ℕ} (θ : Offspring J) : θ.genIter 0 = 0

theorem BranchingProcess.Offspring.genIter_succ {J : ℕ} (θ : Offspring J) (n : ℕ) : θ.genIter (n + 1) = θ.gen (θ.genIter n)

One step of the recursion q_{n+1} = f(q_n).

theorem BranchingProcess.Offspring.genIter_mem {J : ℕ} (θ : Offspring J) (n : ℕ) : θ.genIter n ∈ Set.Icc 0 1

The iterates stay in [0,1], where f maps [0,1] to itself.

theorem BranchingProcess.Offspring.genIter_nonneg {J : ℕ} (θ : Offspring J) (n : ℕ) : 0 ≤ θ.genIter n

theorem BranchingProcess.Offspring.genIter_le_one {J : ℕ} (θ : Offspring J) (n : ℕ) : θ.genIter n ≤ 1

theorem BranchingProcess.Offspring.genIter_mono {J : ℕ} (θ : Offspring J) : Monotone θ.genIter

The iterates increase, f being monotone and f(0) ≥ 0.

theorem BranchingProcess.Offspring.genIter_le_extinction {J : ℕ} (θ : Offspring J) (n : ℕ) : θ.genIter n ≤ θ.extinction

Every iterate lies below the extinction probability, that being a fixed point of f.

theorem BranchingProcess.Offspring.tendsto_genIter {J : ℕ} (θ : Offspring J) : Filter.Tendsto θ.genIter Filter.atTop (nhds θ.extinction)

The iterates converge to the extinction probability. They increase, so they converge; the limit is a fixed point of f in [0,1] by continuity, hence at least q by minimality, and at most q termwise.

The law of the offspring field

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

The law of the offspring field. The i.i.d. field on Word N → ℕ whose coordinates are independent with the offspring law θ; the sample of Sample under this measure is the Galton-Watson tree of θ.

Equations

• BranchingProcess.sampleMeasure θ = BranchingProcess.fieldMeasure θ.law

instance BranchingProcess.isProbabilityMeasure_sampleMeasure {J N : ℕ} (θ : Offspring J) : MeasureTheory.IsProbabilityMeasure (sampleMeasure θ)

theorem BranchingProcess.sampleMeasure_coord {J N : ℕ} (θ : Offspring J) (v : Word N) (k : ℕ) : (sampleMeasure θ) {c : Word N → ℕ | c v = k} = ENNReal.ofReal (θ.mass k)

Each vertex has the offspring law: the coordinate at v takes the value k with probability θ_k.

Measurability of the events

theorem BranchingProcess.measurableSet_mem_sample {N : ℕ} (v : Word N) : MeasurableSet {c : Word N → ℕ | v ∈ sample c}

Membership of a fixed word in the sample is a measurable event: it is the finite intersection, one condition per letter, of conditions on single coordinates, and ℕ is discrete.

Extinction as the exhaustion by empty generations

def BranchingProcess.noLevel {N : ℕ} (n : ℕ) : Set (Word N → ℕ)

The event that generation n is empty: no word of length n lies in the sample. These events increase to extinction.

Equations

• BranchingProcess.noLevel n = {c : BranchingProcess.Word N → ℕ | ∀ (v : BranchingProcess.Word N), List.length v = n → v ∉ BranchingProcess.sample c}

theorem BranchingProcess.mem_noLevel_iff {N : ℕ} {c : Word N → ℕ} {n : ℕ} : c ∈ noLevel n ↔ ∀ (v : Word N), List.length v = n → v ∉ sample c

Membership in noLevel, unfolded.

theorem BranchingProcess.finite_sample_of_noLevel {N : ℕ} (n : ℕ) (c : Word N → ℕ) : c ∈ noLevel n → (↑(sample c)).Finite

An empty generation kills the sample. A sample missing a whole generation is finite: the recursion runs down the N subtrees at the root.

theorem BranchingProcess.survives_iff_forall_level {N : ℕ} {c : Word N → ℕ} : Survives c ↔ ∀ (n : ℕ), ∃ (v : Word N), List.length v = n ∧ v ∈ sample c

Survival is reaching every generation.

theorem BranchingProcess.not_survives_iff_exists_noLevel {N : ℕ} {c : Word N → ℕ} : ¬Survives c ↔ ∃ (n : ℕ), c ∈ noLevel n

Extinction is the failure of some generation to be reached.

theorem BranchingProcess.noLevel_mono {N : ℕ} : Monotone noLevel

The empty generations increase: a missing generation makes every later one missing, the sample being prefix-closed.

theorem BranchingProcess.notSurvives_eq_iUnion {N : ℕ} : {c : Word N → ℕ | ¬Survives c} = ⋃ (n : ℕ), noLevel n

Extinction is the union of the empty-generation events.

theorem BranchingProcess.measurableSet_noLevel {N : ℕ} (n : ℕ) : MeasurableSet (noLevel n)

The empty-generation event is measurable: a countable intersection over the words of the generation, Word N being countable.

theorem BranchingProcess.measurableSet_survives {N : ℕ} : MeasurableSet {c : Word N → ℕ | Survives c}

Survival is a measurable event.

The splitting of the field at the root

def BranchingProcess.Branch (N : ℕ) : Option (Fin N) → Type

The index of the splitting of the ambient tree at the root: none names the root, which carries a single coordinate, and some j the copy of the tree hanging under the letter j.

Equations

• BranchingProcess.Branch N none = Unit
• BranchingProcess.Branch N (some val) = BranchingProcess.Word N

def BranchingProcess.rootSplit {N : ℕ} (i : Option (Fin N)) : Branch N i → Word N

The splitting bijection: a word is either the root or a letter followed by a word.

Equations

• BranchingProcess.rootSplit none x_2 = []
• BranchingProcess.rootSplit (some j) w = j :: w

def BranchingProcess.rootIdx {N : ℕ} : Branch N none

The single coordinate carried by the root block.

Equations

• BranchingProcess.rootIdx = ()

@[simp]

theorem BranchingProcess.rootSplit_none {N : ℕ} (u : Branch N none) : rootSplit none u = []

@[simp]

theorem BranchingProcess.rootSplit_some {N : ℕ} (j : Fin N) (w : Branch N (some j)) : rootSplit (some j) w = j :: w

theorem BranchingProcess.injective_rootSplit {N : ℕ} : Function.Injective fun (p : (i : Option (Fin N)) × Branch N i) => rootSplit p.fst p.snd

The splitting is injective, [] being the one word that is not a letter followed by a word.

def BranchingProcess.split {N : ℕ} (c : Word N → ℕ) (i : Option (Fin N)) : Branch N i → ℕ

The splitting map: the offspring count at the root together with the offspring fields of the N subtrees at the children of the root.

Equations

• BranchingProcess.split c i x = c (BranchingProcess.rootSplit i x)

@[simp]

theorem BranchingProcess.split_none {N : ℕ} (c : Word N → ℕ) (u : Branch N none) : split c none u = c []

@[simp]

theorem BranchingProcess.split_some {N : ℕ} (c : Word N → ℕ) (j : Fin N) (w : Branch N (some j)) : split c (some j) w = c (j :: w)

theorem BranchingProcess.measurable_split {N : ℕ} : Measurable split

theorem BranchingProcess.map_split {J N : ℕ} (θ : Offspring J) : MeasureTheory.Measure.map split (sampleMeasure θ) = MeasureTheory.Measure.infinitePi fun (i : Option (Fin N)) => MeasureTheory.Measure.infinitePi fun (x : Branch N i) => θ.law

The branching property of the law. Under the splitting the field becomes the offspring count at the root together with N independent copies of itself, one for each letter.

One step of the recursion

def BranchingProcess.levelBox {N : ℕ} (n k : ℕ) (i : Option (Fin N)) : Set (Branch N i → ℕ)

The product event at the root: the root has k children, and generation n is empty in the subtree hanging under each of the first k of them.

Equations

• BranchingProcess.levelBox n k none = {u : BranchingProcess.Branch N none → ℕ | u BranchingProcess.rootIdx = k}
• BranchingProcess.levelBox n k (some val) = if ↑val < k then BranchingProcess.noLevel n else Set.univ

@[simp]

theorem BranchingProcess.levelBox_none {N : ℕ} (n k : ℕ) : levelBox n k none = {u : Branch N none → ℕ | u rootIdx = k}

@[simp]

theorem BranchingProcess.levelBox_some {N : ℕ} (n k : ℕ) (j : Fin N) : levelBox n k (some j) = if ↑j < k then noLevel n else Set.univ

theorem BranchingProcess.measurableSet_levelBox {N : ℕ} (n k : ℕ) (i : Option (Fin N)) : MeasurableSet (levelBox n k i)

theorem BranchingProcess.split_preimage_levelBox {N : ℕ} (n k : ℕ) : split ⁻¹' Set.univ.pi (levelBox n k) = {c : Word N → ℕ | c [] = k} ∩ noLevel (n + 1)

The product event is the one-step event. The sample misses generation n+1 and has k children at the root exactly when it has k children at the root and each of the corresponding subtrees misses generation n.

theorem BranchingProcess.infinitePi_levelBox_none {J N : ℕ} (θ : Offspring J) (n k : ℕ) : (MeasureTheory.Measure.infinitePi fun (x : Branch N none) => θ.law) (levelBox n k none) = ENNReal.ofReal (θ.mass k)

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

theorem BranchingProcess.infinitePi_branch_some {J N : ℕ} (θ : Offspring J) (j : Fin N) (s : Set (Word N → ℕ)) : (MeasureTheory.Measure.infinitePi fun (x : Branch N (some j)) => θ.law) s = (sampleMeasure θ) s

A child factor of the product is a copy of the field measure.

theorem BranchingProcess.prod_ite_lt {N : ℕ} (x : ENNReal) {k : ℕ} (hk : k ≤ N) : (∏ j : Fin N, if ↑j < k then x else 1) = x ^ k

The product of the child factors: only the first k letters contribute.

theorem BranchingProcess.sampleMeasure_root_noLevel {J N : ℕ} (θ : Offspring J) (n : ℕ) {k : ℕ} (hk : k ≤ N) : (sampleMeasure θ) ({c : Word N → ℕ | c [] = k} ∩ noLevel (n + 1)) = ENNReal.ofReal (θ.mass k) * (sampleMeasure θ) (noLevel n) ^ k

The one-step measure. The event that the root has k children and generation n+1 is empty has probability θ_k q_n^k.

The law of extinction

theorem BranchingProcess.sampleMeasure_noLevel_succ {J N : ℕ} (θ : Offspring J) (hJN : J ≤ N) (n : ℕ) : (sampleMeasure θ) (noLevel (n + 1)) = ∑ k ∈ Finset.range (J + 1), ENNReal.ofReal (θ.mass k) * (sampleMeasure θ) (noLevel n) ^ k

The recursion. Splitting at the root, the probability that generation n+1 is empty is the generating function evaluated at the probability that generation n is empty. The bound J ≤ N makes the ambient alphabet wide enough to carry the whole offspring law.

theorem BranchingProcess.sampleMeasure_noLevel {J N : ℕ} (θ : Offspring J) (hJN : J ≤ N) (n : ℕ) : (sampleMeasure θ) (noLevel n) = ENNReal.ofReal (θ.genIter n)

The masses of the empty-generation events are the iterates of the generating function: the sample dies out by generation n with probability f^n(0).

theorem BranchingProcess.sampleMeasure_not_survives {J N : ℕ} (θ : Offspring J) (hJN : J ≤ N) : (sampleMeasure θ) {c : Word N → ℕ | ¬Survives c} = ENNReal.ofReal θ.extinction

The extinction probability is the probability of extinction. The events that a generation is empty increase to extinction, and their masses are the iterates f^n(0), which converge to the least fixed point q of f.

theorem BranchingProcess.toReal_sampleMeasure_not_survives {J N : ℕ} (θ : Offspring J) (hJN : J ≤ N) : ((sampleMeasure θ) {c : Word N → ℕ | ¬Survives c}).toReal = θ.extinction

The real form of the theorem: the sample dies out with probability q.

theorem BranchingProcess.sampleMeasure_survives {J N : ℕ} (θ : Offspring J) (hJN : J ≤ N) : (sampleMeasure θ) {c : Word N → ℕ | Survives c} = ENNReal.ofReal (1 - θ.extinction)

The survival probability is 1 - q; it is positive exactly for a supercritical law, by extinction_lt_one_of_supercritical.

theorem BranchingProcess.gen_extinctionProb {J N : ℕ} (θ : Offspring J) (hJN : J ≤ N) : θ.gen ((sampleMeasure θ) {c : Word N → ℕ | ¬Survives c}).toReal = ((sampleMeasure θ) {c : Word N → ℕ | ¬Survives c}).toReal

The probability of extinction is a fixed point of the generating function, the identity the classical recursion is read off from.