Total progeny and the hitting-time theorem

DefinitionFirst passage of the exploration walk#✓fully proved

The exploration walk started at k with steps x_i - 1 stays positive at every time j < n: j < k + ∑_{i < j} x_i. Together with ∑ x_i + k = n this says that the walk first hits 0 at time n.

def IsFirstPassage (k n : ℕ) (x : Fin n → ℕ) : Prop :=
  ∀ j ∈ range n, j < k + ∑ i with i.val < j, x i

Used by 5

Used byCycle lemma · Hitting weight of first-passage step sequences · Probability of first passage at time n · Hitting-time theorem · Otter–Dwass formula

DefinitionCyclic shift of a tuple#✓fully proved

The cyclic shift i ↦ x_{(i + r) mod n} of a tuple.

def rotate {n : ℕ} (x : Fin n → ℕ) (r : ℕ) : Fin n → ℕ :=
  fun i => x ⟨(i.val + r) % n, Nat.mod_lt _ (Nat.zero_lt_of_lt i.isLt)⟩

Used by 2

Used byCycle lemma · Hitting-time theorem

TheoremCycle lemma#✓fully proved

Cycle lemma (Dvoretzky–Motzkin 1947). If x : Fin n → ℕ satisfies ∑ x_i + k = n with 1 ≤ k, then exactly k of the n cyclic shifts of x (counted by shift r < n) are first-passage sequences.

theorem card_filter_isFirstPassage_rotate {k n : ℕ} (hk : 1 ≤ k) (x : Fin n → ℕ)
    (hx : ∑ i, x i + k = n) :
    #{r ∈ range n | IsFirstPassage k n (rotate x r)} = k

Uses 2 · Used by 1

Statement usesFirst passage of the exploration walk · Cyclic shift of a tuple

Used byHitting-time theorem

DefinitionWalk weight of step sequences ending at zero#✓fully proved

The weight W_p(k, n) = ∑ ∏_i p(x_i) over the step sequences x : Fin n → ℕ with ∑ x_i + k = n (the walk from k is at 0 at time n). For p(j) = P(ξ = j) this is P(ξ_1 + ⋯ + ξ_n = n - k) when k ≤ n, and 0 when k > n.

def walkWeight {R : Type*} [CommSemiring R] (p : ℕ → R) (k n : ℕ) : R :=
  ∑ x ∈ (Nat.antidiagonalTuple n (n - k)).filter (fun x => ∑ i, x i + k = n), ∏ i, p (x i)

Used by 5

Used byProbability of the offspring walk event as a walk weight · Hitting-time theorem · Borel–Tanner law · Otter–Dwass formula · Walk weights for Poisson offspring

DefinitionHitting weight of first-passage step sequences#✓fully proved

The weight H_p(k, n) = ∑ ∏_i p(x_i) over the step sequences with ∑ x_i + k = n along which the walk from k first hits 0 at time n. For p(j) = P(ξ = j) this is the probability P(T = n) that the total progeny of k ancestors is n.

def hittingWeight {R : Type*} [CommSemiring R] (p : ℕ → R) (k n : ℕ) : R :=
  ∑ x ∈ (Nat.antidiagonalTuple n (n - k)).filter
    (fun x => ∑ i, x i + k = n ∧ IsFirstPassage k n x), ∏ i, p (x i)

Uses 1 · Used by 5

Statement usesFirst passage of the exploration walk

Used byBorel law · Probability of first passage at time n · Hitting-time theorem · Borel–Tanner law · Otter–Dwass formula

TheoremHitting-time theorem#✓fully proved

Hitting-time theorem, weighted form: n · H_p(k, n) = k · W_p(k, n) for every weight p with values in a commutative semiring and all k, n. For probability weights this is the hitting-time theorem of van der Hofstad–Keane (2008); the proof double counts cyclic shifts with the cycle lemma.

theorem natCast_mul_hittingWeight {R : Type*} [CommSemiring R] (p : ℕ → R) (k n : ℕ) :
    (n : R) * hittingWeight p k n = k * walkWeight p k n

Uses 5 · Used by 2

Statement usesHitting weight of first-passage step sequences · Walk weight of step sequences ending at zero

Proof usesFirst passage of the exploration walk · Cycle lemma · Cyclic shift of a tuple

Used byBorel–Tanner law · Otter–Dwass formula

TheoremProbability of first passage at time n#✓fully proved

Under ν^{⊗n}, the event that the walk from k first hits 0 at time n has measure H_p(k, n) with p(j) = ν{j}. When ν is a probability measure this is the probability P(T = n).

theorem measure_firstPassage (k n : ℕ) :
    (Measure.pi fun _ : Fin n => ν) {x | ∑ i, x i + k = n ∧ IsFirstPassage k n x} =
      hittingWeight (fun j => ν {j}) k n

Uses 2 · Used by 1

Statement usesFirst passage of the exploration walk · Hitting weight of first-passage step sequences

Used byOtter–Dwass formula

TheoremProbability of the offspring walk event as a walk weight#✓fully proved

Under ν^{⊗n}, the event ξ_1 + ⋯ + ξ_n + k = n has measure W_p(k, n) with p(j) = ν{j}. When ν is a probability measure this is the probability P(ξ_1 + ⋯ + ξ_n = n - k).

theorem measure_walk (k n : ℕ) :
    (Measure.pi fun _ : Fin n => ν) {x | ∑ i, x i + k = n} =
      walkWeight (fun j => ν {j}) k n

Uses 1 · Used by 1

Statement usesWalk weight of step sequences ending at zero

Used byOtter–Dwass formula

TheoremOtter–Dwass formula#✓fully proved

For i.i.d. offspring numbers with law ν and k ancestors, the finite-measure identity n · P(T = n) = k · P(ξ_1 + ⋯ + ξ_n = n - k) holds as an identity of event masses (Otter 1949; Dwass 1969); the two sides are probabilities when ν is a probability measure.

theorem natCast_mul_measure_firstPassage (k n : ℕ) :
    (n : ℝ≥0∞) * (Measure.pi fun _ : Fin n => ν)
        {x | ∑ i, x i + k = n ∧ IsFirstPassage k n x} =
      k * (Measure.pi fun _ : Fin n => ν) {x | ∑ i, x i + k = n}

Uses 6

Statement usesFirst passage of the exploration walk

Proof usesHitting weight of first-passage step sequences · Probability of first passage at time n · Probability of the offspring walk event as a walk weight · Hitting-time theorem · Walk weight of step sequences ending at zero

TheoremWalk weights for Poisson offspring#✓fully proved

For Poisson(r) step weights, W_p(k, n) = e^{-rn} (rn)^{n-k} / (n-k)! when k ≤ n: the sum of n independent Poisson(r) variables is Poisson(rn).

theorem walkWeight_poisson (r : ℝ≥0) {k n : ℕ} (hkn : k ≤ n) :
    walkWeight (fun j => (poissonMeasure r).real {j}) k n =
      Real.exp (-(r * n)) * (r * n) ^ (n - k) / (n - k)!

Uses 1 · Used by 1

Statement usesWalk weight of step sequences ending at zero

Used byBorel–Tanner law

TheoremBorel–Tanner law#✓fully proved

For Poisson(r) offspring and k ≤ n ancestors, n · P(T = n) = k e^{-rn} (rn)^{n-k} / (n-k)! (Tanner 1961; Haight–Breuer 1960).

theorem natCast_mul_hittingWeight_poisson (r : ℝ≥0) {k n : ℕ} (hkn : k ≤ n) :
    (n : ℝ) * hittingWeight (fun j => (poissonMeasure r).real {j}) k n =
      k * (Real.exp (-(r * n)) * (r * n) ^ (n - k) / (n - k)!)

Uses 4 · Used by 1

Statement usesHitting weight of first-passage step sequences

Proof usesHitting-time theorem · Walk weight of step sequences ending at zero · Walk weights for Poisson offspring

Used byBorel law

TheoremBorel law#✓fully proved

For Poisson(r) offspring and one ancestor, the total progeny satisfies P(T = n) = e^{-rn} (rn)^{n-1} / n! for n ≥ 1 (Borel 1942).

theorem hittingWeight_poisson_one (r : ℝ≥0) {n : ℕ} (hn : 1 ≤ n) :
    hittingWeight (fun j => (poissonMeasure r).real {j}) 1 n =
      Real.exp (-(r * n)) * (r * n) ^ (n - 1) / n !

Uses 2

Statement usesHitting weight of first-passage step sequences

Proof usesBorel–Tanner law

DefinitionMean total progeny of a Galton–Watson process#✓fully proved

The mean total progeny ∑_n E Z_n of the Galton–Watson process started from one individual. By Tonelli this is E ∑_n Z_n for any process with the generation laws law ν n.

noncomputable def meanTotalProgeny : ℝ≥0∞ :=
  ∑' n, ∫⁻ z, (z : ℝ≥0∞) ∂(law ν n)

Uses 1 · Used by 1

Statement usesGeneration-size law of a Galton–Watson process

Used byMean total progeny equals \(1/(1-m)\)

TheoremMean total progeny equals \(1/(1-m)\)#✓fully proved

The mean total progeny is (1 - m)⁻¹ in [0, ∞]: it is 1 / (1 - m) for m < 1 and ∞ for m ≥ 1 (m the mean offspring number).

theorem meanTotalProgeny_eq [IsProbabilityMeasure ν] : meanTotalProgeny ν = (1 - mean ν)⁻¹

Uses 4

Statement usesMean offspring number · Mean total progeny of a Galton–Watson process

Proof usesGeneration-size law of a Galton–Watson process · Mean generation size of a Galton–Watson process

14 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.