theorem pointwiseGrowthFunction_eq_zero_of_nonpos {X : Type u} [MetricSpace X] (f : X → ℝ) (xBar : X) (t : ℝ) (ht : t ≤ 0) : pointwiseGrowthFunction f xBar t = 0

Proposition 3.34 (1): the pointwise growth function ω_f(xBar; t) vanishes for every nonpositive radius t.

theorem pointwiseGrowthFunction_monotone {X : Type u} [MetricSpace X] (f : X → ℝ) (xBar : X) : Monotone (pointwiseGrowthFunction f xBar)

Proposition 3.34 (2): the function t ↦ ω_f(xBar; t) is monotone nondecreasing in the radius parameter.

theorem sub_le_pointwiseGrowthFunction_dist {X : Type u} [MetricSpace X] (f : X → ℝ) (xBar x : X) : ↑(f x) - ↑(f xBar) ≤ pointwiseGrowthFunction f xBar (dist x xBar)

Proposition 3.34 (3): every increment f x - f xBar is bounded above by the pointwise growth function evaluated at the distance from x to xBar.