structure BranchingProcess.Offspring (J : ℕ) : Type

An offspring distribution with support in {0,…,J}: the masses θ_0,…,θ_J of the number of children of a vertex.

• mass : ℕ → ℝ

  The mass function j ↦ θ_j.

• nonneg (j : ℕ) : 0 ≤ self.mass j

  Masses are nonnegative.

• vanishing (j : ℕ) : J < j → self.mass j = 0

  The support lies in {0,…,J}.

• total : ∑ j ∈ Finset.range (J + 1), self.mass j = 1

  The masses sum to one.

@[implicit_reducible]

instance BranchingProcess.instCoeFunOffspringForallNatReal {J : ℕ} : CoeFun (Offspring J) fun (x : Offspring J) => ℕ → ℝ

An offspring law acts as its mass function, so θ j is the mass of j.

Equations

• BranchingProcess.instCoeFunOffspringForallNatReal = { coe := BranchingProcess.Offspring.mass }

The law

theorem BranchingProcess.Offspring.mass_le_one {J : ℕ} (θ : Offspring J) (j : ℕ) : θ.mass j ≤ 1

Every mass is at most one.

The mean and the three regimes

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

The mean offspring number m = ∑_j j θ_j.

Equations

• θ.mean = ∑ j ∈ Finset.range (J + 1), ↑j * θ.mass j

def BranchingProcess.Offspring.IsSubcritical {J : ℕ} (θ : Offspring J) : Prop

A law is subcritical when its mean is below one.

Equations

• θ.IsSubcritical = (θ.mean < 1)

def BranchingProcess.Offspring.IsCritical {J : ℕ} (θ : Offspring J) : Prop

A law is critical when its mean is one.

Equations

• θ.IsCritical = (θ.mean = 1)

def BranchingProcess.Offspring.IsSupercritical {J : ℕ} (θ : Offspring J) : Prop

A law is supercritical when its mean exceeds one.

Equations

• θ.IsSupercritical = (1 < θ.mean)

The generating function

noncomputable def BranchingProcess.Offspring.gen {J : ℕ} (θ : Offspring J) (s : ℝ) : ℝ

The generating function f(s) = ∑_{j=0}^{J} θ_j s^j.

Equations

• θ.gen s = ∑ j ∈ Finset.range (J + 1), θ.mass j * s ^ j

@[simp]

theorem BranchingProcess.Offspring.gen_one {J : ℕ} (θ : Offspring J) : θ.gen 1 = 1

f(1) = 1: the masses sum to one.

@[simp]

theorem BranchingProcess.Offspring.gen_zero {J : ℕ} (θ : Offspring J) : θ.gen 0 = θ.mass 0

f(0) = θ_0: only the constant term survives.

theorem BranchingProcess.Offspring.gen_nonneg {J : ℕ} (θ : Offspring J) {s : ℝ} (hs : 0 ≤ s) : 0 ≤ θ.gen s

f is nonnegative on the nonnegative half-line.

theorem BranchingProcess.Offspring.gen_le_one {J : ℕ} (θ : Offspring J) {s : ℝ} (hs : s ∈ Set.Icc 0 1) : θ.gen s ≤ 1

f maps [0,1] into [0,1]; this is the upper half.

theorem BranchingProcess.Offspring.continuous_gen {J : ℕ} (θ : Offspring J) : Continuous θ.gen

f is a polynomial, hence continuous.

theorem BranchingProcess.Offspring.gen_mono {J : ℕ} (θ : Offspring J) {s t : ℝ} (hs : 0 ≤ s) (hst : s ≤ t) : θ.gen s ≤ θ.gen t

f is monotone on the nonnegative half-line, so in particular on [0,1].

noncomputable def BranchingProcess.Offspring.genDeriv {J : ℕ} (θ : Offspring J) (s : ℝ) : ℝ

The derivative f'(s) = ∑_{j=1}^{J} j θ_j s^{j-1}; the j = 0 term vanishes through the cast.

Equations

• θ.genDeriv s = ∑ j ∈ Finset.range (J + 1), ↑j * θ.mass j * s ^ (j - 1)

theorem BranchingProcess.Offspring.hasDerivAt_gen {J : ℕ} (θ : Offspring J) (s : ℝ) : HasDerivAt θ.gen (θ.genDeriv s) s

genDeriv is the derivative of the generating function.

theorem BranchingProcess.Offspring.genDeriv_one {J : ℕ} (θ : Offspring J) : θ.genDeriv 1 = θ.mean

f'(1) = m: the derivative at one is the mean.

The difference quotient at one

noncomputable def BranchingProcess.Offspring.genSlope {J : ℕ} (θ : Offspring J) (s : ℝ) : ℝ

The polynomial g(s) = ∑_j θ_j (1 + s + ⋯ + s^{j-1}), the difference quotient (1-f(s))/(1-s) cleared of its denominator.

Equations

• θ.genSlope s = ∑ j ∈ Finset.range (J + 1), θ.mass j * ∑ i ∈ Finset.range j, s ^ i

theorem BranchingProcess.Offspring.one_sub_gen {J : ℕ} (θ : Offspring J) (s : ℝ) : 1 - θ.gen s = (1 - s) * θ.genSlope s

1 - f(s) = (1-s) g(s), the geometric sum taken termwise.

theorem BranchingProcess.Offspring.genSlope_one {J : ℕ} (θ : Offspring J) : θ.genSlope 1 = θ.mean

g(1) = m: the difference quotient at one is the mean.

theorem BranchingProcess.Offspring.continuous_genSlope {J : ℕ} (θ : Offspring J) : Continuous θ.genSlope

g is a polynomial, hence continuous.

The extinction probability

def BranchingProcess.Offspring.fixedSet {J : ℕ} (θ : Offspring J) : Set ℝ

The fixed points of the generating function in [0,1].

Equations

• θ.fixedSet = {s : ℝ | s ∈ Set.Icc 0 1 ∧ θ.gen s = s}

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

The extinction probability q = inf {s ∈ [0,1] : f(s) = s}, the least fixed point of the generating function in [0,1].

Equations

• θ.extinction = sInf θ.fixedSet

theorem BranchingProcess.Offspring.one_mem_fixedSet {J : ℕ} (θ : Offspring J) : 1 ∈ θ.fixedSet

1 is a fixed point, so the set is nonempty.

theorem BranchingProcess.Offspring.fixedSet_nonempty {J : ℕ} (θ : Offspring J) : θ.fixedSet.Nonempty

The set of fixed points in [0,1] is nonempty.

theorem BranchingProcess.Offspring.bddBelow_fixedSet {J : ℕ} (θ : Offspring J) : BddBelow θ.fixedSet

The set of fixed points in [0,1] is bounded below by 0.

theorem BranchingProcess.Offspring.isClosed_fixedSet {J : ℕ} (θ : Offspring J) : IsClosed θ.fixedSet

The set of fixed points in [0,1] is closed, f being continuous.

theorem BranchingProcess.Offspring.extinction_mem {J : ℕ} (θ : Offspring J) : θ.extinction ∈ Set.Icc 0 1 ∧ θ.gen θ.extinction = θ.extinction

The infimum is itself a fixed point: q ∈ [0,1] and f(q) = q.

theorem BranchingProcess.Offspring.extinction_nonneg {J : ℕ} (θ : Offspring J) : 0 ≤ θ.extinction

The extinction probability is nonnegative.

theorem BranchingProcess.Offspring.extinction_le_one {J : ℕ} (θ : Offspring J) : θ.extinction ≤ 1

The extinction probability is at most one.

theorem BranchingProcess.Offspring.gen_extinction {J : ℕ} (θ : Offspring J) : θ.gen θ.extinction = θ.extinction

f(q) = q.

theorem BranchingProcess.Offspring.extinction_le_of_fixed {J : ℕ} (θ : Offspring J) {s : ℝ} (hs : s ∈ Set.Icc 0 1) (hfix : θ.gen s = s) : θ.extinction ≤ s

Minimality: the extinction probability is below every fixed point of f in [0,1].

theorem BranchingProcess.Offspring.extinction_eq_zero_iff {J : ℕ} (θ : Offspring J) : θ.extinction = 0 ↔ θ.mass 0 = 0

Extinction is impossible exactly when childless vertices are: q = 0 if and only if θ_0 = 0.

theorem BranchingProcess.Offspring.extinction_pos {J : ℕ} (θ : Offspring J) (h : 0 < θ.mass 0) : 0 < θ.extinction

Positive mass at zero forces a positive extinction probability.

theorem BranchingProcess.Offspring.extinction_lt_one_of_supercritical {J : ℕ} (θ : Offspring J) (h : θ.IsSupercritical) : θ.extinction < 1

The classical criterion: a supercritical law survives with positive probability, q < 1. The mean exceeds one, so the difference quotient g of one_sub_gen exceeds one at some s < 1, whence f(s) < s; since f(0) = θ_0 ≥ 0, the intermediate value theorem returns a fixed point in [0,s], and minimality pushes q below it.