Lean module · Foundations

BanditRLProof.Algorithms.CUCBFiniteExample

A finite noisy triggered-feedback witness. Independent primitive coordinates produce three Bernoulli arms and a fresh extra-trigger coin.

Module map

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

Imports

BanditRLProof.Algorithms.CUCBSourceModel, BanditRLProof.Algorithms.ThompsonRecursiveSampler

Imported by

BanditRLProof, BanditRLProof.Algorithms.CUCBFiniteSourceExample

Declarations

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

abbrev BanditRLProof.CUCB.FiniteExample.Sample 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.Sample

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

abbrev Sample

Source line 12 Chapter context: Foundations

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

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

noncomputable def sampleLaw : Measure Sample

Source line 13 Chapter context: Foundations

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

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

def bit (b : Bool) : UnitOutcome

Source line 16 Chapter context: Foundations

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

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

def outcome (x : Sample) (i : Fin 3) : UnitOutcome

Source line 17 Chapter context: Foundations

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

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

def selected (a : Bool) : Finset (Fin 3)

Source line 20 Chapter context: Foundations

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

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

def feedback (a : Bool) (x : Sample) : Feedback 3

Source line 21 Chapter context: Foundations

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

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

noncomputable def environment : Kernel Bool (Feedback 3) where

Source line 26 Chapter context: Foundations

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

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

noncomputable def law (i : Fin 3) : Measure UnitOutcome

Source line 33 Chapter context: Foundations

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

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

theorem sampleLaw_apply (s : Set Sample) : sampleLaw s=∑x:Sample, if x∈s then (1/64:ENNReal) else 0

Source line 39 Chapter context: Foundations

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

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

theorem environment_apply (a : Bool) (s : Set (Feedback 3)) (hs : MeasurableSet s) : environment a s=∑x:Sample, if feedback a x∈s then (1/64:ENNReal) else 0

Source line 45 Chapter context: Foundations

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

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

theorem law_apply (i : Fin 3) (s : Set UnitOutcome) (hs : MeasurableSet s) : law i s=∑x:Sample, if outcome x i∈s then (1/64:ENNReal) else 0

Source line 51 Chapter context: Foundations

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

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

theorem environment_observed (a : Bool) (i : Fin 3) : environment a (observedSet i)=if i∈selected a then 1 else 1/2

Source line 56 Chapter context: Foundations

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

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

theorem observation_compatible (a : Bool) (i : Fin 3) : ObservationCompatible (environment a) (law i) i

Source line 66 Chapter context: Foundations

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

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

theorem reward_integrable (a : Bool) : Integrable (fun z => z.2.2) (environment a)

Source line 83 Chapter context: Foundations

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

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

theorem reward_nonneg (a : Bool) : ∀ᵐ z ∂environment a, 0≤z.2.2

Source line 88 Chapter context: Foundations

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

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

noncomputable def model : FeedbackModel Bool 3 where

Source line 95 Chapter context: Foundations

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

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

theorem mean_value (i : Fin 3) : marginalMean (law i)=if i=0 then 1/4 else if i=1 then 1/2 else 3/4

Source line 125 Chapter context: Foundations

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

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

theorem expected_reward (a : Bool) : model.expectedReward a=if a then 3/8 else 1/8

Source line 133 Chapter context: Foundations

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

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

theorem law_one_mass (i : Fin 3) : (law i {bit true}).toReal=if i=0 then 1/4 else if i=1 then 1/2 else 3/4

Source line 140 Chapter context: Foundations

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

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

theorem noisy_each_arm (i : Fin 3) : 0<(law i {bit true}).toReal ∧ (law i {bit true}).toReal<1

Source line 149 Chapter context: Foundations

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

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

theorem selected_size (a : Bool) : (selected a).card=2

Source line 153 Chapter context: Foundations