Finite-tree contour bracketing by DFS heights

This module compares the discrete contour of a finite plane tree with its depth-first height sequence, using the exact first-visit times.

def BGW.PlaneTree.heightSeq (t : PlaneTree) (i : ℕ) : ℕ

DFS heights extended by 0: |v_i| for i < size, and 0 for i ≥ size.

Equations

• t.heightSeq i = (Option.map List.length t.vertices[i]?).getD 0

def BGW.PlaneTree.contourAt (t : PlaneTree) (m : ℕ) : ℕ

The contour at integer time m (original speed), 0 after the end of the contour.

Equations

• t.contourAt m = t.contour.getD m 0

noncomputable def BGW.PlaneTree.heightLin (t : PlaneTree) (u : ℝ) : ℝ

Linear interpolation of the heights at integer times (used for u ≥ 0).

Equations

• t.heightLin u = (1 - (u - ↑⌊u⌋₊)) * ↑(t.heightSeq ⌊u⌋₊) + (u - ↑⌊u⌋₊) * ↑(t.heightSeq (⌊u⌋₊ + 1))

noncomputable def BGW.PlaneTree.contourLin (t : PlaneTree) (s : ℝ) : ℝ

Linear interpolation of the contour at integer times (used for s ≥ 0).

Equations

• t.contourLin s = (1 - (s - ↑⌊s⌋₊)) * ↑(t.contourAt ⌊s⌋₊) + (s - ↑⌊s⌋₊) * ↑(t.contourAt (⌊s⌋₊ + 1))

Heights

theorem BGW.PlaneTree.heightSeq_of_lt (t : PlaneTree) {i : ℕ} (hi : i < t.size) : t.heightSeq i = t.height ⟨i, hi⟩

On an existing DFS index, the extended height sequence is the vertex depth.

theorem BGW.PlaneTree.heightSeq_of_le (t : PlaneTree) {i : ℕ} (hi : t.size ≤ i) : t.heightSeq i = 0

At and beyond the size, the extended height sequence is zero.

theorem BGW.PlaneTree.heightSeq_le (t : PlaneTree) (i : ℕ) : t.heightSeq i ≤ i

A vertex is deeper than its DFS index at most.

theorem BGW.PlaneTree.heightSeq_succ_le (t : PlaneTree) (i : ℕ) : t.heightSeq (i + 1) ≤ t.heightSeq i + 1

Heights increase by at most one along the DFS order.

theorem BGW.PlaneTree.heightLin_natCast (t : PlaneTree) (i : ℕ) : t.heightLin ↑i = ↑(t.heightSeq i)

At a natural time, linear interpolation recovers the DFS height.

theorem BGW.PlaneTree.contourLin_natCast (t : PlaneTree) (m : ℕ) : t.contourLin ↑m = ↑(t.contourAt m)

At an integer time, linear interpolation recovers the contour value.

Contour values

theorem BGW.PlaneTree.contourAt_of_lt (t : PlaneTree) {m : ℕ} (hm : 2 * (t.size - 1) < m) : t.contourAt m = 0

Beyond the contour's final listed time, the totalized contour is zero.

theorem BGW.PlaneTree.contourAt_firstVisit (t : PlaneTree) {i : ℕ} (hi : i < t.size) : t.contourAt (2 * i - t.heightSeq i) = t.heightSeq i

First visit of the DFS vertex i at time 2i - H_i.

theorem BGW.PlaneTree.exists_contourAt_le_heightSeq (t : PlaneTree) (m : ℕ) : ∃ i < t.size, t.contourAt m ≤ t.heightSeq i

Every contour value is at most the depth of some vertex (a depth, before the end).

theorem BGW.PlaneTree.exists_contourAt_eq_heightSeq (t : PlaneTree) {m : ℕ} (hm : m < 2 * t.size - 1) : ∃ i < t.size, t.contourAt m = t.heightSeq i

Before the end, every contour value is the depth of some vertex.

Local bracketing

theorem BGW.PlaneTree.contourAt_bracket (t : PlaneTree) {i m : ℕ} (hi : i < t.size) (hm1 : 2 * i - t.heightSeq i ≤ m) (hm2 : m ≤ 2 * (i + 1) - t.heightSeq (i + 1)) : |↑(t.contourAt m) - ↑(t.heightSeq i)| ≤ |↑(t.heightSeq (i + 1)) - ↑(t.heightSeq i)| + 1

Integer bracketing: between the first visits of v_i and v_{i+1} (with b_z = 2z), the contour stays within |H_{i+1} - H_i| + 1 of H_i.

theorem BGW.PlaneTree.contourLin_bracket (t : PlaneTree) {s : ℝ} (hs0 : 0 ≤ s) (hs : s ≤ 2 * ↑t.size) : ∃ i < t.size, s / 2 - 1 ≤ ↑i ∧ ↑i ≤ s / 2 + ↑(t.heightSeq i) / 2 ∧ |t.contourLin s - ↑(t.heightSeq i)| ≤ |↑(t.heightSeq (i + 1)) - ↑(t.heightSeq i)| + 1

Real-time bracketing: every contour time s ∈ [0, 2z] lies in a bracket i with s/2 - 1 ≤ i ≤ s/2 + H_i/2, and the interpolated contour at s is within |H_{i+1} - H_i| + 1 of H_i.

theorem BGW.PlaneTree.contourLin_two_mul_sub_heightLin_le (t : PlaneTree) {u ω δ : ℝ} (hu0 : 0 ≤ u) (hu : u ≤ ↑t.size) (hω1 : 1 ≤ ω) (hω2 : ∀ j < t.size, ↑j ≤ 2 * u → ↑(t.heightSeq j) / 2 ≤ ω) (hδ : ∀ (x y : ℝ), 0 ≤ x → x ≤ ↑t.size → 0 ≤ y → y ≤ ↑t.size → |x - y| ≤ ω → |t.heightLin x - t.heightLin y| ≤ δ) : |t.contourLin (2 * u) - t.heightLin u| ≤ 2 * δ + 1

Prefix-local comparison of the contour at time 2u with the interpolated height at u: if ω ≥ 1 bounds half the heights of the vertices of index ≤ 2u, and δ bounds the oscillation of heightLin over windows of width ω inside [0, z], then the two differ by at most 2δ + 1. Only indices ≤ 2u are used (K16 applies it on a larger prefix a' < 1).