LemmaStatement: AI-adaptedProof: AI-generatedPipeline-generatedjudge pass (gpt-6-luna)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

A deterministic-prefix envelope sum for the sharper UCB count bound

Statement

Let $n \geq 5$ be an integer, let $a > 0$ , and put $L = \log n$ . For $x \geq 0$ define $x_{+} = \max {x, 0}$ and $f (x) = \exp (- \frac{(a \sqrt{x} - 2 \sqrt{L})_{+}^{2}}{2}) .$ Then $\sum_{s = 1}^{n - 1} f (s) \leq 1 + \frac{8 L}{a^{2}} .$ For $n \geq 12$ the stronger bound $\sum_{s = 1}^{n - 1} f (s) \leq 8 L / a^{2}$ holds. All integrals in the proof are proper Riemann integrals or their separately convergent improper limits.

Statement references

Lattimore and Szepesvári, Bandit Algorithms, Theorems 7.1–7.2: supplies the UCB proof context; this deterministic estimate is proved locally.

Facts & Assumptions

Given: The integer $n$ , positive $a$ , and $L = \log n$ in the Statement.

[F1]

The Gaussian integral is $\int_{- \infty}^{\infty} e^{- x^{2}} d x = \sqrt{π}$ . The Gaussian integral $\int_{- \infty}^{\infty} e^{- x^{2}} d x = \sqrt{π}$

[F2]

A monotone differentiable surjection between improper intervals preserves the integral, with absolute Jacobian, when its derivative is locally integrable and proper substitution holds on every compact truncation. Change of variable in an improper integral

[F3]

Proper substitution holds for a differentiable substitution with integrable derivative and continuous integrand on an interval containing its image. Substitution: if $φ$ is differentiable on $[c, d]$ with $φ^{'}$ integrable and $f$ is continuous on an interval containing $φ ([c, d])$ , then $\int_{φ (c)}^{φ (d)} f = \int_{c}^{d} (f \circ φ) φ^{'}$

[F4]

For $u > 0$ , $\log^{'} (u) = 1 / u$ and $\log u = \int_{1}^{u} d t / t$ ; logarithms are increasing and obey the product law. The natural logarithm has derivative 1/x and equals the integral from 1 to x of 1/t Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm

[F5]

Principal arctangent satisfies $(\arctan x)^{'} = 1 / (1 + x^{2})$ , $\arctan x = \int_{0}^{x} d t / (1 + t^{2})$ , and $\arctan 1 = π / 4$ . Principal arctangent: derivative, integral, power series, and the Gregory–Leibniz series

[F6]

An integrable derivative integrates to the endpoint difference; integration preserves pointwise inequalities between integrable functions. The second fundamental theorem: if $G$ is differentiable on $[a, b]$ with $G^{'} = f$ and $f$ is integrable, then $\int_{a}^{b} f = G (b) - G (a)$ If $f \leq g$ on $[a, b]$ and both are integrable then $\int_{a}^{b} f \leq \int_{a}^{b} g$ ; and $m (b - a) \leq \int_{a}^{b} f \leq M (b - a)$

[F7]

The exponential has derivative equal to itself, and the chain rule differentiates compositions. The exponential function is smooth and $(\exp)^{'} = \exp$ The chain rule, in one line from Carathéodory: if $g$ is differentiable at $c$ and $f$ is differentiable at $g (c)$ , then $f \circ g$ is differentiable at $c$ with $(f \circ g)^{'} (c) = f^{'} (g (c)) g^{'} (c)$

[F8]

Convergent improper integrals can be split at a finite interior point and combined linearly. Improper convergence is independent of finite truncations and split points Linearity of convergent improper integrals

[F9]

Nonnegative reals have unique nonnegative square roots. Square roots exist: a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ ; the positives are ${x^{2} : x \neq 0}$

[F10]

A continuous function on an interval is decreasing when its derivative is negative throughout the interior. On an interval $I$ , for $f$ continuous on $I$ and differentiable at every interior point: $f^{'} \geq 0$ throughout gives $f$ nondecreasing, $f^{'} > 0$ gives $f$ increasing, $f^{'} \leq 0$ and $f^{'} < 0$ give the two decreasing forms; conversely a nondecreasing $f$ has $f^{'} \geq 0$ and a nonincreasing $f$ has $f^{'} \leq 0$ wherever it is differentiable, and no strict converse is claimed

[F11]

The exponential is positive and strictly increasing. The exponential function is strictly increasing The exponential is positive and satisfies $\exp (- x) = 1 / \exp (x)$

[F12]

Polynomial powers differentiate by the power rule, and sums, products and nonvanishing quotients obey the derivative algebra. For a natural $n \geq 1$ the function $x \mapsto x^{n}$ is differentiable everywhere with derivative $ι (n) x^{n - 1}$ ; for $n = 0$ it is the constant $1$ , with derivative $0$ ; for a natural $n \geq 1$ the function $x \mapsto x^{- n}$ is differentiable at every $x \neq 0$ with derivative $- ι (n) x^{- n - 1}$ ; consequently every polynomial function is differentiable at every real, with the derivative computed term by term Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$

[F13]

The exponential tends to zero at negative infinity. The exponential tends to $+ \infty$ at $+ \infty$ and to $0$ at $- \infty$

[F14]

The real exponential is continuous, positive, strictly increasing, and satisfies $\exp (0) = 1$ (The real exponential function and the number $e$ by a power series, The exponential function is strictly increasing, The exponential is positive and satisfies $\exp (- x) = 1 / \exp (x)$ ).

[F15]

Sums and scalar multiples of continuous real functions are continuous, every real polynomial map is continuous, and continuous maps compose continuously (Sums, scalar multiples, products, absolute values, maxima, minima and quotients with nonvanishing denominator of continuous functions are continuous, as are constants, the identity and every polynomial function, A composite of continuous functions is continuous, with no side hypothesis of the kind the composition of limits needs).

[F16]

A continuous real function on a compact interval is Riemann integrable (A continuous function on $[a, b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion).

[F17]

For an integrable function, proper integrals add over adjacent subintervals (For $a < c < b$ : $f$ is integrable on $[a, b]$ if and only if it is integrable on $[a, c]$ and on $[c, b]$ , and then $\int_{a}^{b} f = \int_{a}^{c} f + \int_{c}^{b} f$ ; with the oriented form for arbitrary $a, b, c$ ).

Proof

1.1givenF6F8F9F14F15F16F17algebraF11

By [F9], for $0 \leq x < y$ the identity $y - x = (\sqrt{y} - \sqrt{x}) (\sqrt{y} + \sqrt{x})$ and $\sqrt{y} + \sqrt{x} > 0$ imply $\sqrt{x} < \sqrt{y}$ : indeed $y > 0$ , and $\sqrt{y} > 0$ follows because its square is $y$ . Thus the nonnegative square-root map is increasing. It is continuous at every $x_{0} > 0$ , since $\sqrt{x} + \sqrt{x_{0}} \geq \sqrt{x_{0}} > 0$ and $∣ \sqrt{x} - \sqrt{x_{0}} ∣ = \frac{∣ x - x_{0} ∣}{\sqrt{x} + \sqrt{x_{0}}} \leq \frac{∣ x - x_{0} ∣}{\sqrt{x_{0}}};$ given $ε > 0$ , $∣ x - x_{0} ∣ < ε \sqrt{x_{0}}$ makes this difference less than $ε$ . At $x_{0} = 0$ , for each $ε > 0$ , $0 \leq x < ε^{2}$ implies $\sqrt{x} < \sqrt{ε^{2}} = ε$ , so it is continuous there as well. The map $u \mapsto u_{+}$ is nondecreasing and continuous, since $∣ u_{+} - v_{+} ∣ \leq ∣ u - v ∣$ by its sign cases. Thus $a \sqrt{x} - 2 \sqrt{L}$ and its positive part are continuous, and [F15] makes the final composition defining $f$ continuous. The positive part is nonnegative and nondecreasing; for $0 \leq u \leq v$ , $v^{2} - u^{2} = (v - u) (v + u) \geq 0$ , so squaring preserves that order. Hence the exponent is nonincreasing, and [F14] makes $f$ nonincreasing; its exponent is nonpositive, so positivity, monotonicity and $\exp (0) = 1$ give $0 < f \leq 1$ . The continuous function $f$ is integrable on $[0, n - 1]$ by [F16], and repeated use of [F17] gives $\int_{0}^{n - 1} f = \sum_{s = 1}^{n - 1} \int_{s - 1}^{s} f$ . For $x \in [s - 1, s]$ , $f (x) \geq f (s)$ ; [F6] gives $f (s) \leq \int_{s - 1}^{s} f (x) d x$ . Hence $S : = \sum_{s = 1}^{n - 1} f (s) \leq \int_{0}^{n - 1} f (x) d x$ . If $\int_{0}^{\infty} f$ converges, nonnegativity of the tail and [F8] give $\int_{0}^{n - 1} f \leq \int_{0}^{\infty} f$ . Also $S \leq n - 1$ .

1.2F1F2F6F7F8F12F13given

Write $b = 2 \sqrt{L} > 0$ . The integrands $e^{- y^{2} / 2}$ and $y e^{- y^{2} / 2}$ are continuous on every compact truncation of $[0, \infty)$ . Evenness in [F1] and the scaling $y = \sqrt{2} x$ give $\int_{0}^{\infty} e^{- y^{2} / 2} d y = \sqrt{π / 2}$ by [F2], with convergence inherited from the Gaussian integral. The primitive $- e^{- y^{2} / 2}$ gives $\int_{0}^{\infty} y e^{- y^{2} / 2} d y = 1$ by [F6] and [F7]; the endpoint limit follows from [F13]. The substitutions are increasing smooth surjections on the half-lines, with continuous derivatives and continuous integrands on every compact truncation, so all hypotheses of [F2] hold and these two improper integrals converge separately.

1.3F5F6F12algebra

The integrand $x^{4} (1 - x)^{4} / (1 + x^{2})$ is continuous on $[0, 1]$ , since $1 + x^{2} > 0$ there. Polynomial division gives $\frac{x^{4} (1 - x)^{4}}{1 + x^{2}} = x^{6} - 4 x^{5} + 5 x^{4} - 4 x^{2} + 4 - \frac{4}{1 + x^{2}} .$ Integrating on $[0, 1]$ using [F5] and [F6] yields $\int_{0}^{1} \frac{x^{4} (1 - x)^{4}}{1 + x^{2}} d x = \frac{1}{7} - \frac{2}{3} + 1 - \frac{4}{3} + 4 - π = \frac{22}{7} - π > 0.$ The strict positivity follows because the integrand is nonnegative and on $[1 / 4, 3 / 4]$ is at least $1 / (2 \cdot 4^{8}) > 0$ . Thus $π < 22 / 7$ .

2.1F2F3F8F9step 1.2algebra

On $[0, b^{2} / a^{2}]$ , $f = 1$ . On the remaining half-line use $x = (y + b)^{2} / a^{2}$ , whose derivative $2 (y + b) / a^{2}$ is positive and continuous and whose image is exactly $[b^{2} / a^{2}, \infty)$ . Proper substitution applies on compact truncations by [F3], so [F2], [F8], and step 1.2 give $\int_{0}^{\infty} f (x) d x = \frac{b^{2}}{a^{2}} + \frac{2}{a^{2}} \int_{0}^{\infty} (y + b) e^{- y^{2} / 2} d y = \frac{4 L + 2 + \sqrt{8 π L}}{a^{2}} .$ This proves finiteness and justifies step 1.1.

2.2F3F4F6F12step 1.3algebra

Put $z = (u - 1) / (u + 1)$ for $u > 1$ , so $0 < z < 1$ and $1 / (1 - t^{2})$ is continuous on $[0, z]$ . The increasing substitution $t \mapsto (1 + t) / (1 - t)$ on $[0, z]$ has continuous derivative and takes that interval onto $[1, u]$ . Hence [F3] and [F4] give $\log u = 2 \int_{0}^{z} d t / (1 - t^{2})$ . For every integer $q \geq 0$ , the finite geometric identity gives $1 / (1 - t^{2}) \geq \sum_{j = 0}^{q} t^{2 j}$ on this interval. Integrating this polynomial by [F6] proves $\log u \geq 2 \sum_{j = 0}^{q} \frac{z^{2 j + 1}}{2 j + 1} .$ At $u = 2, q = 1$ , $u = 3, q = 2$ , and $u = 5, q = 2$ , respectively, this yields $\log 2 \geq \frac{56}{81}, \log 3 \geq \frac{263}{240}, \log 5 \geq \frac{1924}{1215} > \frac{11}{7} > \frac{π}{2} .$

3.1F4step 2.2algebra

By [F4] and step 2.2, $\log 12 = 2 \log 2 + \log 3 \geq \frac{16061}{6480} > \frac{99}{40}, \log 11 > \log 10 = \log 2 + \log 5 \geq \frac{2764}{1215} > \frac{9}{4} .$ All comparisons follow by multiplying positive integer denominators; no decimal approximation is used.

4.1F6F9step 1.1step 2.1step 1.3step 3.1algebra

Define $D (L) = 2 + \sqrt{8 π L} - 4 L$ . If $n \geq 12$ , step 3.1 gives $L > 99 / 40$ . At $L_{0} = 99 / 40$ , $(4 L_{0} - 2)^{2} = \frac{6241}{100} > 8 \frac{22}{7} \frac{99}{40} > 8 π L_{0},$ so $D (L_{0}) < 0$ . For $L_{2} > L_{1} \geq L_{0} > 1$ , the difference of $4 L - 2 - \sqrt{8 π L}$ at these two values equals $(\sqrt{L_{2}} - \sqrt{L_{1}}) (4 (\sqrt{L_{2}} + \sqrt{L_{1}}) - \sqrt{8 π}) > 0$ , since $π < 22 / 7 < 8$ . Thus $D (L) \leq 0$ here. Steps 1.1 and 2.1 give $S \leq 8 L / a^{2}$ , the asserted stronger bound.

4.2F4F6F9F10F12step 2.2step 3.1algebra

Suppose $5 \leq n \leq 11$ . Step 2.2 gives $L > π / 2$ , whence $\sqrt{8 π L} \leq 4 L$ and $D (L) \leq 2$ . For $g (x) = 4 \log x - x + 2$ , the derivative $g^{'} (x) = 4 / x - 1$ is continuous and negative on $[5, 11]$ , so $g$ is decreasing there. Step 3.1 gives $g (11) > 0$ , hence $g (n) \geq g (11) > 0$ and therefore $n - 2 \leq 4 L$ .

5.1givenstep 1.1step 2.1step 4.1step 4.2casesalgebra∎

If $D (L) \leq 0$ , steps 1.1 and 2.1 already give $S \leq 8 L / a^{2}$ . If $D (L) > 0$ and $a^{2} \geq D (L)$ , those steps give $S \leq (8 L + D (L)) / a^{2} \leq 8 L / a^{2} + 1$ . If $0 < a^{2} < D (L) \leq 2$ , step 4.2 gives $(n - 2) a^{2} \leq (n - 2) D (L) \leq 2 (n - 2) \leq 8 L$ , so $S \leq n - 1 \leq 1 + 8 L / a^{2}$ . These cases exhaust $5 \leq n \leq 11$ and prove the Statement together with step 4.1.

Depends on

Used by

A sharper expected suboptimal-arm pull count for the unchanged UCB rule Lemma

Dependency tree · two levels

117 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Lattimore and Szepesvári, Bandit Algorithms, Theorems 7.1–7.2; independent local sharpening of the expected-pull argument (standard reference, not scraped)