Lean module · Thompson sampling

BanditRLProof.Algorithms.ThompsonReferencePolicy

# Thompson sampling from a reference posterior policy LML defines Thompson sampling from the posterior under a fixed reference algorithm and then transports that posterior to the actual process by an algorithm-density theorem. This module isolates the corresponding local Mathlib boundary. The next action is genuinely sampled by a composition-product measure, so no action conditional-law premise remains. The only process-level premise in the final theorem is posterior invariance between the reference and actual history laws.

Module map

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

Imports

BanditRLProof.Algorithms.ThompsonCanonicalSampler, BanditRLProof.HistoryFiltration

Imported by

BanditRLProof, BanditRLProof.Algorithms.ThompsonAlgorithmDensity

Declarations

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

def BanditRLProof.Thompson.referencePosterior Compiled

A reference source's environment posterior given its history.

noncomputable def referencePosterior {OmegaRef : Type u} {History : Type v} {Env : Type w} [MeasurableSpace OmegaRef] [MeasurableSpace History] [MeasurableSpace Env] [StandardBorelSpace Env] [Nonempty Env] (referenceMu : Measure OmegaRef) [IsFiniteMeasure referenceMu] (referenceEnv : OmegaRef -> Env) (referenceHistory : OmegaRef -> History) (_hreferenceEnv : Measurable referenceEnv) (_hreferenceHistory : Measurable referenceHistory) : PosteriorKernel.MarkovPosteriorKernel History Env

Source line 27 Chapter context: Thompson sampling

theorem BanditRLProof.Thompson.referencePosterior_kernel Compiled

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

theorem referencePosterior_kernel {OmegaRef : Type u} {History : Type v} {Env : Type w} [MeasurableSpace OmegaRef] [MeasurableSpace History] [MeasurableSpace Env] [StandardBorelSpace Env] [Nonempty Env] (referenceMu : Measure OmegaRef) [IsFiniteMeasure referenceMu] (referenceEnv : OmegaRef -> Env) (referenceHistory : OmegaRef -> History) (hreferenceEnv : Measurable referenceEnv) (hreferenceHistory : Measurable referenceHistory) : (referencePosterior referenceMu referenceEnv referenceHistory hreferenceEnv hreferenceHistory).kernel = ProbabilityTheory.condDistrib referenceEnv referenceHistory referenceMu

Source line 42 Chapter context: Thompson sampling

def BanditRLProof.Thompson.referenceActionKernel Compiled

The Thompson action policy obtained by mapping a reference posterior.

noncomputable def referenceActionKernel {OmegaRef : Type u} {History : Type v} {Env : Type w} {Action : Type x} [MeasurableSpace OmegaRef] [MeasurableSpace History] [MeasurableSpace Env] [StandardBorelSpace Env] [Nonempty Env] [MeasurableSpace Action] (referenceMu : Measure OmegaRef) [IsFiniteMeasure referenceMu] (referenceEnv : OmegaRef -> Env) (referenceHistory : OmegaRef -> History) (hreferenceEnv : Measurable referenceEnv) (hreferenceHistory : Measurable referenceHistory) (bestAction : Env -> Action) (_hbestAction : Measurable bestAction) : ProbabilityTheory.Kernel History Action

Source line 57 Chapter context: Thompson sampling

def BanditRLProof.Thompson.policySamplerMeasure Compiled

Extend a base process by sampling an action from a history-indexed policy.

noncomputable def policySamplerMeasure {Omega : Type u} {History : Type v} {Action : Type w} [MeasurableSpace Omega] [MeasurableSpace History] [MeasurableSpace Action] (mu : Measure Omega) [IsFiniteMeasure mu] (history : Omega -> History) (hhistory : Measurable history) (policy : ProbabilityTheory.Kernel History Action) [ProbabilityTheory.IsMarkovKernel policy] : Measure (Omega × Action)

Source line 90 Chapter context: Thompson sampling

def BanditRLProof.Thompson.policySamplerEnv Compiled

Base environment coordinate after adjoining a sampled action.

def policySamplerEnv {Omega Env Action : Type*} (env : Omega -> Env) : Omega × Action -> Env

Source line 112 Chapter context: Thompson sampling

def BanditRLProof.Thompson.policySamplerHistory Compiled

Base history coordinate after adjoining a sampled action.

def policySamplerHistory {Omega History Action : Type*} (history : Omega -> History) : Omega × Action -> History

Source line 118 Chapter context: Thompson sampling

def BanditRLProof.Thompson.policySamplerAction Compiled

Newly sampled action coordinate.

def policySamplerAction {Omega Action : Type*} : Omega × Action -> Action

Source line 124 Chapter context: Thompson sampling

theorem BanditRLProof.Thompson.policySamplerEnv_measurable Compiled

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

theorem policySamplerEnv_measurable {Omega Env Action : Type*} [MeasurableSpace Omega] [MeasurableSpace Env] [MeasurableSpace Action] (env : Omega -> Env) (henv : Measurable env) : Measurable (@policySamplerEnv Omega Env Action env)

Source line 127 Chapter context: Thompson sampling

theorem BanditRLProof.Thompson.policySamplerHistory_measurable Compiled

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

theorem policySamplerHistory_measurable {Omega History Action : Type*} [MeasurableSpace Omega] [MeasurableSpace History] [MeasurableSpace Action] (history : Omega -> History) (hhistory : Measurable history) : Measurable (@policySamplerHistory Omega History Action history)

Source line 134 Chapter context: Thompson sampling

theorem BanditRLProof.Thompson.policySamplerAction_measurable Compiled

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

theorem policySamplerAction_measurable {Omega Action : Type*} [MeasurableSpace Omega] [MeasurableSpace Action] : Measurable (@policySamplerAction Omega Action)

Source line 141 Chapter context: Thompson sampling

theorem BanditRLProof.Thompson.map_compProd_comap_history Compiled

History/action projection of a policy sampler. This is the arbitrary-history-map version of `map_compProd_comap_snd` and is a generic Mathlib candidate.

theorem map_compProd_comap_history {Omega History Action : Type*} [MeasurableSpace Omega] [MeasurableSpace History] [MeasurableSpace Action] (mu : Measure Omega) [IsFiniteMeasure mu] (history : Omega -> History) (hhistory : Measurable history) (policy : ProbabilityTheory.Kernel History Action) [ProbabilityTheory.IsMarkovKernel policy] : (mu ⊗ₘ policy.comap history hhistory).map (fun sample => (history sample.1, sample.2)) = mu.map history ⊗ₘ policy

Source line 153 Chapter context: Thompson sampling

theorem BanditRLProof.Thompson.policySampler_base_map_eq Compiled

Adjoining a Markov-policy sample preserves every measurable base map.

theorem policySampler_base_map_eq {Omega History Action Target : Type*} [MeasurableSpace Omega] [MeasurableSpace History] [MeasurableSpace Action] [MeasurableSpace Target] (mu : Measure Omega) [IsFiniteMeasure mu] (history : Omega -> History) (hhistory : Measurable history) (policy : ProbabilityTheory.Kernel History Action) [ProbabilityTheory.IsMarkovKernel policy] (f : Omega -> Target) (hf : Measurable f) : (policySamplerMeasure mu history hhistory policy).map (fun sample => f sample.1) = mu.map f

Source line 183 Chapter context: Thompson sampling

theorem BanditRLProof.Thompson.policySampler_history_action_map_eq Compiled

The constructed sampler's history/action joint law is `historyLaw ⊗ policy`.

theorem policySampler_history_action_map_eq {Omega History Action : Type*} [MeasurableSpace Omega] [MeasurableSpace History] [MeasurableSpace Action] (mu : Measure Omega) [IsFiniteMeasure mu] (history : Omega -> History) (hhistory : Measurable history) (policy : ProbabilityTheory.Kernel History Action) [ProbabilityTheory.IsMarkovKernel policy] : (policySamplerMeasure mu history hhistory policy).map (fun sample => (policySamplerHistory history sample, policySamplerAction sample)) = (policySamplerMeasure mu history hhistory policy).map (policySamplerHistory history) ⊗ₘ policy

Source line 207 Chapter context: Thompson sampling

theorem BanditRLProof.Thompson.policySampler_condDistrib_action_ae_eq_policy Compiled

The sampled action has the policy as its conditional law given history.

theorem policySampler_condDistrib_action_ae_eq_policy {Omega History Action : Type*} [MeasurableSpace Omega] [MeasurableSpace History] [MeasurableSpace Action] [StandardBorelSpace Action] [Nonempty Action] (mu : Measure Omega) [IsFiniteMeasure mu] (history : Omega -> History) (hhistory : Measurable history) (policy : ProbabilityTheory.Kernel History Action) [ProbabilityTheory.IsMarkovKernel policy] : ProbabilityTheory.condDistrib policySamplerAction (policySamplerHistory history) (policySamplerMeasure mu history hhistory policy) =ᵐ[ (policySamplerMeasure mu history hhistory policy).map (policySamplerHistory history)] policy

Source line 229 Chapter context: Thompson sampling

theorem BanditRLProof.Thompson.policySampler_condDistrib_env_ae_eq_of_base Compiled

Adjoining a history-dependent action sample preserves an environment posterior.

theorem policySampler_condDistrib_env_ae_eq_of_base {Omega History Env Action : Type*} [MeasurableSpace Omega] [MeasurableSpace History] [MeasurableSpace Env] [StandardBorelSpace Env] [Nonempty Env] [MeasurableSpace Action] (mu : Measure Omega) [IsFiniteMeasure mu] (env : Omega -> Env) (history : Omega -> History) (henv : Measurable env) (hhistory : Measurable history) (policy : ProbabilityTheory.Kernel History Action) [ProbabilityTheory.IsMarkovKernel policy] (posterior : ProbabilityTheory.Kernel History Env) [ProbabilityTheory.IsMarkovKernel posterior] (hbase : ProbabilityTheory.condDistrib env history mu =ᵐ[mu.map history] posterior) : ProbabilityTheory.condDistrib (policySamplerEnv env) (policySamplerHistory history) (policySamplerMeasure mu history hhistory policy) =ᵐ[ (policySamplerMeasure mu history hhistory policy).map (policySamplerHistory history)] posterior

Source line 251 Chapter context: Thompson sampling

theorem BanditRLProof.Thompson.referencePolicySampler_condDistrib_action_ae_eq_bestAction_of_posterior_invariance Compiled

Reference-posterior Thompson probability matching with a constructed sampler. The action law is generated by `policySamplerMeasure`. The sole law transport premise is that the reference posterior agrees with the actual environment posterior at the actual history law; this is the conclusion supplied by LML's algorithm-density route.

theorem referencePolicySampler_condDistrib_action_ae_eq_bestAction_of_posterior_invariance {Omega : Type u} {OmegaRef : Type v} {History : Type w} {Env : Type x} {Action : Type y} [MeasurableSpace Omega] [MeasurableSpace OmegaRef] [MeasurableSpace History] [MeasurableSpace Env] [StandardBorelSpace Env] [Nonempty Env] [MeasurableSpace Action] [StandardBorelSpace Action] [Nonempty Action] (mu : Measure Omega) [IsFiniteMeasure mu] (env : Omega -> Env) (history : Omega -> History) (henv : Measurable env) (hhistory : Measurable history) (referenceMu : Measure OmegaRef) [IsFiniteMeasure referenceMu] (referenceEnv : OmegaRef -> Env) (referenceHistory : OmegaRef -> History) (hreferenceEnv : Measurable referenceEnv) (hreferenceHistory : Measurable referenceHistory) (bestAction : Env -> Action) (hbestAction : Measurable bestAction) (hposteriorInvariance : (referencePosterior referenceMu referenceEnv referenceHistory hreferenceEnv hreferenceHistory).kernel =ᵐ[mu.map history] ProbabilityTheory.condDistrib env history mu) : let policy := referenceActionKernel referenceMu referenceEnv referenceHistory hreferenceEnv hreferenceHistory bestAction hbestAction let sampler := policySamplerMeasure mu history hhistory policy ProbabilityTheory.condDistrib policySamplerAction (policySamplerHistory history) sampler =ᵐ[ sampler.map (policySamplerHistory history)] ProbabilityTheory.condDistrib (bestAction ∘ policySamplerEnv env) (policySamplerHistory history) sampler

Source line 307 Chapter context: Thompson sampling

theorem BanditRLProof.Thompson.finitePairReferencePolicySampler_condDistrib_action_ae_eq_bestAction_of_posterior_invariance Compiled

Finite action/reward-prefix specialization of the reference-policy theorem. This is the per-time interface used by the recursive bandit route. The remaining premise is exactly posterior invariance between the reference and actual finite-pair history laws.

theorem finitePairReferencePolicySampler_condDistrib_action_ae_eq_bestAction_of_posterior_invariance {Omega : Type u} {OmegaRef : Type v} {Env : Type w} {Action : Type x} {Reward : Type y} [MeasurableSpace Omega] [MeasurableSpace OmegaRef] [MeasurableSpace Env] [StandardBorelSpace Env] [Nonempty Env] [MeasurableSpace Action] [StandardBorelSpace Action] [Nonempty Action] [MeasurableSpace Reward] (mu : Measure Omega) [IsFiniteMeasure mu] (env : Omega -> Env) (action : Omega -> ActionTrace Action) (reward : Omega -> RewardTrace Reward) (henv : Measurable env) (haction : forall t : Nat, Measurable (fun omega => action omega t)) (hreward : forall t : Nat, Measurable (fun omega => reward omega t)) (referenceMu : Measure OmegaRef) [IsFiniteMeasure referenceMu] (referenceEnv : OmegaRef -> Env) (referenceAction : OmegaRef -> ActionTrace Action) (referenceReward : OmegaRef -> RewardTrace Reward) (hreferenceEnv : Measurable referenceEnv) (hreferenceAction : forall t : Nat, Measurable (fun omega => referenceAction omega t)) (hreferenceReward : forall t : Nat, Measurable (fun omega => referenceReward omega t)) (n : Nat) (bestAction : Env -> Action) (hbestAction : Measurable bestAction) (hposteriorInvariance : ProbabilityTheory.condDistrib referenceEnv (fun omega => History.finitePairHistoryOfTrace (referenceAction omega) (referenceReward omega) n) referenceMu =ᵐ[ mu.map (fun omega => History.finitePairHistoryOfTrace (action omega) (reward omega) n)] ProbabilityTheory.condDistrib env (fun omega => History.finitePairHistoryOfTrace (action omega) (reward omega) n) mu) : let actualHistory := fun omega => History.finitePairHistoryOfTrace (action omega) (reward omega) n let referenceHistory := fun omega => History.finitePairHistoryOfTrace (referenceAction omega) (referenceReward omega) n let policy := referenceActionKernel referenceMu referenceEnv referenceHistory hreferenceEnv (History.measurable_finitePairHistoryOfTrace referenceAction referenceReward hreferenceAction hreferenceReward n) bestAction hbestAction let sampler := policySamplerMeasure mu actualHistory (History.measurable_finitePairHistoryOfTrace action reward haction hreward n) policy ProbabilityTheory.condDistrib policySamplerAction (policySamplerHistory actualHistory) sampler =ᵐ[ sampler.map (policySamplerHistory actualHistory)] ProbabilityTheory.condDistrib (bestAction ∘ policySamplerEnv env) (policySamplerHistory actualHistory) sampler

Source line 373 Chapter context: Thompson sampling