BanditRLProof.Algorithms.ThompsonRecursiveSampler

Uniform probability measure on a nonempty finite action space.

noncomputable def uniformActionMeasure (Action : Type u) [Fintype Action] [Nonempty Action] [MeasurableSpace Action] : Measure Action

Every measure on a finite space is dominated by its uniform measure.

theorem absolutelyContinuous_uniformActionMeasure {Action : Type u} [Fintype Action] [Nonempty Action] [MeasurableSpace Action] (mu : Measure Action) : mu ≪ uniformActionMeasure Action

History-independent uniform reference algorithm.

noncomputable def uniformHistoryAlgorithm (Action : Type u) (Reward : Type v) [Fintype Action] [Nonempty Action] [MeasurableSpace Action] [MeasurableSpace Reward] : HistoryAlgorithm Action Reward where

Any history algorithm is absolutely continuous with respect to uniform.

theorem historyAlgorithmAbsolutelyContinuous_uniform {Action : Type u} {Reward : Type v} [Fintype Action] [Nonempty Action] [MeasurableSpace Action] [MeasurableSpace Reward] (algorithm : HistoryAlgorithm Action Reward) : HistoryAlgorithmAbsolutelyContinuous algorithm (uniformHistoryAlgorithm Action Reward) where

Mixing environment-indexed trajectory laws preserves a common conditional action kernel. This is the generic measure transport needed to turn pointwise trajectory laws into one global recursive process law.

theorem trajectoryMixture_map_history_action_eq_compProd {Env : Type u} {Omega : Type v} {History : Type w} {Action : Type x} [MeasurableSpace Env] [MeasurableSpace Omega] [MeasurableSpace History] [MeasurableSpace Action] (prior : Measure Env) [IsFiniteMeasure prior] (trajectory : ProbabilityTheory.Kernel Env Omega) [ProbabilityTheory.IsMarkovKernel trajectory] (history : Omega -> History) (hhistory : Measurable history) (action : Omega -> Action) (haction : Measurable action) (policy : ProbabilityTheory.Kernel History Action) [ProbabilityTheory.IsMarkovKernel policy] (hlaw : forall env, (trajectory env).map (fun omega => (history omega, action omega)) = (trajectory env).map history ⊗ₘ policy) : (prior ⊗ₘ trajectory).map (fun sample => (history sample.2, action sample.2)) = (prior ⊗ₘ trajectory).map (history ∘ Prod.snd) ⊗ₘ policy

Conditional-law form of `trajectoryMixture_map_history_action_eq_compProd`.

theorem trajectoryMixture_condDistrib_action {Env : Type u} {Omega : Type v} {History : Type w} {Action : Type x} [MeasurableSpace Env] [MeasurableSpace Omega] [MeasurableSpace History] [MeasurableSpace Action] [StandardBorelSpace Action] [Nonempty Action] (prior : Measure Env) [IsFiniteMeasure prior] (trajectory : ProbabilityTheory.Kernel Env Omega) [ProbabilityTheory.IsMarkovKernel trajectory] (history : Omega -> History) (hhistory : Measurable history) (action : Omega -> Action) (haction : Measurable action) (policy : ProbabilityTheory.Kernel History Action) [ProbabilityTheory.IsMarkovKernel policy] (hlaw : forall env, (trajectory env).map (fun omega => (history omega, action omega)) = (trajectory env).map history ⊗ₘ policy) : ProbabilityTheory.condDistrib (action ∘ Prod.snd) (history ∘ Prod.snd) (prior ⊗ₘ trajectory) =ᵐ[(prior ⊗ₘ trajectory).map (history ∘ Prod.snd)] policy

The visible action marginal of each fixed-environment successor law.

theorem canonicalMeasurableEnvironmentTrajectoryKernel_map_history_action_eq_compProd {Env : Type u} {Action : Type v} {Reward : Type w} [MeasurableSpace Env] [StandardBorelSpace Env] [MeasurableSpace Action] [StandardBorelSpace Action] [Nonempty Action] [MeasurableSpace Reward] [StandardBorelSpace Reward] [Nonempty Reward] (algorithm : HistoryAlgorithm Action Reward) (environment : MeasurableHistoryEnvironment Env Action Reward) (env : Env) (n : Nat) : (canonicalMeasurableEnvironmentTrajectoryKernel algorithm environment env).map (fun trajectory => (Preorder.frestrictLe n trajectory, (trajectory (n + 1)).1)) = (canonicalMeasurableEnvironmentTrajectoryKernel algorithm environment env).map (Preorder.frestrictLe n) ⊗ₘ algorithm.policy n

The next action coordinate of the global prior/trajectory measure has the algorithm policy as its conditional law given the visible finite history.

theorem canonicalMeasurableEnvironmentTrajectoryMeasure_condDistrib_action {Env : Type u} {Action : Type v} {Reward : Type w} [MeasurableSpace Env] [StandardBorelSpace Env] [MeasurableSpace Action] [StandardBorelSpace Action] [Nonempty Action] [MeasurableSpace Reward] [StandardBorelSpace Reward] [Nonempty Reward] (prior : Measure Env) [IsFiniteMeasure prior] (algorithm : HistoryAlgorithm Action Reward) (environment : MeasurableHistoryEnvironment Env Action Reward) (n : Nat) : ProbabilityTheory.condDistrib (fun sample : Env × ((k : Nat) -> Action × Reward) => (sample.2 (n + 1)).1) (fun sample => Preorder.frestrictLe n sample.2) (prior ⊗ₘ canonicalMeasurableEnvironmentTrajectoryKernel algorithm environment) =ᵐ[ (prior ⊗ₘ canonicalMeasurableEnvironmentTrajectoryKernel algorithm environment).map (fun sample => Preorder.frestrictLe n sample.2)] algorithm.policy n

Expose the posterior-invariance conclusion of the conditional process-density route without adjoining a fresh action sampler.

theorem finitePairReferencePosterior_ae_eq_condDistrib_of_conditionalProcessSource {Omega : Type u} {OmegaRef : Type v} {Env : Type w} {Action : Type x} {Reward : Type*} [MeasurableSpace Omega] [StandardBorelSpace Omega] [Nonempty Omega] [MeasurableSpace OmegaRef] [StandardBorelSpace OmegaRef] [Nonempty OmegaRef] [MeasurableSpace Env] [StandardBorelSpace Env] [Nonempty Env] [MeasurableSpace Action] [StandardBorelSpace Action] [Nonempty Action] [MeasurableSpace Reward] [StandardBorelSpace Reward] [Nonempty Reward] (mu : Measure Omega) [IsFiniteMeasure mu] (env : Omega -> Env) (action : Omega -> ActionTrace Action) (reward : Omega -> RewardTrace Reward) (referenceMu : Measure OmegaRef) [IsFiniteMeasure referenceMu] (referenceEnv : OmegaRef -> Env) (referenceAction : OmegaRef -> ActionTrace Action) (referenceReward : OmegaRef -> RewardTrace Reward) (algorithm referenceAlgorithm : HistoryAlgorithm Action Reward) (feedbackEnvironment : Env -> HistoryEnvironment Action Reward) (source : ConditionalHistoryAlgorithmDensitySource mu env action reward referenceMu referenceEnv referenceAction referenceReward algorithm referenceAlgorithm feedbackEnvironment) (n : Nat) : let actualHistory := fun omega => History.finitePairHistoryOfTrace (action omega) (reward omega) n let referenceHistory := fun omega => History.finitePairHistoryOfTrace (referenceAction omega) (referenceReward omega) n (referencePosterior referenceMu referenceEnv referenceHistory source.measurable_referenceEnv (History.measurable_finitePairHistoryOfTrace referenceAction referenceReward source.measurable_referenceAction source.measurable_referenceReward n)).kernel =ᵐ[mu.map actualHistory] ProbabilityTheory.condDistrib env actualHistory mu

Thompson's non-circular history algorithm: every policy is the posterior under one fixed reference trajectory, mapped through `bestAction`.

noncomputable def referencePosteriorHistoryAlgorithm {Env : Type u} {Action : Type v} {Reward : Type w} [MeasurableSpace Env] [StandardBorelSpace Env] [Nonempty Env] [MeasurableSpace Action] [MeasurableSpace Reward] [Nonempty Action] [Nonempty Reward] (prior : Measure Env) [IsProbabilityMeasure prior] (referenceAlgorithm : HistoryAlgorithm Action Reward) (environment : MeasurableHistoryEnvironment Env Action Reward) (bestAction : Env -> Action) (hbestAction : Measurable bestAction) : HistoryAlgorithm Action Reward where

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

theorem referencePosteriorHistoryAlgorithm_initialAction {Env : Type u} {Action : Type v} {Reward : Type w} [MeasurableSpace Env] [StandardBorelSpace Env] [Nonempty Env] [MeasurableSpace Action] [MeasurableSpace Reward] [Nonempty Action] [Nonempty Reward] (prior : Measure Env) [IsProbabilityMeasure prior] (referenceAlgorithm : HistoryAlgorithm Action Reward) (environment : MeasurableHistoryEnvironment Env Action Reward) (bestAction : Env -> Action) (hbestAction : Measurable bestAction) : (referencePosteriorHistoryAlgorithm prior referenceAlgorithm environment bestAction hbestAction).initialAction = prior.map bestAction

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

theorem referencePosteriorHistoryAlgorithm_policy {Env : Type u} {Action : Type v} {Reward : Type w} [MeasurableSpace Env] [StandardBorelSpace Env] [Nonempty Env] [MeasurableSpace Action] [MeasurableSpace Reward] [Nonempty Action] [Nonempty Reward] (prior : Measure Env) [IsProbabilityMeasure prior] (referenceAlgorithm : HistoryAlgorithm Action Reward) (environment : MeasurableHistoryEnvironment Env Action Reward) (bestAction : Env -> Action) (hbestAction : Measurable bestAction) (n : Nat) : (referencePosteriorHistoryAlgorithm prior referenceAlgorithm environment bestAction hbestAction).policy n = referenceActionKernel (prior ⊗ₘ canonicalMeasurableEnvironmentTrajectoryKernel referenceAlgorithm environment) Prod.fst (fun sample => History.finitePairHistoryOfTrace (environmentTrajectoryAction sample) (environmentTrajectoryReward sample) n) measurable_fst (History.measurable_finitePairHistoryOfTrace environmentTrajectoryAction environmentTrajectoryReward measurable_environmentTrajectoryAction_apply measurable_environmentTrajectoryReward_apply n) bestAction hbestAction

Probability matching for the action coordinate of one globally generated Thompson trajectory. Unlike the earlier finite-prefix sampler endpoint, the next action here is the actual successor coordinate of the same recursive trajectory whose history appears in the conditioning variable. The remaining support contract is the standard algorithm-density condition against the fixed reference algorithm. A finite uniform reference discharges that contract in the downstream specialization.

theorem referencePosteriorHistoryAlgorithm_trajectory_condDistrib_action_ae_eq_bestAction {Env : Type u} {Action : Type v} {Reward : Type w} [MeasurableSpace Env] [StandardBorelSpace Env] [Nonempty Env] [MeasurableSpace Action] [StandardBorelSpace Action] [Nonempty Action] [MeasurableSpace Reward] [StandardBorelSpace Reward] [Nonempty Reward] (prior : Measure Env) [IsProbabilityMeasure prior] (referenceAlgorithm : HistoryAlgorithm Action Reward) (environment : MeasurableHistoryEnvironment Env Action Reward) (bestAction : Env -> Action) (hbestAction : Measurable bestAction) (absolutelyContinuous : HistoryAlgorithmAbsolutelyContinuous (referencePosteriorHistoryAlgorithm prior referenceAlgorithm environment bestAction hbestAction) referenceAlgorithm) (n : Nat) : let algorithm := referencePosteriorHistoryAlgorithm prior referenceAlgorithm environment bestAction hbestAction let trajectoryKernel := canonicalMeasurableEnvironmentTrajectoryKernel algorithm environment let actualMeasure := prior ⊗ₘ trajectoryKernel let actualHistory := fun sample => History.finitePairHistoryOfTrace (environmentTrajectoryAction sample) (environmentTrajectoryReward sample) n let nextAction := fun sample => environmentTrajectoryAction sample (n + 1) ProbabilityTheory.condDistrib nextAction actualHistory actualMeasure =ᵐ[ actualMeasure.map actualHistory] ProbabilityTheory.condDistrib (bestAction ∘ Prod.fst) actualHistory actualMeasure

Concrete finite-action Thompson algorithm using one uniform reference process. The definition is non-circular: its posterior policy is computed from the uniform algorithm's trajectory, not from the Thompson trajectory being built.

noncomputable def uniformReferenceThompsonAlgorithm {Env : Type u} {Action : Type v} {Reward : Type w} [MeasurableSpace Env] [StandardBorelSpace Env] [Nonempty Env] [MeasurableSpace Action] [Fintype Action] [Nonempty Action] [MeasurableSpace Reward] [Nonempty Reward] (prior : Measure Env) [IsProbabilityMeasure prior] (environment : MeasurableHistoryEnvironment Env Action Reward) (bestAction : Env -> Action) (hbestAction : Measurable bestAction) : HistoryAlgorithm Action Reward

Premise-free finite-action probability matching on the actual globally recursive Thompson trajectory. Uniform full support discharges every algorithm-density absolute-continuity obligation internally.

theorem uniformReferenceThompsonAlgorithm_trajectory_condDistrib_action_ae_eq_bestAction {Env : Type u} {Action : Type v} {Reward : Type w} [MeasurableSpace Env] [StandardBorelSpace Env] [Nonempty Env] [MeasurableSpace Action] [StandardBorelSpace Action] [Fintype Action] [Nonempty Action] [MeasurableSpace Reward] [StandardBorelSpace Reward] [Nonempty Reward] (prior : Measure Env) [IsProbabilityMeasure prior] (environment : MeasurableHistoryEnvironment Env Action Reward) (bestAction : Env -> Action) (hbestAction : Measurable bestAction) (n : Nat) : let algorithm := uniformReferenceThompsonAlgorithm prior environment bestAction hbestAction let trajectoryKernel := canonicalMeasurableEnvironmentTrajectoryKernel algorithm environment let actualMeasure := prior ⊗ₘ trajectoryKernel let actualHistory := fun sample => History.finitePairHistoryOfTrace (environmentTrajectoryAction sample) (environmentTrajectoryReward sample) n let nextAction := fun sample => environmentTrajectoryAction sample (n + 1) ProbabilityTheory.condDistrib nextAction actualHistory actualMeasure =ᵐ[ actualMeasure.map actualHistory] ProbabilityTheory.condDistrib (bestAction ∘ Prod.fst) actualHistory actualMeasure