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

Actual reward and true-score expectations on every horizon of the same CUCB trajectory. The joint action/feedback distribution is retained.

Module map

Declarations
8
Placeholders
0

Imports

BanditRLProof.Algorithms.CUCBRewardKernel

Imported by

BanditRLProof, BanditRLProof.Algorithms.CUCBRegretDecomposition

Declarations

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

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

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

theorem integrable_actual_reward (n : ℕ) : Integrable (fun Y : ℕ → Round A m => (Y n).2.2.2) (cucbTrajectory S.oracle M.environment)
Source line 11 Chapter context: Foundations
theorem BanditRLProof.CUCB.SourceModel.actual_reward_expectation 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.actual_reward_expectation

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

theorem actual_reward_expectation (n : ℕ) : (∫Y : ℕ → Round A m, (Y n).2.2.2 ∂cucbTrajectory S.oracle M.environment)= ∫Y : ℕ → Round A m, S.score M.trueInput (Y n).1 ∂cucbTrajectory S.oracle M.environment
Source line 37 Chapter context: Foundations
theorem BanditRLProof.CUCB.SourceModel.cumulative_actual_reward_expectation 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.cumulative_actual_reward_expectation

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

theorem cumulative_actual_reward_expectation (n : ℕ) : (∫Y : ℕ → Round A m, ∑t∈Finset.range n, (Y t).2.2.2 ∂cucbTrajectory S.oracle M.environment)= ∫Y : ℕ → Round A m, ∑t∈Finset.range n, S.score M.trueInput (Y t).1 ∂cucbTrajectory S.oracle M.environment
Source line 68 Chapter context: Foundations
def BanditRLProof.CUCB.SourceModel.approximationRegret 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

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

noncomputable def approximationRegret (n : ℕ) : ℝ
Source line 77 Chapter context: Foundations
theorem BanditRLProof.CUCB.SourceModel.approximationRegret_zero 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_zero

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

theorem approximationRegret_zero : S.approximationRegret 0=0
Source line 82 Chapter context: Foundations
theorem BanditRLProof.CUCB.SourceModel.approximationRegret_eq_mean 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_eq_mean

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

theorem approximationRegret_eq_mean (n : ℕ) : S.approximationRegret n=(n:ℝ)*S.alpha*S.beta*scoreOptimum S.score M.trueInput- ∫Y : ℕ → Round A m, ∑t∈Finset.range n, S.score M.trueInput (Y t).1 ∂cucbTrajectory S.oracle M.environment
Source line 85 Chapter context: Foundations
theorem BanditRLProof.CUCB.SourceModel.integrable_actual_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 identitydeclaration:BanditRLProof.CUCB.SourceModel.integrable_actual_gap

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

theorem integrable_actual_gap (t : ℕ) : Integrable (fun Y : ℕ → Round A m => S.gap (Y t).1) (cucbTrajectory S.oracle M.environment)
Source line 91 Chapter context: Foundations
theorem BanditRLProof.CUCB.SourceModel.approximationRegret_eq_gap_sum 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 identitydeclaration:BanditRLProof.CUCB.SourceModel.approximationRegret_eq_gap_sum

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

theorem approximationRegret_eq_gap_sum (n : ℕ) : S.approximationRegret n = (∫Y : ℕ → Round A m, ∑t∈Finset.range n, S.gap (Y t).1 ∂cucbTrajectory S.oracle M.environment)- (n:ℝ)*S.alpha*(1-S.beta)*scoreOptimum S.score M.trueInput
Source line 97 Chapter context: Foundations