Integer grid enclosures and linear interpolation

Long regeneration gaps control short integer rises. Close enclosing grid values then bound all integer heights between them. Convex interpolation preserves the same enclosure, including large downward steps.

theorem BGW.StableTrees.HeightTightness.exists_clock_gap {r : ℕ → ℕ} (hr0 : r 0 = 0) {L M s : ℕ} (hL : M < r L) (hs : s ≤ M) : ∃ j < L, r j ≤ s ∧ s < r (j + 1)

The first clock endpoint after s determines a gap among the first L.

theorem BGW.StableTrees.HeightTightness.short_rise_le_of_long_gaps {h r : ℕ → ℕ} {q L M d : ℕ} (hr0 : r 0 = 0) (hL : M < r L) (hgaps : ∀ j < L, d < r (j + 1) - r j) (hrise : ∀ j < L, ∀ (s : ℕ), r j ≤ s → ∀ (t : ℕ), s ≤ t → t ≤ r (j + 1) → h t ≤ h s + q) {s t : ℕ} (hst : s ≤ t) (ht : t ≤ M) (hd : t - s ≤ d) : h t ≤ h s + 2 * q

Long gaps and bounded rises within gaps control every short upward variation.

theorem BGW.StableTrees.HeightTightness.interpolation_mem_Icc {x y l u a : ℝ} (hx : x ∈ Set.Icc l u) (hy : y ∈ Set.Icc l u) (ha : a ∈ Set.Icc 0 1) : (1 - a) * x + a * y ∈ Set.Icc l u

Convex combinations of values in the same interval remain in that interval.

theorem BGW.StableTrees.HeightTightness.forestHeightLin_mem_Icc {ω : ℕ → ℕ} {c l u t : ℝ} {p r : ℕ} (ht : 0 ≤ t) (hp : p ≤ ⌊t⌋₊) (hr : ⌊t⌋₊ + 1 ≤ r) (hb : ∀ (i : ℕ), p ≤ i → i ≤ r → c * ↑(DiscreteForest.forestHeight ω i) ∈ Set.Icc l u) : c * DiscreteForest.forestHeightLin ω t ∈ Set.Icc l u

Linear interpolation stays within bounds valid at its two neighboring integer times.

theorem BGW.StableTrees.HeightTightness.forestHeightLin_oscillation_le_enclosing_grid {ω : ℕ → ℕ} {c η s t : ℝ} {p r q : ℕ} (hc : 0 ≤ c) (hs : 0 ≤ s) (ht : 0 ≤ t) (hps : p ≤ ⌊s⌋₊) (hsr : ⌊s⌋₊ + 1 ≤ r) (hpt : p ≤ ⌊t⌋₊) (htr : ⌊t⌋₊ + 1 ≤ r) (hend : |c * ↑(DiscreteForest.forestHeight ω p) - c * ↑(DiscreteForest.forestHeight ω r)| ≤ η) (hrise : ∀ (i : ℕ), p ≤ i → ∀ (j : ℕ), i ≤ j → j ≤ r → DiscreteForest.forestHeight ω j ≤ DiscreteForest.forestHeight ω i + 2 * q) : |c * DiscreteForest.forestHeightLin ω s - c * DiscreteForest.forestHeightLin ω t| ≤ η + 4 * c * ↑q

Integer rise bounds and close enclosing grid values control interpolated oscillations.