Proof of Thm 3 (App. D.1), p. 46 — D_kl(P₁‖P₂) = −log(1 − δ) ≤ δ/(1 − δ) ≤ 2δ for δ ≤ ½

Proved

UniformDRO.LowerBound.kl_second_branch

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

inequalitykl-divergenceminimax-lower-boundp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $0 < \delta \le \tfrac12$ . Let $P_1$ be the point mass at $0$ (the law of $Z_1 \equiv 0$ ) and $P_2$ the law on $\{0, M\}$ with mass $\delta$ at $M$ . Then

D_{\mathrm{kl}}(P_1\|P_2) = -\log(1-\delta) \le \frac{\delta}{1-\delta} \le 2\delta .

This bounds the information in one observation for the $n^{-1/k_*}$ branch of Theorem 3.

Formalization Note. $D_{\mathrm{kl}}(P_1\|P_2)$ is the platform's Bernoulli relative entropy $d(0, \delta) = 0\cdot\log(0/\delta) + 1\cdot\log(1/(1-\delta))$ , where $0 \log 0 = 0$ is the standard convention. Stated as three conjuncts, one per relation of the chain.

Preamble

import Mathlib
import Definitions.Def_bernoulliRelativeEntropy
import Definitions.Def_UniformDRO_LowerBound_Setting

Formal statement

namespace UniformDRO.LowerBound

theorem kl_second_branch (δ : ℝ) (hδ : 0 < δ) (hδh : δ ≤ 1 / 2) :
    BanditAlgorithm.bernoulliRelativeEntropy 0 δ = -Real.log (1 - δ) ∧
      -Real.log (1 - δ) ≤ δ / (1 - δ) ∧ δ / (1 - δ) ≤ 2 * δ := by sorry

end UniformDRO.LowerBound

Source

Duchi & Namkoong, arXiv:1810.08750v6, proof of Theorem 3 (App. D.1), p. 46, second-branch KL display

Human review

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

View graph