Lean module · Foundations

BanditRLProof.Algorithms.CUCBFiniteSourceExample

Concrete nonlinear score and input-dependent maximizing oracle for the finite noisy feedback model. Ties choose the inferior true-reward action.

Module map

Source: BanditRLProof/Algorithms/CUCBFiniteSourceExample.lean
Teaching chapter: 1. Finite bandits, traces, and regret
Declarations: 23
Placeholders: 0

Imports

BanditRLProof.Algorithms.CUCBFiniteExample, BanditRLProof.Algorithms.CUCBPolynomialRegret

Imported by

BanditRLProof, BanditRLProof.Algorithms.CUCBFiniteDeterministicExample

Declarations

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

def BanditRLProof.CUCB.FiniteExample.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.FiniteExample.score

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

def score (v : Input 3) (a : Bool) : ℝ

Source line 11 Chapter context: Foundations

def BanditRLProof.CUCB.FiniteExample.choose 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.choose

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

noncomputable def choose (v : Input 3) : Bool

Source line 13 Chapter context: Foundations

theorem BanditRLProof.CUCB.FiniteExample.measurable_choose 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.measurable_choose

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

theorem measurable_choose : Measurable choose

Source line 16 Chapter context: Foundations

theorem BanditRLProof.CUCB.FiniteExample.choose_max 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.choose_max

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

theorem choose_max (v : Input 3) : scoreOptimum score v≤score v (choose v)

Source line 23 Chapter context: Foundations

theorem BanditRLProof.CUCB.FiniteExample.product_smooth 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.product_smooth

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

theorem product_smooth (x y u v : UnitOutcome) (L : ℝ) (hL : 0≤L) (hx : |(x:ℝ)-u|≤L) (hy : |(y:ℝ)-v|≤L) : |(x:ℝ)*y-(u:ℝ)*v|≤2*L

Source line 32 Chapter context: Foundations

def BanditRLProof.CUCB.FiniteExample.source 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.source

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

noncomputable def source : SourceModel model where

Source line 48 Chapter context: Foundations

theorem BanditRLProof.CUCB.FiniteExample.trigger_value 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.trigger_value

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

theorem trigger_value (a : Bool) (i : Fin 3) : model.triggerProbability a i=if i∈selected a then 1 else 1/2

Source line 83 Chapter context: Foundations

theorem BanditRLProof.CUCB.FiniteExample.minTrigger_value 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.minTrigger_value

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

theorem minTrigger_value (i : Fin 3) : model.minTrigger i=if i=1 then 1 else 1/2

Source line 89 Chapter context: Foundations

theorem BanditRLProof.CUCB.FiniteExample.globalMinTrigger_value 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.globalMinTrigger_value

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

theorem globalMinTrigger_value : model.globalMinTrigger=1/2

Source line 107 Chapter context: Foundations

theorem BanditRLProof.CUCB.FiniteExample.true_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.FiniteExample.true_score

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

theorem true_score (a : Bool) : score model.trueInput a=if a then 3/8 else 1/8

Source line 116 Chapter context: Foundations

theorem BanditRLProof.CUCB.FiniteExample.true_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.FiniteExample.true_optimum

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

theorem true_optimum : scoreOptimum score model.trueInput=3/8

Source line 119 Chapter context: Foundations

theorem BanditRLProof.CUCB.FiniteExample.max_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.FiniteExample.max_gap

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

theorem max_gap : maxPositiveGap source.score model.trueInput source.alpha=1/4

Source line 127 Chapter context: Foundations

theorem BanditRLProof.CUCB.FiniteExample.choose_initial 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.choose_initial

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

theorem choose_initial : choose (initialInput 3)=false

Source line 139 Chapter context: Foundations

theorem BanditRLProof.CUCB.FiniteExample.initial_action_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.FiniteExample.initial_action_gap

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

theorem initial_action_gap : source.gap (choose (initialInput 3))=1/4

Source line 142 Chapter context: Foundations

theorem BanditRLProof.CUCB.FiniteExample.probabilistic_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.probabilistic_regret

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

theorem probabilistic_regret (H : ℕ) (hH : 1≤H) : source.approximationRegret H≤ 4*(72*Real.log (H:ℝ))^((1:ℝ)/2)*(H:ℝ)^((1:ℝ)/2)+ (1+Real.pi^2/2)*(3/4)+30*Real.log (H:ℝ)

Source line 147 Chapter context: Foundations

def BanditRLProof.CUCB.FiniteExample.randomizedSource 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.randomizedSource

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

noncomputable def randomizedSource : SourceModel model

Source line 160 Chapter context: Foundations

theorem BanditRLProof.CUCB.FiniteExample.randomized_action_mass 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.randomized_action_mass

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

theorem randomized_action_mass (v : Input 3) (a : Bool) : randomizedSource.oracle v {a}=(1/2:ENNReal)

Source line 177 Chapter context: Foundations

theorem BanditRLProof.CUCB.FiniteExample.randomized_probabilistic_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.randomized_probabilistic_regret

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

theorem randomized_probabilistic_regret (H : ℕ) (hH : 1≤H) : randomizedSource.approximationRegret H≤ 4*(72*Real.log (H:ℝ))^((1:ℝ)/2)*(H:ℝ)^((1:ℝ)/2)+ (1+Real.pi^2/2)*(3/4)+30*Real.log (H:ℝ)

Source line 183 Chapter context: Foundations

def BanditRLProof.CUCB.FiniteExample.noBadSource 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.noBadSource

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

noncomputable def noBadSource : SourceModel model

Source line 197 Chapter context: Foundations

theorem BanditRLProof.CUCB.FiniteExample.no_bad_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.no_bad_regret

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

theorem no_bad_regret (H : ℕ) : noBadSource.approximationRegret H≤0

Source line 211 Chapter context: Foundations

theorem BanditRLProof.CUCB.FiniteExample.first_action_law 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.first_action_law

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

theorem first_action_law : (cucbTrajectory source.oracle model.environment).map (fun Y => (Y 0).1)=Measure.dirac false

Source line 218 Chapter context: Foundations

theorem BanditRLProof.CUCB.FiniteExample.regret_one_positive 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.regret_one_positive

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

theorem regret_one_positive : source.approximationRegret 1=1/4

Source line 227 Chapter context: Foundations

theorem BanditRLProof.CUCB.FiniteExample.refined_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.refined_regret

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

theorem refined_regret (H : ℕ) (hH : 1≤H) : source.approximationRegret H≤(∑i:Fin 3,source.armRefinedTerm H i)+(1+Real.pi^2/2)*(3/4)

Source line 244 Chapter context: Foundations