Lemma 2 — square-root perturbation

Proved

GittinsUCB.Patient.lemma_2

by mikedeng1 · Oct 22, 2026 · Mathlib 0df444a (Lean v4.33.1)

asymptoticsp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1real-analysis

Let $f:\mathbb R\to\mathbb R$ satisfy $|f(x)|=o(\sqrt{x})$ as $x\to\infty$ . Then

\sqrt{x+f(x)}=\sqrt{x}+o(1)\qquad(x\to\infty).

This estimate is used when lower-order corrections enter the square roots in the index bounds.

Formalization Note The paper prints $f:\mathbb R_+\to\mathbb R_+$ , but its later application to $h(\gamma)$ requires negative values. The real-valued version records that intended domain; $\sqrt{\cdot}$ is Lean's total real square root, and the little-o premise controls the eventual radicand.

Preamble

import Mathlib
import Definitions.Def_GittinsUCB_Patient_Model
open MeasureTheory ProbabilityTheory Filter Asymptotics NNReal

Formal statement

namespace GittinsUCB.Patient

/-- Lemma 2: square-root perturbations. -/
theorem lemma_2 (f : ℝ → ℝ)
    (hf : (fun x : ℝ => |f x|) =o[atTop] Real.sqrt) :
    Tendsto (fun x : ℝ => Real.sqrt (x + f x) - Real.sqrt x) atTop (nhds 0) := by sorry

end GittinsUCB.Patient

Source

Russo, A Note on the Equivalence of Upper Confidence Bounds and Gittins Indices for Patient Agents, arXiv:1904.04732v1, p. 3, Lemma 2

Human review

Endorsed by Shuze Chen · Oct 22, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 22, 2026
Confirmed by the mission captain (proposal self-audit).

View graph