BanditRLlib
Lean gate passed before this site build; local proof declarations are shown as compiled.Lean-verified build · exact declarations linked.

Lean module · Foundations

BanditRLProof.Algorithms.CUCBUnderCountIntegral

Refined integral bound for the actual under-sampled charge weights.

Module map

Declarations
7
Placeholders
0

Imports

BanditRLProof.Algorithms.CUCBUnderCount, BanditRLProof.FiniteGapLayerCake

Imported by

BanditRLProof, BanditRLProof.Algorithms.CUCBRefinedRegret

Declarations

Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.

def BanditRLProof.CUCB.SourceModel.underChargeWeight Compiled

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

Used in these reading views: Bandit Book

1. Finite bandits, traces, and regret

Canonical node identitydeclaration:BanditRLProof.CUCB.SourceModel.underChargeWeight

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

noncomputable def underChargeWeight (H : ℕ) (actions : ℕ → A) (i : Fin m) : ℝ
Source line 11 Chapter context: Foundations
theorem BanditRLProof.CUCB.SourceModel.underChargeWeight_le_refined Compiled

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

Used in these reading views: Bandit Book

1. Finite bandits, traces, and regret

Canonical node identitydeclaration:BanditRLProof.CUCB.SourceModel.underChargeWeight_le_refined

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem underChargeWeight_le_refined (H : ℕ) (hH : 1≤H) (actions : ℕ → A) (i : Fin m) (hi : (S.badActions i).Nonempty) : S.underChargeWeight H actions i ≤ S.minBadGap i hi*S.gapThreshold H (M.minTrigger i) (S.minBadGap i hi)+ (∫x in S.minBadGap i hi..S.maxBadGap i hi, S.gapThreshold H (M.minTrigger i) x)+ S.maxBadGap i hi
Source line 14 Chapter context: Foundations
def BanditRLProof.CUCB.SourceModel.armRefinedTerm Compiled

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

Used in these reading views: Bandit Book

1. Finite bandits, traces, and regret

Canonical node identitydeclaration:BanditRLProof.CUCB.SourceModel.armRefinedTerm

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

noncomputable def armRefinedTerm (H : ℕ) (i : Fin m) : ℝ
Source line 30 Chapter context: Foundations
theorem BanditRLProof.CUCB.SourceModel.underChargeWeight_le_armRefinedTerm Compiled

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

Used in these reading views: Bandit Book

1. Finite bandits, traces, and regret

Canonical node identitydeclaration:BanditRLProof.CUCB.SourceModel.underChargeWeight_le_armRefinedTerm

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem underChargeWeight_le_armRefinedTerm (H : ℕ) (hH : 1≤H) (actions : ℕ → A) (i : Fin m) : S.underChargeWeight H actions i≤ S.armRefinedTerm H i+maxPositiveGap S.score M.trueInput S.alpha
Source line 37 Chapter context: Foundations
theorem BanditRLProof.CUCB.SourceModel.underSampledGap_eq_sum_arms Compiled

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

Used in these reading views: Bandit Book

1. Finite bandits, traces, and regret

Canonical node identitydeclaration:BanditRLProof.CUCB.SourceModel.underSampledGap_eq_sum_arms

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem underSampledGap_eq_sum_arms (H : ℕ) (N : Fin m → ℕ) (a : A) : S.underSampledGap H N a=∑i:Fin m, if S.chargeData.choose N a=some i ∧ (N i:ℝ)≤samplingThreshold H (S.inverseGap a) (M.minTrigger i) then S.gap a else 0
Source line 50 Chapter context: Foundations
theorem BanditRLProof.CUCB.SourceModel.sum_underSampledGap_eq_weights Compiled

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

Used in these reading views: Bandit Book

1. Finite bandits, traces, and regret

Canonical node identitydeclaration:BanditRLProof.CUCB.SourceModel.sum_underSampledGap_eq_weights

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem sum_underSampledGap_eq_weights (H : ℕ) (actions : ℕ → A) : (∑t∈Finset.range H, S.underSampledGap H (S.chargeData.counters actions t) (actions t))= ∑i:Fin m, S.underChargeWeight H actions i
Source line 75 Chapter context: Foundations
theorem BanditRLProof.CUCB.SourceModel.sum_underSampledGap_le_refined Compiled

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

Used in these reading views: Bandit Book

1. Finite bandits, traces, and regret

Canonical node identitydeclaration:BanditRLProof.CUCB.SourceModel.sum_underSampledGap_le_refined

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem sum_underSampledGap_le_refined (H : ℕ) (hH : 1≤H) (actions : ℕ → A) : (∑t∈Finset.range H, S.underSampledGap H (S.chargeData.counters actions t) (actions t))≤ (∑i:Fin m, S.armRefinedTerm H i)+(m:ℝ)*maxPositiveGap S.score M.trueInput S.alpha
Source line 85 Chapter context: Foundations