`Bandits.UCB.constSum_le`🔗

Lemma

From the authors

For c > 2, the sum constSum c n is at most 1 + 1 / (c - 2), uniformly in n.

Given

c : ℝ
n : ℕ

Assuming

hc : 2 < c

Then

constSum c n ≤ 1 + 1 / (c - 2)

Real : Type

The type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers.

Nat : Type

The natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.

LT.lt : {α : Type u} → [self : LT α] → α → α → Prop

The less-than relation: `x < y` 

Conventions for notations in identifiers:

 * The recommended spelling of `<` in identifiers is `lt`.

LE.le : {α : Type u} → [self : LE α] → α → α → Prop

The less-equal relation: `x ≤ y` 

Conventions for notations in identifiers:

 * The recommended spelling of `≤` in identifiers is `le`.

Bandits.UCB.constSum : ℝ → ℕ → ℝ

A sum that appears in the UCB regret upper bound. For `c > 2` it is bounded uniformly in `n`,
see `constSum_le`.

Go to its page

HAdd.hAdd : {α : Type u} → {β : Type v} → {γ : outParam (Type w)} → [self : HAdd α β γ] → α → β → γ

`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+` in identifiers is `add`.

HDiv.hDiv : {α : Type u} → {β : Type v} → {γ : outParam (Type w)} → [self : HDiv α β γ] → α → β → γ

`a / b` computes the result of dividing `a` by `b`.
The meaning of this notation is type-dependent.
* For most types like `Nat`, `Int`, `Rat`, `Real`, `a / 0` is defined to be `0`.
* For `Nat`, `a / b` rounds downwards.
* For `Int`, `a / b` rounds downwards if `b` is positive or upwards if `b` is negative.
  It is implemented as `Int.ediv`, the unique function satisfying
  `a % b + b * (a / b) = a` and `0 ≤ a % b < natAbs b` for `b ≠ 0`.
  Other rounding conventions are available using the functions
  `Int.fdiv` (floor rounding) and `Int.tdiv` (truncation rounding).
* For `Float`, `a / 0` follows the IEEE 754 semantics for division,
  usually resulting in `inf` or `nan`. 

Conventions for notations in identifiers:

 * The recommended spelling of `/` in identifiers is `div`.

HSub.hSub : {α : Type u} → {β : Type v} → {γ : outParam (Type w)} → [self : HSub α β γ] → α → β → γ

`a - b` computes the difference of `a` and `b`.
The meaning of this notation is type-dependent.
* For natural numbers, this operator saturates at 0: `a - b = 0` when `a ≤ b`. 

Conventions for notations in identifiers:

 * The recommended spelling of `-` in identifiers is `sub` (when used as a binary operator).

Code

lemma constSum_le {c : ℝ} (hc : 2 < c) (n : ℕ) : constSum c n ≤ 1 + 1 / (c - 2)

Proof

by
  have hc2 : 0 < c - 2 := by linarith
  cases n with
  | zero => simp only [constSum, range_zero, sum_empty]; positivity
  | succ m =>
    -- Comparison of the sum with the integral of `x ↦ x ^ (-(c - 1))` on `[1, 1 + m]`.
    have h_anti : AntitoneOn (fun x : ℝ ↦ x ^ (-(c - 1))) (Set.Icc 1 (1 + m)) :=
      (antitoneOn_rpow_Ioi_of_exponent_nonpos (by linarith)).mono
        fun x hx ↦ zero_lt_one.trans_le hx.1
    have h_sum := AntitoneOn.sum_le_integral h_anti
    rw [integral_rpow (Or.inr ⟨by linarith, ?_⟩)] at h_sum
    swap
    · rw [Set.uIcc_of_le (le_add_of_nonneg_right (by positivity))]
      simp
    have h_pow_nonneg : 0 ≤ (1 + (m : ℝ)) ^ (-(c - 1) + 1) := Real.rpow_nonneg (by positivity) _
    calc constSum c (m + 1)
    _ = 1 + ∑ i ∈ range m, (1 + ((i + 1 : ℕ) : ℝ)) ^ (-(c - 1)) := by
      rw [constSum, Finset.sum_range_succ', add_comm]
      congr 1
      · simp
      · refine Finset.sum_congr rfl fun i _ ↦ ?_
        rw [Real.rpow_neg (by positivity), one_div]
        push_cast
        ring_nf
    _ ≤ 1 + ((1 + m) ^ (-(c - 1) + 1) - 1 ^ (-(c - 1) + 1)) / (-(c - 1) + 1) := by gcongr
    _ = 1 + (1 - (1 + m) ^ (-(c - 1) + 1)) / (c - 2) := by
      rw [Real.one_rpow]
      congr 1
      rw [div_eq_div_iff (by linarith) hc2.ne']
      ring
    _ ≤ 1 + 1 / (c - 2) := by gcongr; linarith

New in v4.34.0-rc2-90-gdde3322 (2026-09-16), and its meaning has not changed since.

Self-contained, with its dependencies inlined and proofs replaced by sorry: download the raw file · open it in the Lean web editor.

Dependency graph

Audit surface: 1 project declarations, 31 external constants

✓ Proved: no sorry anywhere in its closure

This is the tool's own reading of one build's recorded axioms, and it is not robust against an author who wants it to pass. Checking meant to be relied on should go through Comparator, which replays the proof through the kernel from an export against an explicit list of permitted axioms.

Bandits.UCB.constSum_le🔗

`Bandits.UCB.constSum_le`🔗