The Borel Growth Lemma

This file proves Émile Borel's Growth Lemma: if S : ℝ → ℝ is monotone on Set.Ici a and satisfies 0 ≤ S a, then

∀ᶠ r in volume.cofinite ⊓ atTop, S (r + (S r)⁻¹) ≤ 2 * S r.

In other words: The inequality S (r + (S r)⁻¹) ≤ 2 * S r holds for all sufficiently large r outside an exceptional set E of finite Lebesgue measure. In Value Distribution Theory, this statement is central to the proof of the "Lemma on the Logarithmic Derivatives".

The proof here is simpler than the argument typically found in textbooks and does not make any regularity assumption on S.

References

• Lemma 2.4 in Hayman, Meromorphic functions.

• Lemma 3.7 in Section VI.3 of Lang, Introduction to Complex Hyperbolic Spaces

theorem MonotoneOn.eventually_le_two_mul {S : ℝ → ℝ} {a : ℝ} (h₁ : MonotoneOn S (Set.Ici a)) (h₂ : 0 ≤ S a) : ∀ᶠ (r : ℝ) in MeasureTheory.volume.cofinite ⊓ Filter.atTop, S (r + (S r)⁻¹) ≤ 2 * S r

Borel's Growth Lemma: if S : ℝ → ℝ is monotone on Set.Ici a and is non-negative at a, then the inequality S (r + (S r)⁻¹) ≤ 2 * S r holds for all sufficiently large r outside a set of finite Lebesgue measure.