6. Thompson sampling and Bayesian regret

Plain-English statement. If an environment and observed history have the canonical prior-likelihood joint law, then the canonical posterior kernel equals the conditional law of the environment given that history almost everywhere.

Intuition

A posterior is a measurable kernel from histories to environments; the theorem identifies that constructed kernel with the measure-theoretic conditional distribution.

Why it is needed

Probability matching is valid only after the algorithmic posterior is tied to the actual environment-history law.

Place in the proof

It is the posterior-law root of the Chapter 6 proof DAG.

Proof idea

Use uniqueness of regular conditional distributions under the equality of the observed pair pushforward and the canonical prior-likelihood joint measure.

Lean reading notes

The theorem requires Standard Borel and nonempty environment, measurable environment/history maps, a probability prior, a Markov likelihood kernel, and exact pair-law equality. It does not accept an arbitrary posterior kernel.

Teaching dependencies

No direct teaching dependency recorded.

theorem canonicalPosterior_kernel_ae_eq_condDistrib_of_pair_map_eq {Omega : Type*} [MeasurableSpace Omega] [StandardBorelSpace Env] [Nonempty Env] (mu : Measure Omega) [IsFiniteMeasure mu] (env : Omega -> Env) (history : Omega -> History) (henv : Measurable env) (hhistory : Measurable history) (prior : Measure Env) [IsProbabilityMeasure prior] (likelihood : ProbabilityTheory.Kernel Env History) [ProbabilityTheory.IsMarkovKernel likelihood] (hpair : mu.map (fun omega => (env omega, history omega)) = canonicalJointMeasure prior likelihood) : (canonicalPosterior prior likelihood).kernel =ᵐ[mu.map history] ProbabilityTheory.condDistrib env history mu

Plain-English statement. For the canonical one-step sampler, the sampled action conditioned on history has the same law as the best action of the latent environment conditioned on that history.

Intuition

Draw an environment from the posterior and act optimally for that draw; pushing the posterior through bestAction is exactly the posterior optimal-action law.

Why it is needed

This is the local probability-matching identity later transported to every successor action of the recursive algorithm.

Place in the proof

It consumes posterior-kernel correctness and feeds the recursive trajectory sampler.

Proof idea

Construct the canonical sampler measure, apply posterior equals conditional environment law, and map both sides through the measurable best-action selector.

Lean reading notes

Standard Borel/nonempty environment and action spaces, a probability prior, Markov likelihood, and measurable bestAction are explicit. This is one-step matching, not yet a generated multi-round regret theorem.

Teaching dependencies

BanditRLProof.PosteriorKernel.canonicalPosterior_kernel_ae_eq_condDistrib_of_pair_map_eq

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)

Plain-English statement. On the actual globally recursive Thompson trajectory, the action at round n+1 conditioned on the trajectory's own finite history through n probability-matches the posterior best action.

Intuition

The uniform reference policy supplies full support, so the posterior sampler can be recursively coupled without assuming a second unrelated action process.

Why it is needed

Bayesian regret decomposition needs matching for the actions that the generated algorithm actually takes.

Place in the proof

It is the bridge from the canonical one-step sampler to the generated finite-history score identities.

Proof idea

Build the recursive history algorithm and canonical environment trajectory kernel, extract the actual finite history, apply density and conditional-law invariance, and identify the successor coordinate.

Lean reading notes

The canary restates the complete algorithm, trajectoryKernel, actualMeasure, actualHistory, and nextAction let chain. It is not an adjoined sampler theorem.

Teaching dependencies

BanditRLProof.Thompson.canonicalSampler_condDistrib_action_ae_eq_bestAction

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

Plain-English statement. Expected comparator-relative mean regret on the generated trajectory splits exactly into a selector-score gap and a selected-action score gap for any integrable finite-history score; the Bayesian-regret reading additionally requires a mean-optimal selector.

Intuition

Add and subtract the same score; probability matching makes the expected score of the sampled action equal the expected score of the latent best action.

Why it is needed

It turns posterior-law equality into the two error terms that concentration can control.

Place in the proof

It follows recursive probability matching and precedes the concrete clipped-UCB specialization.

Proof idea

Apply the finite-history conditional-distribution equality to each score, integrate the score identity, sum over the finite horizon, and regroup the mean differences.

Lean reading notes

The theorem retains separate integrability hypotheses for selector means, selected means, selected scores, and selector scores. The decomposition is valid for any measurable selector; `trajectoryBayesMeanRegret` is genuinely Bayesian pseudo-regret only when `IsOptimalMeanSelector mean bestAction` is available.

Teaching dependencies

BanditRLProof.Thompson.uniformReferenceThompsonAlgorithm_trajectory_condDistrib_action_ae_eq_bestAction

theorem integral_trajectoryBayesMeanRegret_eq_add_historyScore {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) (mean : Env -> Action -> Real) (score : HistoryActionScore Action Reward) (horizon : Nat) (hmeanBest : Integrable (fun sample : Env × ((n : Nat) -> Action × Reward) => mean sample.1 (bestAction sample.1)) (prior ⊗ₘ canonicalMeasurableEnvironmentTrajectoryKernel (uniformReferenceThompsonAlgorithm prior environment bestAction hbestAction) environment)) (hmeanAction : forall t : Nat, t < horizon -> Integrable (fun sample : Env × ((n : Nat) -> Action × Reward) => mean sample.1 (environmentTrajectoryAction sample t)) (prior ⊗ₘ canonicalMeasurableEnvironmentTrajectoryKernel (uniformReferenceThompsonAlgorithm prior environment bestAction hbestAction) environment)) (hscoreAction : forall t : Nat, t < horizon -> Integrable (fun sample : Env × ((n : Nat) -> Action × Reward) => trajectoryHistoryScore score sample t) (prior ⊗ₘ canonicalMeasurableEnvironmentTrajectoryKernel (uniformReferenceThompsonAlgorithm prior environment bestAction hbestAction) environment)) (hscoreBest : forall t : Nat, t < horizon -> Integrable (fun sample : Env × ((n : Nat) -> Action × Reward) => trajectoryBestHistoryScore score bestAction sample t) (prior ⊗ₘ canonicalMeasurableEnvironmentTrajectoryKernel (uniformReferenceThompsonAlgorithm prior environment bestAction hbestAction) environment)) : let algorithm := uniformReferenceThompsonAlgorithm prior environment bestAction hbestAction let actualMeasure := prior ⊗ₘ canonicalMeasurableEnvironmentTrajectoryKernel algorithm environment integral actualMeasure (fun sample => trajectoryBayesMeanRegret mean bestAction sample horizon) = integral actualMeasure (fun sample => ∑ t ∈ range horizon, (mean sample.1 (bestAction sample.1) - trajectoryBestHistoryScore score bestAction sample t)) + integral actualMeasure (fun sample => ∑ t ∈ range horizon, (trajectoryHistoryScore score sample t - mean sample.1 (environmentTrajectoryAction sample t)))

Plain-English statement. Choosing the measurable bounded clipped-UCB history score specializes the comparator-relative decomposition to confidence terms suitable for stationary reward tails; optimality is imposed at the final Bayesian-regret terminal.

Intuition

Clipping keeps scores inside the known mean range while empirical means plus widths retain optimism with high probability.

Why it is needed

This is the exact bridge from probability matching to concentration and the final finite regret bound.

Place in the proof

It consumes the history-score decomposition and feeds the two stationary clipped-score expectation inequalities.

Proof idea

Prove the clipped score is measurable and uniformly bounded, automatically obtain the needed integrability, and instantiate the general history-score equality.

Lean reading notes

The mean surface must be measurable and contained in [l,u]. The theorem is comparator-relative algebra and does not itself assert selector optimality or provide the stationary concentration bounds.

Teaching dependencies

BanditRLProof.Thompson.integral_trajectoryBayesMeanRegret_eq_add_historyScore

theorem integral_trajectoryBayesMeanRegret_eq_add_clippedUCB {Env : Type u} {K : Nat} [MeasurableSpace Env] [StandardBorelSpace Env] [Nonempty Env] [Nonempty (Fin K)] (prior : Measure Env) [IsProbabilityMeasure prior] (environment : MeasurableHistoryEnvironment Env (Fin K) Real) (bestAction : Env -> Fin K) (hbestAction : Measurable bestAction) (mean : Env -> Fin K -> Real) (hmean : Measurable (fun pair : Env × Fin K => mean pair.1 pair.2)) (l u sigma2 delta : Real) (hlu : l <= u) (hmeanMem : forall env arm, mean env arm ∈ Set.Icc l u) (horizon : Nat) : let algorithm := uniformReferenceThompsonAlgorithm prior environment bestAction hbestAction let actualMeasure := prior ⊗ₘ canonicalMeasurableEnvironmentTrajectoryKernel algorithm environment integral actualMeasure (fun sample => trajectoryBayesMeanRegret mean bestAction sample horizon) = integral actualMeasure (fun sample => ∑ t ∈ range horizon, (mean sample.1 (bestAction sample.1) - clippedUCB l u sigma2 delta (environmentTrajectoryAction sample) (environmentTrajectoryReward sample) (bestAction sample.1) t)) + integral actualMeasure (fun sample => ∑ t ∈ range horizon, (clippedUCB l u sigma2 delta (environmentTrajectoryAction sample) (environmentTrajectoryReward sample) (environmentTrajectoryAction sample t) t - mean sample.1 (environmentTrajectoryAction sample t)))

Plain-English statement. For the canonical latent-stream environment, every generated reward coordinate agrees almost everywhere with the next unused reward coordinate of the selected arm's stationary stream.

Intuition

A latent infinite reward stream for each arm turns adaptive sampling into coordinate selection without changing the actual recursive policy.

Why it is needed

Stationary empirical-mean tails must apply to the rewards actually observed by Thompson sampling, not to an independent offline sample.

Place in the proof

It connects the recursive generated trajectory to arm-stream concentration and clipped-score expectation bounds.

Proof idea

Use the canonical step-kernel construction and induction over finite trajectory prefixes to identify each feedback draw with rewardFromArmStream at the selected pull count.

Lean reading notes

The equality is almost everywhere under the canonical generated trajectory kernel for each latent environment/stream input. It is a support/alignment theorem, not independence stated by fiat.

Teaching dependencies

BanditRLProof.Thompson.uniformReferenceThompsonAlgorithm_trajectory_condDistrib_action_ae_eq_bestAction

theorem canonicalLatentArmStreamTrajectory_reward_eq_rewardFromArmStream_ae {Env : Type u} {K : Nat} [MeasurableSpace Env] [StandardBorelSpace Env] [NeZero K] (algorithm : HistoryAlgorithm (Fin K) Real) (env : Env) (stream : UCB.ArmRewardStream K) : canonicalHistoryTrajectoryReward =ᵐ[ canonicalMeasurableEnvironmentTrajectoryKernel algorithm (latentArmStreamMeasurableHistoryEnvironment (Env

Plain-English statement. For the canonical stationary latent-arm-stream Thompson process, expected Bayesian mean regret is at most (2K+1)(u-l) plus 8 times the square root of sigma-squared K n log n.

Intuition

Posterior sampling matches the law of the optimal action, so a carefully chosen confidence decomposition can compare the sampled and optimal actions in expectation.

Why it is needed

It is the final stationary theorem of the local Thompson route and demonstrates that posterior-law construction reaches an actual regret endpoint.

Place in the proof

It closes the scoped stationary canonical Chapter 6 route while BRL-TS-BAYES-001 and direct upstream identity remain separate.

Proof idea

Construct actual and reference trajectories, prove posterior-action conditional-law equality, integrate the Bayesian regret decomposition, apply clipped-UCB bounds, and discharge stationary reward tails.

Lean reading notes

The exact statement requires a probability prior, Standard Borel nonempty environment, finite nonempty arms, stationary Markov reward kernel, measurable bestAction, pointwise `IsOptimalMeanSelector mean bestAction`, a measurable mean surface, means in [l,u], centered sub-Gaussian MGF, nonzero variance proxy, and the canonical augmented latent stream. It is not a universal or sharp-asymptotic Thompson theorem.

Teaching dependencies

BanditRLProof.Thompson.integral_trajectoryBayesMeanRegret_eq_add_clippedUCB, BanditRLProof.Thompson.canonicalLatentArmStreamTrajectory_reward_eq_rewardFromArmStream_ae, BanditRLProof.Thompson.stationaryLatentArmStreamCanonicalTrajectoryMeasure_integral_sum_mean_bestAction_sub_clippedUCB_le, BanditRLProof.Thompson.stationaryLatentArmStreamCanonicalTrajectoryMeasure_integral_sum_clippedUCB_action_sub_mean_le

theorem stationaryLatentArmStreamCanonicalTrajectoryMeasure_integral_trajectoryBayesMeanRegret_le {Env : Type u} {K : Nat} [MeasurableSpace Env] [StandardBorelSpace Env] [Nonempty Env] [NeZero K] (prior : Measure Env) [IsProbabilityMeasure prior] (rewardKernel : Kernel (Env × Fin K) Real) [IsMarkovKernel rewardKernel] (bestAction : Env -> Fin K) (hbestAction : Measurable bestAction) (mean : Env -> Fin K -> Real) (hbest : IsOptimalMeanSelector mean bestAction) (hmeas_mean : Measurable (fun input : Env × Fin K => mean input.1 input.2)) (l u : Real) (hlu : l <= u) (hmeanMem : forall env arm, mean env arm ∈ Set.Icc l u) (sigma2 : NNReal) (hsubG : forall env arm, HasSubgaussianMGF (fun reward => reward - mean env arm) sigma2 (rewardKernel (env, arm))) (hsigma2 : sigma2 ≠ 0) (n : Nat) : let augmentedPrior := stationaryLatentArmStreamPrior prior rewardKernel let feedbackEnvironment := latentArmStreamMeasurableHistoryEnvironment (Env