Enclosing short interpolation windows by a fixed grid #
Three grid steps enclose a short pair of interpolation times. Short upward variations and close grid endpoint values then control their absolute difference, without an assumption on the largest downward jump.
theorem
BGW.StableTrees.HeightTightness.forestHeightLin_short_oscillation_of_grid
{ω : ℕ → ℕ}
{n N q : ℕ}
{c T δ η : ℝ}
(hc : 0 ≤ c)
(hδ : 0 < δ)
(hδ1 : δ ≤ 1 / 4)
(hn : 1 ≤ ↑n * δ)
(hcover : T + 1 ≤ ↑N * δ)
(hgrid :
∀ j < N,
|c * ↑(DiscreteForest.forestHeight ω ⌊↑n * (↑j * δ)⌋₊) - c * ↑(DiscreteForest.forestHeight ω ⌊↑n * (↑(j + 1) * δ)⌋₊)| ≤ η)
(hrise :
∀ (i j : ℕ),
i ≤ j →
j ≤ ⌊↑n * (↑N * δ)⌋₊ →
j - i ≤ ⌊↑n * (4 * δ)⌋₊ → DiscreteForest.forestHeight ω j ≤ DiscreteForest.forestHeight ω i + 2 * q)
{s t : ℝ}
(hs : s ∈ Set.Icc 0 T)
(ht : t ∈ Set.Icc 0 T)
(hst : s ≤ t)
(hd : t - s ≤ δ)
:
Three grid steps enclose a short ordered pair of interpolation times.