The padded contour of a discrete forest

The forest is explored block by block, with two zero contour units after each tree. Its contour is bracketed by the record-count height process, with a normalized uniform-error estimate stated in terms of height oscillation and adjacent height jumps.

@[instance_reducible]

def BGW.StableTrees.ForestContour.forestContourTreeMeasurable : MeasurableSpace PlaneTree

The discrete σ-algebra on plane trees, used locally for countable sums over trees.

Equations

• BGW.StableTrees.ForestContour.forestContourTreeMeasurable = ⊤

theorem BGW.StableTrees.ForestContour.forestContourTreeSingleton : MeasurableSingletonClass PlaneTree

@[instance_reducible]

def BGW.StableTrees.ForestContour.forestContourWordMeasurable : MeasurableSpace (List ℕ)

The discrete σ-algebra on words of natural numbers, used locally for countable sums.

Equations

• BGW.StableTrees.ForestContour.forestContourWordMeasurable = ⊤

theorem BGW.StableTrees.ForestContour.forestContourWordSingleton : MeasurableSingletonClass (List ℕ)

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

The block whose padded contour interval [2 L r, 2 L (r+1)) contains the integer time m (junk 0 when no block does, which happens only off LadderFinite).

Equations

• BGW.StableTrees.ForestContour.contourBlock ω m = sInf {r : ℕ | m < 2 * BGW.StableTrees.DiscreteForest.ladderTime ω (r + 1)}

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

Padded forest contour at integer time m: the contour of blockTree ω r at local time m - 2 L r, r = contourBlock ω m, so that tree r occupies [2 L r, 2 L (r+1)] (its contour, then two zero units); junk 0 off LadderFinite.

Equations

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

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

Linear interpolation of the padded forest contour at integer times.

Equations

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

noncomputable def BGW.StableTrees.ForestContour.forestContourPath (B : ℕ → ℝ) (n : ℕ) (T : NNReal) (ω : ℕ → ℕ) : C(↑(Set.Icc 0 ↑T), ℝ)

The normalized contour path t ↦ (B n / n) * forestContourLin ω (2 n t) on [0,T] (the junk branch never occurs, continuous_forestContourLin).

Equations

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

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

The uniform distance on [0,T] between the normalized contour at time 2nt and the normalized interpolated height at time nt.

Equations

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

theorem BGW.StableTrees.ForestContour.continuous_forestContourLin (ω : ℕ → ℕ) : Continuous (forestContourLin ω)

The interpolated padded contour is continuous.

theorem BGW.StableTrees.ForestContour.forestContourPath_apply (B : ℕ → ℝ) (n : ℕ) (T : NNReal) (ω : ℕ → ℕ) (t : ↑(Set.Icc 0 ↑T)) : (forestContourPath B n T ω) t = B n / ↑n * forestContourLin ω (2 * ↑n * ↑t)

Evaluation of the normalized padded-contour path.

theorem BGW.StableTrees.ForestContour.measurable_forestContour (m : ℕ) : Measurable fun (ω : ℕ → ℕ) => forestContour ω m

Each integer-time padded-contour coordinate is measurable.

theorem BGW.StableTrees.ForestContour.measurable_forestContourPath (B : ℕ → ℝ) (n : ℕ) (T : NNReal) : Measurable (forestContourPath B n T)

The normalized padded-contour path on a compact horizon is measurable.

theorem BGW.StableTrees.ForestContour.measurable_forestContourHeightError (B : ℕ → ℝ) (n : ℕ) (T : NNReal) : Measurable (forestContourHeightError B n T)

The uniform contour/height error is measurable.

theorem BGW.StableTrees.ForestContour.dist_forestContourPath_forestHeightPath (B : ℕ → ℝ) (n : ℕ) (T : NNReal) (ω : ℕ → ℕ) : dist (forestContourPath B n T ω) (DiscreteForest.forestHeightPath B n T ω) = forestContourHeightError B n T ω

The error is the uniform distance between the contour and height paths.

Tree-by-tree adapters to K12a

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

The padded clock: tree r occupies 2 z_r time units, also when it is a singleton.

theorem BGW.StableTrees.ForestContour.forestContour_two_mul_ladderTime_add {ω : ℕ → ℕ} (hω : DiscreteForest.LadderFinite ω) (r : ℕ) {m : ℕ} (hm : m < 2 * (DiscreteForest.blockTree ω r).size) : forestContour ω (2 * DiscreteForest.ladderTime ω r + m) = (DiscreteForest.blockTree ω r).contourAt m

On block r the padded forest contour is the contour of blockTree ω r, followed by two zero units (local times 2 z_r - 2 and 2 z_r - 1).

theorem BGW.StableTrees.ForestContour.forestHeight_ladderTime_add {ω : ℕ → ℕ} (hω : DiscreteForest.LadderFinite ω) (r : ℕ) {i : ℕ} (hi : i ≤ (DiscreteForest.blockTree ω r).size) : DiscreteForest.forestHeight ω (DiscreteForest.ladderTime ω r + i) = (DiscreteForest.blockTree ω r).heightSeq i

Forest heights on block r are the DFS heights of blockTree ω r, including the value 0 at index z_r (the next root).

theorem BGW.StableTrees.ForestContour.forestContourLin_two_mul_ladderTime_add {ω : ℕ → ℕ} (hω : DiscreteForest.LadderFinite ω) (r : ℕ) {s : ℝ} (hs0 : 0 ≤ s) (hs : s ≤ 2 * ↑(DiscreteForest.blockTree ω r).size) : forestContourLin ω (2 * ↑(DiscreteForest.ladderTime ω r) + s) = (DiscreteForest.blockTree ω r).contourLin s

Interpolated form, on the closed block [2 L r, 2 L r + 2 z_r].

theorem BGW.StableTrees.ForestContour.forestHeightLin_ladderTime_add {ω : ℕ → ℕ} (hω : DiscreteForest.LadderFinite ω) (r : ℕ) {u : ℝ} (hu0 : 0 ≤ u) (hu : u ≤ ↑(DiscreteForest.blockTree ω r).size) : DiscreteForest.forestHeightLin ω (↑(DiscreteForest.ladderTime ω r) + u) = (DiscreteForest.blockTree ω r).heightLin u

Interpolated form, on the closed block [L r, L r + z_r].

Forest bracketing

theorem BGW.StableTrees.ForestContour.forestContour_firstVisit {ω : ℕ → ℕ} (hω : DiscreteForest.LadderFinite ω) (k : ℕ) : forestContour ω (2 * k - DiscreteForest.forestHeight ω k) = DiscreteForest.forestHeight ω k

Forest first visit: the DFS vertex of global index k is first visited by the padded contour at time b_k = 2k - H_k.

theorem BGW.StableTrees.ForestContour.forestContour_bracket {ω : ℕ → ℕ} (hω : DiscreteForest.LadderFinite ω) {k m : ℕ} (hm1 : 2 * k - DiscreteForest.forestHeight ω k ≤ m) (hm2 : m ≤ 2 * (k + 1) - DiscreteForest.forestHeight ω (k + 1)) : |↑(forestContour ω m) - ↑(DiscreteForest.forestHeight ω k)| ≤ |↑(DiscreteForest.forestHeight ω (k + 1)) - ↑(DiscreteForest.forestHeight ω k)| + 1

Integer forest bracketing: between the first visits b_k and b_{k+1}, the padded contour stays within |H_{k+1} - H_k| + 1 of H_k (across a tree boundary, H_{k+1} = 0).

theorem BGW.StableTrees.ForestContour.forestContourLin_bracket {ω : ℕ → ℕ} (hω : DiscreteForest.LadderFinite ω) {s : ℝ} (hs : 0 ≤ s) : ∃ (k : ℕ), s / 2 - 1 ≤ ↑k ∧ ↑k ≤ s / 2 + ↑(DiscreteForest.forestHeight ω k) / 2 ∧ |forestContourLin ω s - ↑(DiscreteForest.forestHeight ω k)| ≤ |↑(DiscreteForest.forestHeight ω (k + 1)) - ↑(DiscreteForest.forestHeight ω k)| + 1

Real-time forest bracketing: every contour time s ≥ 0 lies in a bracket k with s/2 - 1 ≤ k ≤ s/2 + H_k/2, and the interpolated contour at s is within |H_{k+1} - H_k| + 1 of H_k.

theorem BGW.StableTrees.ForestContour.forestContourHeightError_le {ω : ℕ → ℕ} (hω : DiscreteForest.LadderFinite ω) (B : ℕ → ℝ) {n : ℕ} (hB : 0 ≤ B n) (T : NNReal) {w : ℝ} (hw1 : 1 ≤ w) (hwn : w + 1 ≤ ↑n) (hw : ∀ (j : ℕ), ↑j ≤ 2 * ↑n * ↑T → ↑(DiscreteForest.forestHeight ω j) / 2 ≤ w) : forestContourHeightError B n T ω ≤ HeightTightness.heightOscillation B n (↑T + 1) (w / ↑n) ω + HeightTightness.maxHeightJump B n (↑T + 1) ω + B n / ↑n

Normalized deterministic bound: if w ≥ 1 bounds half the heights of indices ≤ 2nT and w + 1 ≤ n, the contour/height error on [0,T] is at most the height oscillation at scale w/n plus the largest adjacent jump, both on the horizon T + 1, plus B_n/n.

theorem BGW.StableTrees.ForestContour.contour_height_error_tendstoInMeasure {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) {T : NNReal} (hT : 0 < T) : MeasureTheory.TendstoInMeasure (↑(DiscreteForest.offspringSeqLaw μ)) (fun (n : ℕ) (ω : ℕ → ℕ) => forestContourHeightError B n T ω) Filter.atTop fun (x : ℕ → ℕ) => 0

Contour/height comparison (blueprint K12) on every positive horizon: sup_{t ≤ T} |(B_n/n) C(2nt) - (B_n/n) H_lin(nt)| → 0 in probability.