The unpadded forest contour clock

The ordinary forest contour removes the two zero time units inserted after each tree by the padded contour. This file identifies the two clocks and proves their normalized contours agree asymptotically.

noncomputable def BGW.StableTrees.ForestContour.unpaddedStart (ω : ℕ → ℕ) (r : ℕ) : ℕ

Start of tree r on the unpadded clock: 2 (L r - r), each earlier tree of size z contributing 2 (z - 1) (zero for a singleton).

Equations

• BGW.StableTrees.ForestContour.unpaddedStart ω r = 2 * (BGW.StableTrees.DiscreteForest.ladderTime ω r - r)

noncomputable def BGW.StableTrees.ForestContour.unpaddedBlock (ω : ℕ → ℕ) (m : ℕ) : ℕ

The block whose unpadded interval [2 (L r - r), 2 (L (r+1) - r - 1)) contains m (singletons have empty intervals and are skipped; junk 0 when no block does).

Equations

• BGW.StableTrees.ForestContour.unpaddedBlock ω m = sInf {r : ℕ | m < BGW.StableTrees.ForestContour.unpaddedStart ω (r + 1)}

noncomputable def BGW.StableTrees.ForestContour.forestContourUnpadded (ω : ℕ → ℕ) (m : ℕ) : ℕ

Unpadded forest contour at integer time m: the plain concatenation of the tree contours (junk 0 off LadderFinite).

Equations

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

noncomputable def BGW.StableTrees.ForestContour.forestContourUnpaddedLin (ω : ℕ → ℕ) (s : ℝ) : ℝ

Linear interpolation of the unpadded forest contour at integer times.

Equations

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

noncomputable def BGW.StableTrees.ForestContour.forestContourUnpaddedError (B : ℕ → ℝ) (n : ℕ) (T : NNReal) (ω : ℕ → ℕ) : ℝ

The uniform distance on [0,T] between the normalized unpadded and padded contours, both at time 2nt.

Equations

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

theorem BGW.StableTrees.ForestContour.two_mul_ladderTime_eq_unpaddedStart {ω : ℕ → ℕ} (hω : DiscreteForest.LadderFinite ω) (r : ℕ) : 2 * DiscreteForest.ladderTime ω r = unpaddedStart ω r + 2 * r

The padded and unpadded starts differ by exactly 2r.

theorem BGW.StableTrees.ForestContour.unpaddedStart_succ {ω : ℕ → ℕ} (hω : DiscreteForest.LadderFinite ω) (r : ℕ) : unpaddedStart ω (r + 1) = unpaddedStart ω r + 2 * ((DiscreteForest.blockTree ω r).size - 1)

The unpadded clock: tree r lasts 2 (z_r - 1), zero for a singleton.

theorem BGW.StableTrees.ForestContour.monotone_unpaddedStart {ω : ℕ → ℕ} (hω : DiscreteForest.LadderFinite ω) : Monotone (unpaddedStart ω)

The unpadded start time is monotone.

theorem BGW.StableTrees.ForestContour.unpaddedBlock_start {ω : ℕ → ℕ} (m : ℕ) : unpaddedStart ω (unpaddedBlock ω m) ≤ m

The selected unpadded block has started by the given time.

theorem BGW.StableTrees.ForestContour.ae_tendsto_unpaddedStart (μ : PMF ℕ) (hc : IsCritical μ) (hne : μ 1 ≠ 1) : ∀ᵐ (ω : ℕ → ℕ) ∂↑(DiscreteForest.offspringSeqLaw μ), Filter.Tendsto (unpaddedStart ω) Filter.atTop Filter.atTop

The total unpadded contour duration is infinite almost surely.

theorem BGW.StableTrees.ForestContour.forestContourUnpaddedLin_eq {ω : ℕ → ℕ} (hω : DiscreteForest.LadderFinite ω) (hdiv : Filter.Tendsto (unpaddedStart ω) Filter.atTop Filter.atTop) {s : ℝ} (hs : 0 ≤ s) : forestContourUnpaddedLin ω s = forestContourLin ω (s + 2 * ↑(unpaddedBlock ω ⌊s⌋₊))

Padded/unpadded identity: when the unpadded clock diverges, the unpadded contour at time s is the padded contour at time s + 2r, r = unpaddedBlock ω ⌊s⌋ the number of earlier trees.