Lean module · Foundations
BanditRLProof.Algorithms.CUCBOracleMeasurable
Source bounded smoothness produces score continuity and measurable oracle events; no extra score-measurability assumption is added to the model.
Module map
Imports
BanditRLProof.Algorithms.CUCBSourceModel
Imported by
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.CUCB.SourceModel.continuous_score
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.continuous_scoreReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem continuous_score (a : A) : Continuous (fun v => S.score v a)
theorem
BanditRLProof.CUCB.SourceModel.continuous_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.SourceModel.continuous_optimumReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem continuous_optimum : Continuous (scoreOptimum S.score)
theorem
BanditRLProof.CUCB.SourceModel.measurable_joint_score
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.measurable_joint_scoreReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem measurable_joint_score : Measurable (fun p : Input m × A => S.score p.1 p.2)
def
BanditRLProof.CUCB.SourceModel.oracleSuccess
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.oracleSuccessReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
def oracleSuccess : Set (Input m × A)
theorem
BanditRLProof.CUCB.SourceModel.measurableSet_oracleSuccess
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.measurableSet_oracleSuccessReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem measurableSet_oracleSuccess : MeasurableSet S.oracleSuccess
theorem
BanditRLProof.CUCB.SourceModel.measurableSet_path_oracleSuccess
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.measurableSet_path_oracleSuccessReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem measurableSet_path_oracleSuccess (n : ℕ) : MeasurableSet {Y : ℕ → Round A m | (oracleInput (fun t => (Y t).2) n, (Y n).1)∈S.oracleSuccess}