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.CUCBGapCutoff

Actual gap cutoff bound used by the distribution-independent CUCB proof. The baseline is paid once per round, not once per arm threshold crossing.

Module map

Declarations
6
Placeholders
0

Imports

BanditRLProof.Algorithms.CUCBRefinedRegret, BanditRLProof.FiniteGapCutoff

Imported by

BanditRLProof, BanditRLProof.Algorithms.CUCBFiniteConcavity, BanditRLProof.Algorithms.CUCBPolynomialThreshold

Declarations

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

theorem BanditRLProof.CUCB.SourceModel.card_underChargeTimes_le 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.card_underChargeTimes_le

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

theorem card_underChargeTimes_le (H : ℕ) (actions : ℕ → A) (i : Fin m) : (S.underChargeTimes H actions i).card≤S.chargeData.counters actions H i
Source line 12 Chapter context: Foundations
theorem BanditRLProof.CUCB.SourceModel.sum_card_underChargeTimes_le 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_card_underChargeTimes_le

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

theorem sum_card_underChargeTimes_le (H : ℕ) (actions : ℕ → A) : (∑i:Fin m, ((S.underChargeTimes H actions i).card:ℝ))≤H
Source line 24 Chapter context: Foundations
theorem BanditRLProof.CUCB.SourceModel.underChargeWeight_le_cutoff 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_cutoff

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

theorem underChargeWeight_le_cutoff (H : ℕ) (hH : 1≤H) (actions : ℕ → A) (i : Fin m) (a : ℝ) (ha : a∈S.gapDomain) : S.underChargeWeight H actions i≤ a*((S.underChargeTimes H actions i).card:ℝ)+ (∫x in a..maxPositiveGap S.score M.trueInput S.alpha, S.gapThreshold H (M.minTrigger i) x)+ (maxPositiveGap S.score M.trueInput S.alpha-a)
Source line 34 Chapter context: Foundations
theorem BanditRLProof.CUCB.SourceModel.sum_underSampledGap_le_cutoff 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_cutoff

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

theorem sum_underSampledGap_le_cutoff (H : ℕ) (hH : 1≤H) (actions : ℕ → A) (a : ℝ) (ha : a∈S.gapDomain) : (∑t∈Finset.range H, S.underSampledGap H (S.chargeData.counters actions t) (actions t))≤ (H:ℝ)*a+(∑i:Fin m, ∫x in a..maxPositiveGap S.score M.trueInput S.alpha, S.gapThreshold H (M.minTrigger i) x)+(m:ℝ)*maxPositiveGap S.score M.trueInput S.alpha
Source line 47 Chapter context: Foundations
theorem BanditRLProof.CUCB.SourceModel.approximationRegret_le_gap_cutoff 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.approximationRegret_le_gap_cutoff

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

theorem approximationRegret_le_gap_cutoff (H : ℕ) (hH : 1≤H) (a : ℝ) (ha : a∈S.gapDomain) : S.approximationRegret H≤(H:ℝ)*a+ (∑i:Fin m, ∫x in a..maxPositiveGap S.score M.trueInput S.alpha, S.gapThreshold H (M.minTrigger i) x)+ (1+(2+(if M.globalMinTrigger<1 then 1 else 0))*Real.pi^2/6)* (m:ℝ)*maxPositiveGap S.score M.trueInput S.alpha
Source line 62 Chapter context: Foundations
theorem BanditRLProof.CUCB.SourceModel.approximationRegret_le_large_cutoff 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.approximationRegret_le_large_cutoff

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

theorem approximationRegret_le_large_cutoff (H : ℕ) (a : ℝ) (ha : maxPositiveGap S.score M.trueInput S.alpha≤a) : S.approximationRegret H≤(H:ℝ)*a+ (2+(if M.globalMinTrigger<1 then 1 else 0))*(m:ℝ)* maxPositiveGap S.score M.trueInput S.alpha*Real.pi^2/6
Source line 77 Chapter context: Foundations