Lean module · Foundations
BanditRLProof.Algorithms.CUCBRewardKernel
Actual reward integrability and round expectations from the primitive nonnegative L1 reward law. No bound on realized rewards is imposed.
Module map
Imports
BanditRLProof.Algorithms.CUCBOracleSuccess
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.integrable_trueScore_comp
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.integrable_trueScore_compReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem integrable_trueScore_comp {Ω : Type*} [MeasurableSpace Ω] (ν : Measure Ω) [IsProbabilityMeasure ν] (g : Ω → A) (hg : Measurable g) : Integrable (fun ω => S.score M.trueInput (g ω)) ν
theorem
BanditRLProof.CUCB.SourceModel.environment_norm_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 identity
declaration:BanditRLProof.CUCB.SourceModel.environment_norm_rewardReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem environment_norm_reward (a : A) : (∫z, ‖z.2.2‖ ∂M.environment a)=S.score M.trueInput a
theorem
BanditRLProof.CUCB.SourceModel.integrable_round_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 identity
declaration:BanditRLProof.CUCB.SourceModel.integrable_round_rewardReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem integrable_round_reward (v : Input m) : Integrable (fun z : Round A m => z.2.2.2) (roundKernel S.oracle M.environment v)
theorem
BanditRLProof.CUCB.SourceModel.round_reward_nonneg
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.round_reward_nonnegReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem round_reward_nonneg (v : Input m) : ∀ᵐ z ∂roundKernel S.oracle M.environment v, 0≤z.2.2.2
theorem
BanditRLProof.CUCB.SourceModel.integral_round_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 identity
declaration:BanditRLProof.CUCB.SourceModel.integral_round_rewardReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem integral_round_reward (v : Input m) : (∫z : Round A m, z.2.2.2 ∂roundKernel S.oracle M.environment v)= ∫a, S.score M.trueInput a ∂S.oracle v
theorem
BanditRLProof.CUCB.SourceModel.integral_round_norm_reward_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 identity
declaration:BanditRLProof.CUCB.SourceModel.integral_round_norm_reward_leReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem integral_round_norm_reward_le (v : Input m) : (∫z : Round A m, ‖z.2.2.2‖ ∂roundKernel S.oracle M.environment v)≤ scoreOptimum S.score M.trueInput
theorem
BanditRLProof.CUCB.SourceModel.integral_round_reward_eq_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.integral_round_reward_eq_scoreReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem integral_round_reward_eq_score (v : Input m) : (∫z : Round A m, z.2.2.2 ∂roundKernel S.oracle M.environment v)= ∫z : Round A m, S.score M.trueInput z.1 ∂roundKernel S.oracle M.environment v
theorem
BanditRLProof.CUCB.SourceModel.integrable_joint_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 identity
declaration:BanditRLProof.CUCB.SourceModel.integrable_joint_rewardReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem integrable_joint_reward {Ω : Type*} [MeasurableSpace Ω] (ν : Measure Ω) [IsProbabilityMeasure ν] (g : Ω → Input m) (hg : Measurable g) : Integrable (fun p : Ω × Round A m => p.2.2.2.2) (ν ⊗ₘ (roundKernel S.oracle M.environment).comap g hg)
theorem
BanditRLProof.CUCB.SourceModel.integral_joint_reward_eq_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.integral_joint_reward_eq_scoreReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem integral_joint_reward_eq_score {Ω : Type*} [MeasurableSpace Ω] (ν : Measure Ω) [IsProbabilityMeasure ν] (g : Ω → Input m) (hg : Measurable g) : (∫p : Ω × Round A m, p.2.2.2.2 ∂(ν ⊗ₘ (roundKernel S.oracle M.environment).comap g hg))= ∫p : Ω × Round A m, S.score M.trueInput p.2.1 ∂(ν ⊗ₘ (roundKernel S.oracle M.environment).comap g hg)