Proof of Theorem 2.1, p. 10: x ≤ 2 log(1+x) for 0 ≤ x ≤ 1

Proved

GenEllipPot.Potential.scalar_log_bound

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

elliptical-potentiallogarithmp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1

For every real $x\in[0,1]$ ,

x\le 2\log(1+x).

This scalar comparison converts a bounded posterior quadratic form into a logarithmic increment in the proof of the elliptical potential bound.

Preamble

import Mathlib

Formal statement

namespace GenEllipPot.Potential

/-- Scalar inequality used in the proof of Theorem 2.1, p. 10. -/
theorem scalar_log_bound (x : ℝ) (hx : x ∈ Set.Icc (0 : ℝ) 1) :
    x ≤ 2 * Real.log (1 + x) := by sorry

end GenEllipPot.Potential

Source

Hamidi & Bayati, The Elliptical Potential Lemma for General Distributions with an Application to Linear Thompson Sampling, arXiv:2102.07987v3, p. 10, proof of Theorem 2.1, before (A.2)

Human review

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

View graph