Lebesgue measure of occupation cells #
The floor fibers are disjoint half-open cells of equal length. The only extra piece after the discrete mesh endpoint is the final incomplete cell.
theorem
BGW.StableTrees.DiscreteHeightApprox.finiteHeightApprox_forestWalkPath
(B : ℕ → ℝ)
{n : ℕ}
(hn : 0 < n)
(hB : 0 < B n)
(T : NNReal)
(ω : ℕ → ℕ)
{t : NNReal}
(ht : t ≤ T)
{ε : ℝ}
(hε : 0 < ε)
:
finiteHeightApprox T t ε (DiscreteForest.forestWalkPath B n T ω) = discreteOccupation B n ε ω t + (↑t - ↑⌊↑n * ↑t⌋₊ / ↑n) / ε
The finite-path occupation equals its discrete mesh count plus the final partial cell.
theorem
BGW.StableTrees.DiscreteHeightApprox.abs_finiteHeightApprox_sub_discreteOccupation_le
(B : ℕ → ℝ)
{n : ℕ}
(hn : 0 < n)
(hB : 0 < B n)
(T : NNReal)
(ω : ℕ → ℕ)
{t : NNReal}
(ht : t ≤ T)
{ε : ℝ}
(hε : 0 < ε)
:
|finiteHeightApprox T t ε (DiscreteForest.forestWalkPath B n T ω) - discreteOccupation B n ε ω t| ≤ 1 / (↑n * ε)
The last partial cell contributes less than one mesh cell to the occupation.