BanditRLProof.Algorithms.Thompson

A lightweight descriptor for a Bayesian bandit parameter space.

structure PriorSketch where

The proof-DAG leaves usually needed for Thompson sampling regret.

def obligationNames : List String

Source contract for the Thompson probability-matching identity. The ledger records the exact law expected from a Thompson action sampler: its action kernel at a history agrees on every measurable action event with the posterior distribution pushed forward by the environment-to-best-action map. It is a contract surface, not a Bayes-rule proof or posterior-sampler construction.

structure PosteriorActionIdentityLedger (History : Type u) (Env : Type v) (Action : Type w) [MeasurableSpace History] [MeasurableSpace Env] [MeasurableSpace Action] where

Any best-action selector out of a countable singleton-measurable environment space is measurable. This is the regularity wrapper needed by finite or countable posterior model spaces before constructing a Thompson posterior-action identity ledger.

theorem bestAction_measurable_of_countable_env {Env : Type v} {Action : Type w} [MeasurableSpace Env] [MeasurableSingletonClass Env] [Countable Env] [MeasurableSpace Action] (bestAction : Env -> Action) : Measurable bestAction

Build a posterior-action identity ledger over a countable environment space without separately supplying best-action measurability.

def ofCountableEnv [MeasurableSingletonClass Env] [Countable Env] (posterior : PosteriorKernel.MarkovPosteriorKernel History Env) (actionKernel : ProbabilityTheory.Kernel History Action) (hactionKernel : ProbabilityTheory.IsMarkovKernel actionKernel) (bestAction : Env -> Action) (hmatch : forall (history : History) {event : Set Action}, MeasurableSet event -> actionKernel history event = Measure.map bestAction (posterior.kernel history) event) : PosteriorActionIdentityLedger History Env Action where

Build the Thompson action ledger directly by mapping a posterior kernel through a measurable best-action selector.

noncomputable def ofPosteriorMap (posterior : PosteriorKernel.MarkovPosteriorKernel History Env) (bestAction : Env -> Action) (hbestAction : Measurable bestAction) : PosteriorActionIdentityLedger History Env Action where

The event-level ledger identity is equality of the two Markov kernels.

theorem actionKernel_eq_posterior_map (ledger : PosteriorActionIdentityLedger History Env Action) : ledger.actionKernel = ledger.posterior.kernel.map ledger.bestAction

Event-level Thompson probability matching from the packaged ledger.

theorem actionKernel_apply_eq_posteriorBest_map (ledger : PosteriorActionIdentityLedger History Env Action) (history : History) {event : Set Action} (hevent : MeasurableSet event) : ledger.actionKernel history event = Measure.map ledger.bestAction (ledger.posterior.kernel history) event

Singleton form of the posterior action identity. For discrete or singleton-measurable action spaces, the Thompson probability of choosing `action` is the posterior probability that `action` is the best action.

theorem actionKernel_apply_singleton_eq_posteriorBest_preimage [MeasurableSingletonClass Action] (ledger : PosteriorActionIdentityLedger History Env Action) (history : History) (action : Action) : ledger.actionKernel history ({action} : Set Action) = ledger.posterior.kernel history {env : Env | ledger.bestAction env = action}

Source fields needed for the Thompson posterior-action conditional-law theorem. The first law says the process samples its next action from the ledger action kernel. The second identifies the ledger posterior with the conditional law of the latent environment given the observed history. These are the two law surfaces used by the pinned LML proof.

structure BayesianPosteriorActionSource {Omega : Type u} (History : Type v) (Env : Type w) (Action : Type*) [MeasurableSpace Omega] [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) (nextAction : Omega -> Action) (ledger : PosteriorActionIdentityLedger History Env Action) : Prop where

Thompson probability matching in Mathlib `condDistrib` form. Mapping the posterior-kernel equality through `bestAction` identifies the ledger action kernel with the mapped environment conditional law. Mathlib's `condDistrib_comp` then identifies that map with the conditional law of the random best action itself.

theorem condDistrib_action_ae_eq_bestAction_of_bayesianPosteriorActionSource {Omega : Type u} {History : Type v} {Env : Type w} {Action : Type*} [MeasurableSpace Omega] [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) (nextAction : Omega -> Action) (ledger : PosteriorActionIdentityLedger History Env Action) (source : BayesianPosteriorActionSource History Env Action mu env history nextAction ledger) : ProbabilityTheory.condDistrib nextAction history mu =ᵐ[mu.map history] ProbabilityTheory.condDistrib (ledger.bestAction ∘ env) history mu

Direct posterior-map form of Thompson probability matching. This is the local Mathlib-facing counterpart of pinned LML `Bandits.TS.hasCondDistrib_action`: it avoids a local `HasCondDistrib` wrapper and states the resulting regular conditional-kernel equality directly.

theorem condDistrib_action_ae_eq_bestAction_of_posteriorMap {Omega : Type u} {History : Type v} {Env : Type w} {Action : Type*} [MeasurableSpace Omega] [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) (nextAction : Omega -> Action) (posterior : PosteriorKernel.MarkovPosteriorKernel History Env) (bestAction : Env -> Action) (hbestAction : Measurable bestAction) (henv : Measurable env) (hhistory : Measurable history) (hnextAction : Measurable nextAction) (haction : ProbabilityTheory.condDistrib nextAction history mu =ᵐ[mu.map history] posterior.kernel.map bestAction) (hposterior : posterior.kernel =ᵐ[mu.map history] ProbabilityTheory.condDistrib env history mu) : ProbabilityTheory.condDistrib nextAction history mu =ᵐ[mu.map history] ProbabilityTheory.condDistrib (bestAction ∘ env) history mu

Thompson probability matching from a Bayesian environment/history pair law. Unlike `condDistrib_action_ae_eq_bestAction_of_posteriorMap`, this theorem does not assume the posterior/environment conditional-law equality. It constructs that equality from the source pair law using Mathlib's canonical posterior.

theorem condDistrib_action_ae_eq_bestAction_of_bayesianPairMap {Omega : Type u} {History : Type v} {Env : Type w} {Action : Type*} [MeasurableSpace Omega] [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) (nextAction : Omega -> Action) (prior : Measure Env) [IsProbabilityMeasure prior] (likelihood : ProbabilityTheory.Kernel Env History) [ProbabilityTheory.IsMarkovKernel likelihood] (bestAction : Env -> Action) (hbestAction : Measurable bestAction) (henv : Measurable env) (hhistory : Measurable history) (hnextAction : Measurable nextAction) (hpair : mu.map (fun omega => (env omega, history omega)) = PosteriorKernel.canonicalJointMeasure prior likelihood) (haction : ProbabilityTheory.condDistrib nextAction history mu =ᵐ[mu.map history] (PosteriorKernel.canonicalPosterior prior likelihood).kernel.map bestAction) : ProbabilityTheory.condDistrib nextAction history mu =ᵐ[mu.map history] ProbabilityTheory.condDistrib (bestAction ∘ env) history mu

Canonical-product specialization of the Thompson posterior-action law. The source space is `Env × History` with law `prior ⊗ₘ likelihood`, so the posterior conditional-law premise is discharged entirely by the canonical Bayesian construction. The remaining law premise is exactly the Thompson action sampler's conditional law.

theorem condDistrib_action_ae_eq_bestAction_of_canonicalPriorLikelihood {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] (nextAction : Env × History -> Action) (bestAction : Env -> Action) (hbestAction : Measurable bestAction) (hnextAction : Measurable nextAction) (haction : ProbabilityTheory.condDistrib nextAction Prod.snd (PosteriorKernel.canonicalJointMeasure prior likelihood) =ᵐ[ (PosteriorKernel.canonicalJointMeasure prior likelihood).map Prod.snd] (PosteriorKernel.canonicalPosterior prior likelihood).kernel.map bestAction) : ProbabilityTheory.condDistrib nextAction Prod.snd (PosteriorKernel.canonicalJointMeasure prior likelihood) =ᵐ[ (PosteriorKernel.canonicalJointMeasure prior likelihood).map Prod.snd] ProbabilityTheory.condDistrib (bestAction ∘ Prod.fst) Prod.snd (PosteriorKernel.canonicalJointMeasure prior likelihood)