Lean module · Foundations
BanditRLProof.Algorithms.CUCBFiniteDeterministicExample
Deterministic-trigger recovery of the same noisy three-arm example.
Module map
Imports
BanditRLProof.Algorithms.CUCBFiniteSourceExample
Imported by
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
def
BanditRLProof.CUCB.FiniteExample.fullFeedback
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.FiniteExample.fullFeedbackReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
def fullFeedback (a : Bool) (x : Sample) : Feedback 3
def
BanditRLProof.CUCB.FiniteExample.fullEnvironment
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.FiniteExample.fullEnvironmentReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def fullEnvironment : Kernel Bool (Feedback 3) where
theorem
BanditRLProof.CUCB.FiniteExample.full_observed
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.FiniteExample.full_observedReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem full_observed (a : Bool) (i : Fin 3) : fullEnvironment a (observedSet i)=1
theorem
BanditRLProof.CUCB.FiniteExample.full_compatible
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.FiniteExample.full_compatibleReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem full_compatible (a : Bool) (i : Fin 3) : ObservationCompatible (fullEnvironment a) (law i) i
theorem
BanditRLProof.CUCB.FiniteExample.full_reward_integrable
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.FiniteExample.full_reward_integrableReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem full_reward_integrable (a : Bool) : Integrable (fun z => z.2.2) (fullEnvironment a)
theorem
BanditRLProof.CUCB.FiniteExample.full_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.FiniteExample.full_reward_nonnegReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem full_reward_nonneg (a : Bool) : ∀ᵐ z ∂fullEnvironment a, 0≤z.2.2
def
BanditRLProof.CUCB.FiniteExample.fullModel
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.FiniteExample.fullModelReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def fullModel : FeedbackModel Bool 3 where
theorem
BanditRLProof.CUCB.FiniteExample.full_expected_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.FiniteExample.full_expected_rewardReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem full_expected_reward (a : Bool) : fullModel.expectedReward a=model.expectedReward a
def
BanditRLProof.CUCB.FiniteExample.fullSource
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.FiniteExample.fullSourceReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def fullSource : SourceModel fullModel where
theorem
BanditRLProof.CUCB.FiniteExample.full_minTrigger
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.FiniteExample.full_minTriggerReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem full_minTrigger (i : Fin 3) : fullModel.minTrigger i=1
theorem
BanditRLProof.CUCB.FiniteExample.full_globalMinTrigger
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.FiniteExample.full_globalMinTriggerReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem full_globalMinTrigger : fullModel.globalMinTrigger=1
theorem
BanditRLProof.CUCB.FiniteExample.deterministic_regret
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.FiniteExample.deterministic_regretReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem deterministic_regret (H : ℕ) (hH : 1≤H) : fullSource.approximationRegret H≤ 4*(18*Real.log (H:ℝ))^((1:ℝ)/2)*(H:ℝ)^((1:ℝ)/2)+(1+Real.pi^2/3)*(3/4)