Lean module · Thompson sampling

BanditRLProof.Algorithms.ThompsonCanonicalSampler

This module constructs the one-step joint law obtained by sampling an environment/history pair from a Bayesian prior-likelihood model and then sampling an action from the canonical posterior pushed through a measurable best-action selector. The resulting probability-matching theorem has no separate pair-law or action-law premise.

Module map

Source: BanditRLProof/Algorithms/ThompsonCanonicalSampler.lean
Teaching chapter: 6. Thompson sampling and Bayesian regret
Declarations: 14
Placeholders: 0

Imports

BanditRLProof.Algorithms.Thompson

Imported by

BanditRLProof, BanditRLProof.Algorithms.ThompsonReferencePolicy

Declarations

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

def BanditRLProof.Thompson.canonicalActionKernel Compiled

The Thompson action kernel induced by Mathlib's canonical posterior.

Used in these reading views: Bandit Book

6. Thompson sampling and Bayesian regret

Canonical node identity

declaration:BanditRLProof.Thompson.canonicalActionKernel

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

noncomputable def canonicalActionKernel {History : Type u} {Env : Type v} {Action : Type w} [MeasurableSpace History] [MeasurableSpace Env] [StandardBorelSpace Env] [Nonempty Env] [MeasurableSpace Action] (prior : Measure Env) [IsProbabilityMeasure prior] (likelihood : ProbabilityTheory.Kernel Env History) [ProbabilityTheory.IsMarkovKernel likelihood] (bestAction : Env -> Action) (_hbestAction : Measurable bestAction) : ProbabilityTheory.Kernel History Action

Source line 23 Chapter context: Thompson sampling

def BanditRLProof.Thompson.canonicalActionKernelOnPair Compiled

Lift the history-indexed action kernel to environment/history pairs.

Used in these reading views: Bandit Book

6. Thompson sampling and Bayesian regret

Canonical node identity

declaration:BanditRLProof.Thompson.canonicalActionKernelOnPair

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

noncomputable def canonicalActionKernelOnPair {History : Type u} {Env : Type v} {Action : Type w} [MeasurableSpace History] [MeasurableSpace Env] [StandardBorelSpace Env] [Nonempty Env] [MeasurableSpace Action] (prior : Measure Env) [IsProbabilityMeasure prior] (likelihood : ProbabilityTheory.Kernel Env History) [ProbabilityTheory.IsMarkovKernel likelihood] (bestAction : Env -> Action) (hbestAction : Measurable bestAction) : ProbabilityTheory.Kernel (Env × History) Action

Source line 50 Chapter context: Thompson sampling

def BanditRLProof.Thompson.canonicalSamplerMeasure Compiled

The canonical one-step Thompson law on `(Env × History) × Action`. The first component is sampled from `prior ⊗ₘ likelihood`; the action is then sampled from the canonical posterior mapped by `bestAction` at that history.

Used in these reading views: Bandit Book

6. Thompson sampling and Bayesian regret

Canonical node identity

declaration:BanditRLProof.Thompson.canonicalSamplerMeasure

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

noncomputable def canonicalSamplerMeasure {History : Type u} {Env : Type v} {Action : Type w} [MeasurableSpace History] [MeasurableSpace Env] [StandardBorelSpace Env] [Nonempty Env] [MeasurableSpace Action] (prior : Measure Env) [IsProbabilityMeasure prior] (likelihood : ProbabilityTheory.Kernel Env History) [ProbabilityTheory.IsMarkovKernel likelihood] (bestAction : Env -> Action) (hbestAction : Measurable bestAction) : Measure ((Env × History) × Action)

Source line 83 Chapter context: Thompson sampling

def BanditRLProof.Thompson.canonicalSamplerEnv Compiled

Environment coordinate of the canonical sampler source.

Used in these reading views: Bandit Book

6. Thompson sampling and Bayesian regret

Canonical node identity

declaration:BanditRLProof.Thompson.canonicalSamplerEnv

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

def canonicalSamplerEnv {Env History Action : Type*} : (Env × History) × Action -> Env

Source line 111 Chapter context: Thompson sampling

def BanditRLProof.Thompson.canonicalSamplerHistory Compiled

History coordinate of the canonical sampler source.

Used in these reading views: Bandit Book

6. Thompson sampling and Bayesian regret

Canonical node identity

declaration:BanditRLProof.Thompson.canonicalSamplerHistory

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

def canonicalSamplerHistory {Env History Action : Type*} : (Env × History) × Action -> History

Source line 116 Chapter context: Thompson sampling

def BanditRLProof.Thompson.canonicalSamplerAction Compiled

Action coordinate of the canonical sampler source.

Used in these reading views: Bandit Book

6. Thompson sampling and Bayesian regret

Canonical node identity

declaration:BanditRLProof.Thompson.canonicalSamplerAction

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

def canonicalSamplerAction {Env History Action : Type*} : (Env × History) × Action -> Action

Source line 121 Chapter context: Thompson sampling

theorem BanditRLProof.Thompson.canonicalSamplerEnv_measurable Compiled

No declaration docstring is present; use the chapter context and exact statement below.

Used in these reading views: Bandit Book

6. Thompson sampling and Bayesian regret

Canonical node identity

declaration:BanditRLProof.Thompson.canonicalSamplerEnv_measurable

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

theorem canonicalSamplerEnv_measurable {Env History Action : Type*} [MeasurableSpace Env] [MeasurableSpace History] [MeasurableSpace Action] : Measurable (@canonicalSamplerEnv Env History Action)

Source line 125 Chapter context: Thompson sampling

theorem BanditRLProof.Thompson.canonicalSamplerHistory_measurable Compiled

No declaration docstring is present; use the chapter context and exact statement below.

Used in these reading views: Bandit Book

6. Thompson sampling and Bayesian regret

Canonical node identity

declaration:BanditRLProof.Thompson.canonicalSamplerHistory_measurable

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

theorem canonicalSamplerHistory_measurable {Env History Action : Type*} [MeasurableSpace Env] [MeasurableSpace History] [MeasurableSpace Action] : Measurable (@canonicalSamplerHistory Env History Action)

Source line 131 Chapter context: Thompson sampling

theorem BanditRLProof.Thompson.canonicalSamplerAction_measurable Compiled

No declaration docstring is present; use the chapter context and exact statement below.

Used in these reading views: Bandit Book

6. Thompson sampling and Bayesian regret

Canonical node identity

declaration:BanditRLProof.Thompson.canonicalSamplerAction_measurable

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

theorem canonicalSamplerAction_measurable {Env History Action : Type*} [MeasurableSpace Env] [MeasurableSpace History] [MeasurableSpace Action] : Measurable (@canonicalSamplerAction Env History Action)

Source line 137 Chapter context: Thompson sampling

theorem BanditRLProof.Thompson.map_compProd_comap_snd Compiled

Projecting a composition product whose kernel depends only on the second base coordinate gives the second-coordinate marginal composed with that kernel.

Used in these reading views: Bandit Book

6. Thompson sampling and Bayesian regret

Canonical node identity

declaration:BanditRLProof.Thompson.map_compProd_comap_snd

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

theorem map_compProd_comap_snd {Env History Action : Type*} [MeasurableSpace Env] [MeasurableSpace History] [MeasurableSpace Action] (mu : Measure (Env × History)) [IsFiniteMeasure mu] (actionKernel : ProbabilityTheory.Kernel History Action) [ProbabilityTheory.IsMarkovKernel actionKernel] : (mu ⊗ₘ actionKernel.comap Prod.snd measurable_snd).map (fun sample => (sample.1.2, sample.2)) = mu.map Prod.snd ⊗ₘ actionKernel

Source line 147 Chapter context: Thompson sampling

theorem BanditRLProof.Thompson.canonicalSampler_env_history_map_eq Compiled

The canonical sampler preserves the prescribed environment/history law.

Used in these reading views: Bandit Book

6. Thompson sampling and Bayesian regret

Canonical node identity

declaration:BanditRLProof.Thompson.canonicalSampler_env_history_map_eq

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

theorem canonicalSampler_env_history_map_eq {History : Type u} {Env : Type v} {Action : Type w} [MeasurableSpace History] [MeasurableSpace Env] [StandardBorelSpace Env] [Nonempty Env] [MeasurableSpace Action] (prior : Measure Env) [IsProbabilityMeasure prior] (likelihood : ProbabilityTheory.Kernel Env History) [ProbabilityTheory.IsMarkovKernel likelihood] (bestAction : Env -> Action) (hbestAction : Measurable bestAction) : (canonicalSamplerMeasure prior likelihood bestAction hbestAction).map (fun sample => (canonicalSamplerEnv sample, canonicalSamplerHistory sample)) = PosteriorKernel.canonicalJointMeasure prior likelihood

Source line 181 Chapter context: Thompson sampling

theorem BanditRLProof.Thompson.canonicalSampler_history_action_map_eq Compiled

The history/action marginal is generated by the canonical action kernel.

Used in these reading views: Bandit Book

6. Thompson sampling and Bayesian regret

Canonical node identity

declaration:BanditRLProof.Thompson.canonicalSampler_history_action_map_eq

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

theorem canonicalSampler_history_action_map_eq {History : Type u} {Env : Type v} {Action : Type w} [MeasurableSpace History] [MeasurableSpace Env] [StandardBorelSpace Env] [Nonempty Env] [MeasurableSpace Action] (prior : Measure Env) [IsProbabilityMeasure prior] (likelihood : ProbabilityTheory.Kernel Env History) [ProbabilityTheory.IsMarkovKernel likelihood] (bestAction : Env -> Action) (hbestAction : Measurable bestAction) : (canonicalSamplerMeasure prior likelihood bestAction hbestAction).map (fun sample => (canonicalSamplerHistory sample, canonicalSamplerAction sample)) = (canonicalSamplerMeasure prior likelihood bestAction hbestAction).map canonicalSamplerHistory ⊗ₘ canonicalActionKernel prior likelihood bestAction hbestAction

Source line 200 Chapter context: Thompson sampling

theorem BanditRLProof.Thompson.canonicalSampler_condDistrib_action_ae_eq_actionKernel Compiled

The constructed sampler has the intended next-action conditional law.

Used in these reading views: Bandit Book

6. Thompson sampling and Bayesian regret

Canonical node identity

declaration:BanditRLProof.Thompson.canonicalSampler_condDistrib_action_ae_eq_actionKernel

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

theorem canonicalSampler_condDistrib_action_ae_eq_actionKernel {History : Type u} {Env : Type v} {Action : Type w} [MeasurableSpace History] [MeasurableSpace Env] [StandardBorelSpace Env] [Nonempty Env] [MeasurableSpace Action] [StandardBorelSpace Action] [Nonempty Action] (prior : Measure Env) [IsProbabilityMeasure prior] (likelihood : ProbabilityTheory.Kernel Env History) [ProbabilityTheory.IsMarkovKernel likelihood] (bestAction : Env -> Action) (hbestAction : Measurable bestAction) : ProbabilityTheory.condDistrib canonicalSamplerAction canonicalSamplerHistory (canonicalSamplerMeasure prior likelihood bestAction hbestAction) =ᵐ[ (canonicalSamplerMeasure prior likelihood bestAction hbestAction).map canonicalSamplerHistory] canonicalActionKernel prior likelihood bestAction hbestAction

Source line 242 Chapter context: Thompson sampling

theorem BanditRLProof.Thompson.canonicalSampler_condDistrib_action_ae_eq_bestAction Compiled

Premise-free one-step Thompson probability matching for the canonical sampler. Both law premises of the generic theorem are discharged by the constructed composition-product measure: its environment/history marginal is the canonical Bayesian joint law, and its history/action marginal is generated by the mapped canonical posterior.

Used in these reading views: Bandit Book

6. Thompson sampling and Bayesian regret

Canonical node identity

declaration:BanditRLProof.Thompson.canonicalSampler_condDistrib_action_ae_eq_bestAction

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

theorem canonicalSampler_condDistrib_action_ae_eq_bestAction {History : Type u} {Env : Type v} {Action : Type w} [MeasurableSpace History] [MeasurableSpace Env] [StandardBorelSpace Env] [Nonempty Env] [MeasurableSpace Action] [StandardBorelSpace Action] [Nonempty Action] (prior : Measure Env) [IsProbabilityMeasure prior] (likelihood : ProbabilityTheory.Kernel Env History) [ProbabilityTheory.IsMarkovKernel likelihood] (bestAction : Env -> Action) (hbestAction : Measurable bestAction) : ProbabilityTheory.condDistrib canonicalSamplerAction canonicalSamplerHistory (canonicalSamplerMeasure prior likelihood bestAction hbestAction) =ᵐ[ (canonicalSamplerMeasure prior likelihood bestAction hbestAction).map canonicalSamplerHistory] ProbabilityTheory.condDistrib (bestAction ∘ canonicalSamplerEnv) canonicalSamplerHistory (canonicalSamplerMeasure prior likelihood bestAction hbestAction)

Source line 271 Open teaching explanation Chapter context: Thompson sampling