Lean module · Thompson sampling

BanditRLProof.Algorithms.ThompsonCanonicalSampler

# Canonical one-step Thompson sampler 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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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