Lean module · Foundations
BanditRLProof.Algorithms.CUCBSourceModel
The frozen full triggered-CUCB source model: arbitrary finite feasible superarms, nonlinear smooth reward scores and randomized approximation oracle. No confidence, counting or regret premise is part of this structure.
Module map
Imports
BanditRLProof.Algorithms.CUCBFeedbackModel
Imported by
BanditRLProof, BanditRLProof.Algorithms.CUCBFiniteExample, BanditRLProof.Algorithms.CUCBGapInverse, BanditRLProof.Algorithms.CUCBImpossibleCase, BanditRLProof.Algorithms.CUCBOracleMeasurable, BanditRLProof.Algorithms.CUCBThresholdTail
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
def
BanditRLProof.CUCB.scoreOptimum
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 identity
declaration:BanditRLProof.CUCB.scoreOptimumReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def scoreOptimum (score : Input m → A → ℝ) (v : Input m) : ℝ
theorem
BanditRLProof.CUCB.score_le_optimum
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 identity
declaration:BanditRLProof.CUCB.score_le_optimumReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem score_le_optimum (score : Input m → A → ℝ) (v : Input m) (a : A) : score v a≤scoreOptimum score v
def
BanditRLProof.CUCB.sourceGap
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 identity
declaration:BanditRLProof.CUCB.sourceGapReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def sourceGap (score : Input m → A → ℝ) (v : Input m) (α : ℝ) (a : A) : ℝ
def
BanditRLProof.CUCB.maxPositiveGap
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 identity
declaration:BanditRLProof.CUCB.maxPositiveGapReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def maxPositiveGap (score : Input m → A → ℝ) (v : Input m) (α : ℝ) : ℝ
theorem
BanditRLProof.CUCB.gap_le_maxPositiveGap
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 identity
declaration:BanditRLProof.CUCB.gap_le_maxPositiveGapReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem gap_le_maxPositiveGap (score : Input m → A → ℝ) (v : Input m) (α : ℝ) (a : A) : sourceGap score v α a≤maxPositiveGap score v α
structure
BanditRLProof.CUCB.SourceModel
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
Indexed settings: Combinatorial bandits
Canonical node identity
declaration:BanditRLProof.CUCB.SourceModelReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
structure SourceModel (M : FeedbackModel A m) where
def
BanditRLProof.CUCB.SourceModel.gap
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 identity
declaration:BanditRLProof.CUCB.SourceModel.gapReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def gap (a : A) : ℝ
def
BanditRLProof.CUCB.SourceModel.bad
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 identity
declaration:BanditRLProof.CUCB.SourceModel.badReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def bad (a : A) : Bool
def
BanditRLProof.CUCB.SourceModel.inverseGap
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 identity
declaration:BanditRLProof.CUCB.SourceModel.inverseGapReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def inverseGap (a : A) : ℝ
theorem
BanditRLProof.CUCB.SourceModel.inverseGap_spec
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 identity
declaration:BanditRLProof.CUCB.SourceModel.inverseGap_specReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem inverseGap_spec (a : A) (ha : 0<S.gap a) : 0<S.inverseGap a ∧ S.modulus (S.inverseGap a)=S.gap a
def
BanditRLProof.CUCB.SourceModel.chargeData
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 identity
declaration:BanditRLProof.CUCB.SourceModel.chargeDataReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def chargeData : ChargeData A m
theorem
BanditRLProof.CUCB.SourceModel.chargeData_sufficient
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
Indexed settings: Combinatorial bandits
Canonical node identity
declaration:BanditRLProof.CUCB.SourceModel.chargeData_sufficientReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem chargeData_sufficient (N : Fin m → ℕ) (a : A) (i : Fin m) (h : S.chargeData.choose N a=some i) (n : ℕ) (hi : samplingThreshold n (S.inverseGap a) (M.minTrigger i)<N i) : ∀j∈M.possible a, samplingThreshold n (S.inverseGap a) (M.minTrigger j)<N j
theorem
BanditRLProof.CUCB.SourceModel.optimum_monotone
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 identity
declaration:BanditRLProof.CUCB.SourceModel.optimum_monotoneReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem optimum_monotone (v w : Input m) (h : ∀i, (v i:ℝ)≤(w i:ℝ)) : scoreOptimum S.score v≤scoreOptimum S.score w
theorem
BanditRLProof.CUCB.SourceModel.maxPositiveGap_eq_zero_of_no_bad
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 identity
declaration:BanditRLProof.CUCB.SourceModel.maxPositiveGap_eq_zero_of_no_badReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem maxPositiveGap_eq_zero_of_no_bad (h : ∀a, S.gap a≤0) : maxPositiveGap S.score M.trueInput S.alpha=0
theorem
BanditRLProof.CUCB.SourceModel.counters_zero_of_no_bad
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 identity
declaration:BanditRLProof.CUCB.SourceModel.counters_zero_of_no_badReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem counters_zero_of_no_bad (h : ∀a, S.gap a≤0) (actions : ℕ → A) (n : ℕ) (i : Fin m) : S.chargeData.counters actions n i=0