Fields that agree on a tree

def BranchingProcess.agreeOn {N : ℕ} (e : Word N → ℕ) : Set (Word N → ℕ)

The event that a field agrees with e at every vertex of the sample of e; the coordinates off that tree are left free.

Equations

• BranchingProcess.agreeOn e = {c : BranchingProcess.Word N → ℕ | ∀ v ∈ BranchingProcess.sample e, c v = e v}

@[simp]

theorem BranchingProcess.mem_agreeOn {N : ℕ} {e c : Word N → ℕ} : c ∈ agreeOn e ↔ ∀ v ∈ sample e, c v = e v

theorem BranchingProcess.sample_eq_of_agreeOn {N : ℕ} {e c : Word N → ℕ} (h : c ∈ agreeOn e) : ↑(sample c) = ↑(sample e)

Agreement on a tree cuts out that tree. Whether a child of a vertex of the sample of e is kept is decided by the offspring count there, and the two fields carry the same one; the induction on the word never leaves the tree.

theorem BranchingProcess.agreeOn_subset {N : ℕ} (e : Word N → ℕ) : agreeOn e ⊆ {c : Word N → ℕ | ↑(sample c) = ↑(sample e)}

The agreement event lies inside the event that the sample is the prescribed tree.

theorem BranchingProcess.not_survives_of_sample_eq {N : ℕ} {e c : Word N → ℕ} (hfin : (↑(sample e)).Finite) (h : ↑(sample c) = ↑(sample e)) : ¬Survives c

A field cutting out a finite tree dies out.

The point mass of a finite tree

theorem BranchingProcess.sampleMeasure_agreeOn {J N : ℕ} (θ : Offspring J) {e : Word N → ℕ} (hfin : (↑(sample e)).Finite) : (sampleMeasure θ) (agreeOn e) = ∏ v ∈ hfin.toFinset, ENNReal.ofReal (θ.mass (e v))

The point mass of a finite tree. A field agrees with e at the vertices of the sample of e with probability the product of the offspring weights along that tree: the agreement is a cylinder event over those finitely many coordinates, and the coordinates are independent.

theorem BranchingProcess.ofReal_pow_le_sampleMeasure_agreeOn {J N : ℕ} (θ : Offspring J) {p : ℝ} {e : Word N → ℕ} (hfin : (↑(sample e)).Finite) (hmass : ∀ v ∈ sample e, p ≤ θ.mass (e v)) : ENNReal.ofReal p ^ (↑(sample e)).ncard ≤ (sampleMeasure θ) (agreeOn e)

One factor per vertex. A finite tree whose offspring weights are all at least p has point mass at least p to its number of vertices.

theorem BranchingProcess.ofReal_pow_le_sampleMeasure_sample_eq {J N : ℕ} (θ : Offspring J) {p : ℝ} {e : Word N → ℕ} (hfin : (↑(sample e)).Finite) (hmass : ∀ v ∈ sample e, p ≤ θ.mass (e v)) : ENNReal.ofReal p ^ (↑(sample e)).ncard ≤ (sampleMeasure θ) {c : Word N → ℕ | ↑(sample c) = ↑(sample e)}

The point-mass bound under the sample law: the sample is a prescribed finite tree with probability at least p to its number of vertices.

theorem BranchingProcess.sampleMeasure_le_bushMeasure {J N : ℕ} (θ : Offspring J) {S : Set (Word N → ℕ)} (hS : S ⊆ {c : Word N → ℕ | ¬Survives c}) : (sampleMeasure θ) S ≤ (bushMeasure θ) S

Conditioning on extinction only increases the mass of an event carried by extinction.

theorem BranchingProcess.ofReal_pow_le_bushMeasure_sample_eq {J N : ℕ} (θ : Offspring J) {p : ℝ} {e : Word N → ℕ} (hfin : (↑(sample e)).Finite) (hmass : ∀ v ∈ sample e, p ≤ θ.mass (e v)) : ENNReal.ofReal p ^ (↑(sample e)).ncard ≤ (bushMeasure θ) {c : Word N → ℕ | ↑(sample c) = ↑(sample e)}

The point-mass bound under the law of a bush: a bush is a prescribed finite tree with probability at least p to its number of vertices.

The truncated progeny

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

A child of the root of a sample, unfolded.

def BranchingProcess.progenyTree {N : ℕ} : ℕ → (Word N → ℕ) → Finset (Word N)

The vertices of the sample within the first k generations: the root together with the truncations of the subtrees at the children of the root, each one generation shorter.

Equations

• One or more equations did not get rendered due to their size.
• BranchingProcess.progenyTree 0 x✝ = ∅

theorem BranchingProcess.mem_progenyTree {N : ℕ} (k : ℕ) (c : Word N → ℕ) (v : Word N) : v ∈ progenyTree k c ↔ v ∈ sample c ∧ List.length v < k

The truncation is the sample cut at a generation.

def BranchingProcess.progeny {N : ℕ} (k : ℕ) (c : Word N → ℕ) : ℕ

The truncated progeny: the number of vertices of the sample within the first k generations.

Equations

• BranchingProcess.progeny k c = (BranchingProcess.progenyTree k c).card

@[simp]

theorem BranchingProcess.progeny_zero {N : ℕ} (c : Word N → ℕ) : progeny 0 c = 0

theorem BranchingProcess.progeny_succ {N : ℕ} (k : ℕ) (c : Word N → ℕ) : progeny (k + 1) c = 1 + ∑ i ∈ childSet N (c []), progeny k fun (w : Word N) => c (i :: w)

The recursion at the root: the root, and the truncations of the subtrees at its children. This is the identity the progeny equation is read off.

theorem BranchingProcess.progenyTree_subset {N k l : ℕ} (h : k ≤ l) (c : Word N → ℕ) : progenyTree k c ⊆ progenyTree l c

The truncations increase with the generation.

theorem BranchingProcess.progeny_mono {N : ℕ} (c : Word N → ℕ) : Monotone fun (k : ℕ) => progeny k c

The truncated progeny increases with the generation.

theorem BranchingProcess.progeny_eq_ncard {N : ℕ} {c : Word N → ℕ} {k : ℕ} (h : ∀ u ∈ sample c, u.length < k) : progeny k c = (↑(sample c)).ncard

The truncation stops at the height: once the fuel exceeds the length of every vertex, the truncated progeny is the number of vertices of the sample.

theorem BranchingProcess.exists_progeny_eq_ncard {N : ℕ} {c : Word N → ℕ} (hfin : (↑(sample c)).Finite) : ∃ (k : ℕ), progeny k c = (↑(sample c)).ncard

A finite sample is exhausted by its truncations.

theorem BranchingProcess.measurable_progeny {N : ℕ} (k : ℕ) : Measurable (progeny k)

The truncated progeny is a measurable function of the field: it reads finitely many coordinates, one recursion step at a time.

The blocks of the splitting

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

The law of one block of the splitting, read off map_split.

theorem BranchingProcess.map_shift {J N : ℕ} (θ : Offspring J) (i : Fin N) : MeasureTheory.Measure.map (fun (c : Word N → ℕ) (w : List (Fin N)) => c (i :: w)) (sampleMeasure θ) = sampleMeasure θ

The shift to a child is measure preserving: the field of a subtree at the root is a copy of the whole field.

theorem BranchingProcess.iIndepFun_split {J N : ℕ} (θ : Offspring J) : ProbabilityTheory.iIndepFun (fun (i : Option (Fin N)) (c : Word N → ℕ) => split c i) (sampleMeasure θ)

The blocks of the splitting are independent: the offspring count at the root and the fields of the N subtrees hanging off it.

The progeny recursion

theorem BranchingProcess.measurableSet_rootIdx_eq {N : ℕ} (j : ℕ) : MeasurableSet {u : Branch N none → ℕ | u rootIdx = j}

The offspring count at the root is a measurable coordinate of the root block.

noncomputable def BranchingProcess.progenyFactor {N : ℕ} (s : ENNReal) (k j : ℕ) (i : Option (Fin N)) : (Branch N i → ℕ) → ENNReal

The factors of the one-step product for the truncated progeny: the root block carries the offspring count j together with one power of s, and each child block below j the truncation one generation shorter.

Equations

• BranchingProcess.progenyFactor s k j none = {u : BranchingProcess.Branch N none → ℕ | u BranchingProcess.rootIdx = j}.indicator fun (x : BranchingProcess.Branch N none → ℕ) => s
• BranchingProcess.progenyFactor s k j (some i) = fun (d : BranchingProcess.Branch N (some i) → ℕ) => if ↑i < j then s ^ BranchingProcess.progeny k d else 1

@[simp]

theorem BranchingProcess.progenyFactor_none {N : ℕ} (s : ENNReal) (k j : ℕ) : progenyFactor s k j none = {u : Branch N none → ℕ | u rootIdx = j}.indicator fun (x : Branch N none → ℕ) => s

@[simp]

theorem BranchingProcess.progenyFactor_some {N : ℕ} (s : ENNReal) (k j : ℕ) (i : Fin N) : progenyFactor s k j (some i) = fun (d : Word N → ℕ) => if ↑i < j then s ^ progeny k d else 1

theorem BranchingProcess.measurable_progenyFactor {N : ℕ} (s : ENNReal) (k j : ℕ) (i : Option (Fin N)) : Measurable (progenyFactor s k j i)

theorem BranchingProcess.progenyFactor_none_split {N : ℕ} (s : ENNReal) (k j : ℕ) (c : Word N → ℕ) : progenyFactor s k j none (split c none) = {c : Word N → ℕ | c [] = j}.indicator (fun (x : Word N → ℕ) => s) c

The root factor is the indicator of the offspring count at the root.

theorem BranchingProcess.prod_progenyFactor {N : ℕ} (s : ENNReal) (k j : ℕ) (c : Word N → ℕ) : ∏ i : Option (Fin N), progenyFactor s k j i (split c i) = {c : Word N → ℕ | c [] = j}.indicator (fun (c : Word N → ℕ) => s ^ progeny (k + 1) c) c

The one-step product. On the event that the root has j children the power of the truncated progeny is the product over the blocks of the splitting of the factors, one power of s for the root and the truncation of each of its subtrees.

theorem BranchingProcess.lintegral_progeny_root {J N : ℕ} (θ : Offspring J) (s : ENNReal) (k : ℕ) {j : ℕ} (hj : j ≤ N) : ∫⁻ (c : Word N → ℕ) in {c : Word N → ℕ | c [] = j}, s ^ progeny (k + 1) c ∂sampleMeasure θ = s * ENNReal.ofReal (θ.mass j) * (∫⁻ (c : Word N → ℕ), s ^ progeny k c ∂sampleMeasure θ) ^ j

One step of the progeny recursion at a fixed offspring count. The root has j children and its truncation one generation longer has moment s θ_j times the j-th power of the truncated moment: the blocks of the splitting are independent.

theorem BranchingProcess.lintegral_pow_progeny_succ {J N : ℕ} (θ : Offspring J) (hJN : J ≤ N) (s : ENNReal) (k : ℕ) : ∫⁻ (c : Word N → ℕ), s ^ progeny (k + 1) c ∂sampleMeasure θ = ∑ j ∈ Finset.range (J + 1), s * ENNReal.ofReal (θ.mass j) * (∫⁻ (c : Word N → ℕ), s ^ progeny k c ∂sampleMeasure θ) ^ j

The progeny recursion F_{k+1}(s) = s f(F_k(s)): summing the one-step masses over the offspring count at the root.

The moment of a truncation

theorem BranchingProcess.lintegral_pow_progeny_le {J N : ℕ} (θ : Offspring J) (hJN : J ≤ N) {σ y : ℝ} (hσ : 0 ≤ σ) (hy : 1 ≤ y) (hfix : σ * θ.gen y = y) (k : ℕ) : ∫⁻ (c : Word N → ℕ), ENNReal.ofReal σ ^ progeny k c ∂sampleMeasure θ ≤ ENNReal.ofReal y

The truncated moments are bounded by a fixed point of the progeny equation. The recursion turns the bound at one generation into the same bound at the next, the fixed point being exactly what the generating function returns.

The progeny equation

theorem BranchingProcess.Offspring.exists_gen_lt_self {J : ℕ} (θ : Offspring J) (h : θ.IsSubcritical) : ∃ (y : ℝ), 1 < y ∧ θ.gen y < y

A subcritical generating function drops below the diagonal. The difference quotient of one_sub_gen takes the value m < 1 at one, so it stays below one nearby, and above one that reads f(y) < y.

theorem BranchingProcess.Offspring.exists_progeny_fixedPoint {J : ℕ} (θ : Offspring J) (h : θ.IsSubcritical) : ∃ (s : ℝ) (y : ℝ), 1 < s ∧ 1 < y ∧ s * θ.gen y = y

The progeny equation has a fixed point above one. A subcritical law has y > 1 with f(y) < y, and then s = y / f(y) exceeds one and solves s f(y) = y.

The exponential moment of the total progeny

theorem BranchingProcess.lintegral_pow_ncard_le {J N : ℕ} (θ : Offspring J) (hJN : J ≤ N) {σ y : ℝ} (hσ : 1 ≤ σ) (hy : 1 ≤ y) (hfix : σ * θ.gen y = y) : ∫⁻ (c : Word N → ℕ), ENNReal.ofReal σ ^ (↑(sample c)).ncard ∂sampleMeasure θ ≤ ENNReal.ofReal y

The exponential moment of the total progeny, at a fixed point of the progeny equation: the truncations exhaust a finite sample, so the monotone convergence theorem carries the uniform bound of lintegral_pow_progeny_le to the number of vertices.

theorem BranchingProcess.exists_exponential_moment {J N : ℕ} (θ : Offspring J) (hJN : J ≤ N) (h : θ.IsSubcritical) : ∃ (σ : ℝ), 1 < σ ∧ ∫⁻ (c : Word N → ℕ), ENNReal.ofReal σ ^ (↑(sample c)).ncard ∂sampleMeasure θ < ⊤

The total progeny of a subcritical law has an exponential moment. This is the size-tail input taken from the conjugate law: the number of vertices of a bush is exponentially integrable.

The number of vertices of a random tree

theorem BranchingProcess.measurableSet_subtree_eq {N : ℕ} (F : Finset (Word N)) : MeasurableSet {T : Subtree N | ↑T = ↑F}

A subtree is a prescribed finite set of words on a measurable event: it contains that set and nothing else.

theorem BranchingProcess.measurableSet_ncard_eq {N : ℕ} (n : ℕ) : MeasurableSet {T : Subtree N | (↑T).ncard = n}

The number of vertices is a random variable. A positive value is attained exactly on the countably many finite sets of words of that size, and the value zero on the complement of the others.

theorem BranchingProcess.measurable_pow_ncard {N : ℕ} (s : ENNReal) : Measurable fun (T : Subtree N) => s ^ (↑T).ncard

The power of the number of vertices is a measurable function of the tree.

The exponential moment of a bush

theorem BranchingProcess.lintegral_pow_ncard_bushMeasure_le {J N : ℕ} (θ : Offspring J) (hJN : J ≤ N) (hq0 : 0 < θ.extinction) {σ y : ℝ} (hσ : 1 ≤ σ) (hy : 1 ≤ y) (hfix : σ * (θ.conjugate hq0).gen y = y) : ∫⁻ (c : Word N → ℕ), ENNReal.ofReal σ ^ (↑(sample c)).ncard ∂bushMeasure θ ≤ ENNReal.ofReal y

The exponential moment of the size of a bush. A sample conditioned to die is a Galton-Watson tree with the conjugate law, so the moment of lintegral_pow_ncard_le at that law transports along bushTreeLaw_eq_treeLaw.

theorem BranchingProcess.exists_exponential_moment_bushMeasure {J N : ℕ} (θ : Offspring J) (hJN : J ≤ N) (hq0 : 0 < θ.extinction) (h : (θ.conjugate hq0).IsSubcritical) : ∃ (σ : ℝ), 1 < σ ∧ ∫⁻ (c : Word N → ℕ), ENNReal.ofReal σ ^ (↑(sample c)).ncard ∂bushMeasure θ < ⊤

The size of a bush has an exponential moment once the conjugate law is subcritical: the size-tail input taken from the bushes of the Harris decomposition.