BanditRLProof.Algorithms.KLUCBBernoulli

The closed unit interval predicate used by every KL-UCB parameter.

def IsBernoulliParameter (p : Real) : Prop

The finite analytic Bernoulli relative-entropy expression. It is used only when the second parameter is strictly between zero and one.

noncomputable def bernoulliKLCore (p q : Real) : Real

Bernoulli relative entropy with exact support/endpoint conventions. parameters outside `[0,1]` have value `top`; `d(0,0)=d(1,1)=0`; `d(p,0)=top` for `p>0` and `d(p,1)=top` for `p<1`; otherwise the ordinary finite logarithmic expression is used.

noncomputable def bernoulliKL (p q : Real) : ENNReal

No declaration docstring is present; use the chapter context and exact statement below.

theorem bernoulliKL_nonneg (p q : Real) : 0 <= bernoulliKL p q

No declaration docstring is present; use the chapter context and exact statement below.

theorem bernoulliKL_eq_top_of_not_left {p q : Real} (hp : ¬ IsBernoulliParameter p) : bernoulliKL p q = ⊤

No declaration docstring is present; use the chapter context and exact statement below.

theorem bernoulliKL_eq_top_of_not_right {p q : Real} (hq : ¬ IsBernoulliParameter q) : bernoulliKL p q = ⊤

No declaration docstring is present; use the chapter context and exact statement below.

theorem bernoulliKL_zero_zero : bernoulliKL 0 0 = 0

No declaration docstring is present; use the chapter context and exact statement below.

theorem bernoulliKL_one_one : bernoulliKL 1 1 = 0

No declaration docstring is present; use the chapter context and exact statement below.

theorem bernoulliKL_right_zero {p : Real} (hp : IsBernoulliParameter p) : bernoulliKL p 0 = if p = 0 then 0 else ⊤

No declaration docstring is present; use the chapter context and exact statement below.

theorem bernoulliKL_right_one {p : Real} (hp : IsBernoulliParameter p) : bernoulliKL p 1 = if p = 1 then 0 else ⊤

No declaration docstring is present; use the chapter context and exact statement below.

theorem bernoulliKL_eq_top_right_zero {p : Real} (hp : IsBernoulliParameter p) (hp0 : p ≠ 0) : bernoulliKL p 0 = ⊤

No declaration docstring is present; use the chapter context and exact statement below.

theorem bernoulliKL_eq_top_right_one {p : Real} (hp : IsBernoulliParameter p) (hp1 : p ≠ 1) : bernoulliKL p 1 = ⊤

No declaration docstring is present; use the chapter context and exact statement below.

theorem bernoulliKL_zero_left_of_interior {q : Real} (hq0 : 0 < q) (hq1 : q < 1) : bernoulliKL 0 q = ENNReal.ofReal (Real.log (1 / (1 - q)))

No declaration docstring is present; use the chapter context and exact statement below.

theorem bernoulliKL_one_left_of_interior {q : Real} (hq0 : 0 < q) (hq1 : q < 1) : bernoulliKL 1 q = ENNReal.ofReal (Real.log (1 / q))

The finite Bernoulli expression vanishes on the diagonal away from the singular endpoints.

theorem bernoulliKLCore_self {p : Real} (hp0 : p ≠ 0) (hp1 : p ≠ 1) : bernoulliKLCore p p = 0

The analytic binary KL expression is the two-atom `klFun` integral.

theorem bernoulliKLCore_eq_klFun {p q : Real} (hq0 : q ≠ 0) (hq1 : q ≠ 1) : bernoulliKLCore p q = q * InformationTheory.klFun (p / q) + (1 - q) * InformationTheory.klFun ((1 - p) / (1 - q))

Nontrivial nonnegativity of the finite logarithmic expression. This is stronger than the order-theoretic nonnegativity of its `ENNReal` wrapper.

theorem bernoulliKLCore_nonneg {p q : Real} (hp : IsBernoulliParameter p) (hq0 : 0 < q) (hq1 : q < 1) : 0 <= bernoulliKLCore p q

Interior parameters expose the finite analytic expression without truncation: its real nonnegativity has already been proved.

theorem bernoulliKL_eq_of_interior {p q : Real} (hp : IsBernoulliParameter p) (hq0 : 0 < q) (hq1 : q < 1) : bernoulliKL p q = ENNReal.ofReal (bernoulliKLCore p q)

Algebraically expanded finite KL, convenient for differentiation in the second parameter.

noncomputable def bernoulliKLExpanded (p q : Real) : Real

No declaration docstring is present; use the chapter context and exact statement below.

theorem bernoulliKLCore_eq_expanded {p q : Real} (hp0 : p ≠ 0) (hp1 : p ≠ 1) (hq0 : q ≠ 0) (hq1 : q ≠ 1) : bernoulliKLCore p q = bernoulliKLExpanded p q

No declaration docstring is present; use the chapter context and exact statement below.

theorem hasDerivAt_bernoulliKLExpanded_right (p q : Real) (hq0 : q ≠ 0) (hq1 : q ≠ 1) : HasDerivAt (fun r => bernoulliKLExpanded p r) ((q - p) / (q * (1 - q))) q

A conservative binary Pinsker inequality. The constant `1/2` is weaker than the sharp natural-log constant `2`, but is sufficient to invert every KL-UCB confidence set without changing the KL score itself.

theorem half_sq_sub_le_bernoulliKLCore {p q : Real} (hp : IsBernoulliParameter p) (hq0 : 0 < q) (hq1 : q < 1) : (1 / 2 : Real) * (p - q) ^ 2 <= bernoulliKLCore p q

On an interior reference mean, binary KL is controlled by the squared deviation divided by the Bernoulli variance denominator. This is the bridge from the repository's bounded-reward empirical-mean tails to a genuine KL confidence event.

theorem bernoulliKLCore_le_sq_div {p q : Real} (hp : IsBernoulliParameter p) (hq0 : 0 < q) (hq1 : q < 1) : bernoulliKLCore p q <= (p - q) ^ 2 / (q * (1 - q))

No declaration docstring is present; use the chapter context and exact statement below.

theorem ennnreal_half_sq_sub_le_bernoulliKL {p q : Real} (hp : IsBernoulliParameter p) (hq0 : 0 < q) (hq1 : q < 1) : ENNReal.ofReal ((1 / 2 : Real) * (p - q) ^ 2) <= bernoulliKL p q

No declaration docstring is present; use the chapter context and exact statement below.

theorem bernoulliKL_le_of_sq_le {p q budget : Real} (hp : IsBernoulliParameter p) (hq0 : 0 < q) (hq1 : q < 1) (hsq : (p - q) ^ 2 / (q * (1 - q)) <= budget) : bernoulliKL p q <= ENNReal.ofReal budget

No declaration docstring is present; use the chapter context and exact statement below.

theorem bernoulliKL_self {p : Real} (hp : IsBernoulliParameter p) : bernoulliKL p p = 0

On the nonsingular right-parameter domain the finite expression is continuous. This is the local analytic regularity used by later inversion leaves; endpoint singularities remain in `ENNReal`.

theorem continuousAt_bernoulliKLCore_right (p q : Real) (hq0 : q ≠ 0) (hq1 : q ≠ 1) : ContinuousAt (fun r => bernoulliKLCore p r) q

KL confidence set at one empirical mean, pull count, and exploration budget.

def confidenceSet (empiricalMean : Real) (count : Nat) (budget : Real) : Set Real

The KL-UCB index is the supremum of its confidence set.

noncomputable def index (empiricalMean : Real) (count : Nat) (budget : Real) : Real

No declaration docstring is present; use the chapter context and exact statement below.

theorem confidenceSet_bddAbove (empiricalMean : Real) (count : Nat) (budget : Real) : BddAbove (confidenceSet empiricalMean count budget)

No declaration docstring is present; use the chapter context and exact statement below.

theorem mem_confidenceSet_self {p : Real} (hp : IsBernoulliParameter p) (count : Nat) {budget : Real} (hbudget : 0 <= budget) : p ∈ confidenceSet p count budget

Real finite-KL arithmetic is sufficient to establish exact membership in the `ENNReal` confidence set.

theorem mem_confidenceSet_of_natCast_mul_core_le {p q budget : Real} {count : Nat} (hp : IsBernoulliParameter p) (hq0 : 0 < q) (hq1 : q < 1) (hbudget : (count : Real) * bernoulliKLCore p q <= budget) : q ∈ confidenceSet p count budget

No declaration docstring is present; use the chapter context and exact statement below.

theorem natCast_mul_half_sq_sub_le_budget_of_mem {p q budget : Real} {count : Nat} (hp : IsBernoulliParameter p) (hq0 : 0 < q) (hq1 : q < 1) (hbudget : 0 <= budget) (hmem : q ∈ confidenceSet p count budget) : (count : Real) * ((1 / 2 : Real) * (p - q) ^ 2) <= budget

No declaration docstring is present; use the chapter context and exact statement below.

theorem confidenceSet_nonempty {p : Real} (hp : IsBernoulliParameter p) (count : Nat) {budget : Real} (hbudget : 0 <= budget) : (confidenceSet p count budget).Nonempty

No declaration docstring is present; use the chapter context and exact statement below.

theorem index_le_one {p : Real} (hp : IsBernoulliParameter p) (count : Nat) {budget : Real} (hbudget : 0 <= budget) : index p count budget <= 1

No declaration docstring is present; use the chapter context and exact statement below.

theorem index_nonneg {p : Real} (hp : IsBernoulliParameter p) (count : Nat) {budget : Real} (hbudget : 0 <= budget) : 0 <= index p count budget

No declaration docstring is present; use the chapter context and exact statement below.

theorem index_mem_Icc {p : Real} (hp : IsBernoulliParameter p) (count : Nat) {budget : Real} (hbudget : 0 <= budget) : index p count budget ∈ Set.Icc (0 : Real) 1

Zero empirical count makes every unit-interval parameter feasible. This is the explicit KL-UCB zero-count convention.

theorem mem_confidenceSet_zero_iff (p q budget : Real) (hbudget : 0 <= budget) : q ∈ confidenceSet p 0 budget ↔ IsBernoulliParameter q

No declaration docstring is present; use the chapter context and exact statement below.

theorem index_zero_count {p : Real} (hp : IsBernoulliParameter p) {budget : Real} (hbudget : 0 <= budget) : index p 0 budget = 1

Membership of the true mean implies KL optimism.

theorem le_index_of_mem_confidenceSet {p q : Real} {count : Nat} {budget : Real} (hq : q ∈ confidenceSet p count budget) : q <= index p count budget

A strict lower level below the supremum has a genuine feasible witness. No unproved claim that the supremum itself belongs to the set is used.

theorem exists_mem_confidenceSet_of_lt_index {p level : Real} {count : Nat} {budget : Real} (hp : IsBernoulliParameter p) (hbudget : 0 <= budget) (hlevel : level < index p count budget) : ∃ q ∈ confidenceSet p count budget, level < q