BanditRLProof.ConcentrationConfidenceSchedule

The geometric confidence schedule `delta / 2 / 2^n`.

noncomputable def geometricConfidenceShare (delta : Real) (n : Nat) : Real

Every geometric confidence share is positive when its outer budget is.

theorem geometricConfidenceShare_pos {delta : Real} (hdelta : 0 < delta) (n : Nat) : 0 < geometricConfidenceShare delta n

The ENNReal masses of the geometric confidence shares sum exactly to the outer budget.

theorem tsum_ofReal_geometricConfidenceShare {delta : Real} (hdelta : 0 <= delta) : ∑' n, ENNReal.ofReal (geometricConfidenceShare delta n) = ENNReal.ofReal delta

Positive telescoping weight `1 / ((n+1)(n+2))`. Unlike the geometric weight, its reciprocal grows only polynomially in time.

noncomputable def telescopingConfidenceWeight (n : Nat) : Real

The telescoping weight is a difference of consecutive reciprocals.

theorem telescopingConfidenceWeight_eq_sub (n : Nat) : telescopingConfidenceWeight n = 1 / (((n + 1 : Nat) : Real)) - 1 / (((n + 2 : Nat) : Real))

Exact finite partial sum of the telescoping weights.

theorem sum_range_telescopingConfidenceWeight (n : Nat) : (Finset.range n).sum telescopingConfidenceWeight = 1 - 1 / (((n + 1 : Nat) : Real))

Every telescoping confidence weight is nonnegative.

theorem telescopingConfidenceWeight_nonneg (n : Nat) : 0 <= telescopingConfidenceWeight n

The telescoping weights sum exactly to one.

theorem hasSum_telescopingConfidenceWeight : HasSum telescopingConfidenceWeight 1

Time-`n` confidence share `delta / ((n+1)(n+2))`.

noncomputable def telescopingConfidenceShare (delta : Real) (n : Nat) : Real

Display the telescoping share as the intended quotient.

theorem telescopingConfidenceShare_eq_div (delta : Real) (n : Nat) : telescopingConfidenceShare delta n = delta / (((n + 1 : Nat) : Real) * ((n + 2 : Nat) : Real))

Every telescoping confidence share is positive when its outer budget is.

theorem telescopingConfidenceShare_pos {delta : Real} (hdelta : 0 < delta) (n : Nat) : 0 < telescopingConfidenceShare delta n

The ENNReal masses of the telescoping confidence shares sum exactly to the outer budget.

theorem tsum_ofReal_telescopingConfidenceShare {delta : Real} (hdelta : 0 <= delta) : ∑' n, ENNReal.ofReal (telescopingConfidenceShare delta n) = ENNReal.ofReal delta