Teaching chapter 06 of 10 · Canonical route compiled

6. Thompson sampling and Bayesian regret

The scoped stationary finite-arm Thompson route compiles from posterior kernels and probability matching on the actual recursive generated history through clipped-UCB decomposition, latent-stream confidence, and an explicit Bayesian regret terminal.

How to read the status. It describes this page's canonical local Lean route, not completion of the cited textbook chapter or every extension listed below.

Orientation

Who should read this. Best read after the Probability layer.

Learning goals

Read a posterior as a kernel from histories to environments.
Transport conditional action-law equality onto the generated trajectory.
Understand why one compiled stationary theorem is not a universal posterior-sampling result.

Textbook crosswalk

Read the mathematics before the Lean interface

The Book Map is a curated formalization curriculum anchored in Bandit Algorithms, not a chapter-for-chapter reproduction of one book. Visible page labels use the numbered pages of its free online edition; source buttons use the PDF viewer's physical page index, which includes front matter and can therefore be larger. Companion papers cover algorithm-specific results.

Primary spine · free online edition

Bandit Algorithms

Tor Lattimore and Csaba Szepesvári

Location: Ch. 34 and Ch. 36
Pages: online pp. 421–436 and 460–475

Open at the cited pages

algorithm · ordered flow

Thompson sampling

Read top to bottom: each step supplies the state or proof fact used by the next one.

Condition
Form the posterior distribution of the unknown environment given observed history.
Sample a model
Draw one plausible environment from that posterior.
Optimize the sample
Choose an arm that is best in the sampled environment.
Observe and update
Record the reward and condition the posterior on the enlarged history.

Algorithm · explicit conventions

Posterior-sampling loop

This form makes probability matching visible: sample one environment from the current posterior, then act optimally for that sampled environment.

Posterior sample and selected arm. Formula renderer unavailable; readable fallback: Sample a latent environment from the posterior given the previous history, then choose the least-encoded arm with maximal mean in that sampled environment.\[\widetilde\theta_t\sim\Pi_t(\cdot\mid H_{t-1}),\qquad A_t=\min\operatorname*{arg\,max}_{a\in[k]}\mu_a(\widetilde\theta_t).\]

input: prior Q, likelihood/reward kernel, horizon n, fixed optimal-arm tie rule
initialize posterior Π_1 = Q
for t = 1,…,n:
    sample θ̃_t from Π_t given the visible history H_{t-1}
    choose A_t as the documented mean-optimal arm for θ̃_t
    observe reward X_t and update Π_{t+1} by conditioning on (A_t,X_t)

Source/Lean boundary. BanditRLlib constructs a canonical posterior kernel and a recursive stationary latent-arm-stream trajectory. Its selector carries an explicit pointwise mean-optimality contract, and its compiled endpoint is Bayesian rather than a universal frequentist theorem for every Thompson variant.

Worked example · follow one decision

Read one Thompson decision as probability matching

After the current history, suppose the posterior says arm 1 is optimal with probability 0.7 and arm 2 with probability 0.3. Thompson sampling turns that uncertainty directly into its next-action law.

Start from posterior uncertainty
The probabilities describe uncertainty about the true optimal arm under the Bayesian model, not empirical-mean scores.
Worked example step 1. Formula renderer unavailable; readable fallback: Given the previous history, the posterior probability that arm 1 is optimal is 0.7 and that arm 2 is optimal is 0.3.\[\Pr(A^\star=1\mid H_{t-1})=0.7,\qquad \Pr(A^\star=2\mid H_{t-1})=0.3.\]
Sample a plausible environment
If this posterior draw makes arm 2 optimal, the documented selector chooses arm 2 even though arm 1 is more likely to be truly optimal.
Worked example step 2. Formula renderer unavailable; readable fallback: A sampled environment is drawn from the posterior; in this illustrative draw arm 2 is best, so arm 2 is selected.\[\widetilde\theta_t\sim\Pi_t,\qquad \operatorname*{arg\,max}_a\mu_a(\widetilde\theta_t)=2\Longrightarrow A_t=2.\]
Recover the action probabilities
Across posterior draws, applying the same optimal-arm rule reproduces the posterior law of the true optimal arm.
Worked example step 3. Formula renderer unavailable; readable fallback: Conditioned on the history, Thompson sampling chooses arms 1 and 2 with probabilities 0.7 and 0.3.\[\Pr(A_t=1\mid H_{t-1})=0.7,\qquad \Pr(A_t=2\mid H_{t-1})=0.3.\]

Takeaway. Thompson sampling explores because posterior uncertainty remains: a 30 percent chance that arm 2 is optimal becomes a 30 percent chance of sampling it.

Scope. The numbers specify one hypothetical posterior state and do not perform a Bayesian update. The exact compiled route below constructs the posterior kernel and proves probability matching under its stated latent-environment and tie-breaking contracts.

Proof bridge · source to Lean

Why posterior sampling can be analyzed through probability matching

The analysis uses the fact that the action selected from a posterior sample and the truly optimal action have the same conditional distribution given the visible history.

Condition on the observed history
Given the current history, both the unknown environment and the fresh posterior sample are distributed according to the same posterior kernel.
Step 1 equation. Formula renderer unavailable; readable fallback: Conditionally on the previous history, the sampled and true latent environments share the current posterior law.\[\mathcal L(\widetilde\theta_t\mid H_{t-1})=\mathcal L(\theta_\star\mid H_{t-1})=\Pi_t.\]
Match the optimal-action law
Applying the same documented optimal-arm selector to those two latent environments gives equal conditional laws for the chosen arm and the optimal arm.
Step 2 equation. Formula renderer unavailable; readable fallback: For each arm, its conditional chance of being selected equals its conditional chance of being optimal.\[\mathbb P(A_t=a\mid H_{t-1})=\mathbb P(A^\star=a\mid H_{t-1}).\]
Rewrite Bayesian regret
Probability matching permits a clipped upper-confidence decomposition in which uncertainty and failure terms are separated before expectations are summed.
Step 3 equation. Formula renderer unavailable; readable fallback: Conditional Bayesian regret is bounded by an uncertainty term for the selected arm plus an upper-confidence failure term for the optimal arm.\[\mathbb E_t[\mu(A^\star)-\mu(A_t)]\le\mathbb E_t[U_t(A_t)-\mu(A_t)]+\mathbb E_t[\mu(A^\star)-U_t(A^\star)].\]
Sum uncertainty under the model contract
The bounded-reward, variance, and posterior assumptions then control the accumulated widths and failure charge, producing the source theorem's Bayesian rate.
Step 4 equation. Formula renderer unavailable; readable fallback: Under the stated Bayesian finite-arm assumptions, the accumulated terms yield a constant times square root of k n log n.\[BR_n\le C\sqrt{kn\log n}.\]

Reading boundary. This is a conceptual map of the Bayesian route. The exact compiled terminal has its own boundedness and variance terms and does not establish a frequentist guarantee for arbitrary Thompson-sampling implementations.

Source theorem · faithful restatement

Theorem 36.1 (Bayesian regret of Thompson sampling)

Original at online p. 461 (Chapter 36, §36.1) ↗

Probability matching turns posterior uncertainty about the best arm into an exploration policy.

Model: A k-armed Bayesian bandit environment with prior Q and arm laws indexed by the latent environment.
Assumptions: For every environment and arm, the centered reward law is 1-sub-Gaussian and its mean lies in [0,1]; optimal-arm ties use the algorithm's fixed rule.
Algorithm parameters: Prior Q, arm count k, and horizon n.
Regret notion: Bayesian regret BR_n, averaged over the prior, observations, and policy randomization.
Guarantee: BR_n is at most C√(kn log n) for a universal constant C.

Source mathematical statement. Formula renderer unavailable; readable fallback: In the stated Bayesian finite-armed setting, Thompson sampling has square-root-horizon Bayesian regret up to a logarithmic factor.\[BR_n\le C\sqrt{kn\log n}\quad\text{for the theorem's Bayesian finite-armed model and universal }C.\]

BanditRLlib relationship. BanditRLlib constructs a canonical posterior/kernel and generated stationary latent-arm-stream process. Its compiled terminal has explicit bounded-reward and variance terms and is not a blanket frequentist guarantee for all Thompson variants.

The mathematical content is restated in this site's notation; wording is ours. See online p. 461 (Chapter 36, §36.1) in the linked source for the original statement and full assumptions.

Natural-language and Lean side by side

The mathematical readings are explanatory summaries. The exact generated Lean statement and its source link remain authoritative for hypotheses, types, constants, and indexing.

A curated route through definitions, key bridges, and canonical terminals stays visible. 3 additional dependency, extension, or research-frontier notes are grouped below.

Mathematics ↔ Lean

The canonical posterior is the conditional environment law

Lean declarationBanditRLProof.PosteriorKernel.canonicalPosterior_kernel_ae_eq_condDistrib_of_pair_map_eq

Compiled

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.

Mathematical reading. Formula renderer unavailable; readable fallback: 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.\(\Pi(\cdot\mid H)=\mathcal L(E\mid H)\quad\text{a.e.}\)

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 and Lean reading notes

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.

Exact Lean statement

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

Open in the declaration catalog Open source at line 194

Mathematics ↔ Lean

Thompson actions probability-match the posterior

Lean declarationBanditRLProof.Thompson.uniformReferenceThompsonAlgorithm_trajectory_condDistrib_action_ae_eq_bestAction

Compiled

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.

Mathematical reading. Formula renderer unavailable; readable fallback: 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.\(\mathcal L(A_{n+1}\mid H_n)=\mathcal L(a^\star(E)\mid H_n).\)

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 and Lean reading notes

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

Exact Lean statement

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

Open in the declaration catalog Open source at line 507

Mathematics ↔ Lean

Bayesian regret decomposes through a clipped-UCB score

Lean declarationBanditRLProof.Thompson.integral_trajectoryBayesMeanRegret_eq_add_clippedUCB

Compiled

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.

Mathematical reading. Formula renderer unavailable; readable fallback: 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.\(\mathbb E R_n^{\mathrm{Bayes}}=\mathbb E\sum_{t<n}(\mu_{a^\star}-\mathrm{clip}(U_t(a^\star)))+\mathbb E\sum_{t<n}(\mathrm{clip}(U_t(A_t))-\mu_{A_t}).\)

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 and Lean reading notes

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

Exact Lean statement

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)))

Open in the declaration catalog Open source at line 428

Mathematics ↔ Lean

Finite-time Bayesian regret for the generated Thompson process

Lean declarationBanditRLProof.Thompson.stationaryLatentArmStreamCanonicalTrajectoryMeasure_integral_trajectoryBayesMeanRegret_le

Compiled

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.

Mathematical reading. Formula renderer unavailable; readable fallback: 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.\(\mathbb E[R_n^{\mathrm{Bayes}}]\le(2K+1)(u-l)+8\sqrt{\sigma^2Kn\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 and Lean reading notes

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

Exact Lean statement

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 := Env) (K := K) let augmentedBestAction := fun envStream : Env × UCB.ArmRewardStream K => bestAction envStream.1 let augmentedMean := fun envStream : Env × UCB.ArmRewardStream K => fun arm => mean envStream.1 arm let algorithm := uniformReferenceThompsonAlgorithm augmentedPrior feedbackEnvironment augmentedBestAction (hbestAction.comp measurable_fst) integral (stationaryLatentArmStreamCanonicalTrajectoryMeasure prior rewardKernel algorithm) (fun sample => trajectoryBayesMeanRegret augmentedMean augmentedBestAction sample n) <= (2 * K + 1) * (u - l) + 8 * Real.sqrt ((sigma2 : Real) * K * n * Real.log n)

Open in the declaration catalog Open source at line 3848

Explore 3 additional Lean teaching notes

Mathematics ↔ Lean

For the canonical one-step sampler, the sampled action conditioned on…

Lean declarationBanditRLProof.Thompson.canonicalSampler_condDistrib_action_ae_eq_bestAction

Compiled

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.

Mathematical reading. Formula renderer unavailable; readable fallback: 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.\(\mathcal L(A\mid H)=\mathcal L(a^\star(E)\mid H).\)

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 and Lean reading notes

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

Exact Lean statement

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)

Open in the declaration catalog Open source at line 271

Mathematics ↔ Lean

Expected comparator-relative mean regret on the generated trajectory splits…

Lean declarationBanditRLProof.Thompson.integral_trajectoryBayesMeanRegret_eq_add_historyScore

Compiled

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.

Mathematical reading. Formula renderer unavailable; readable fallback: 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.\(\mathbb E R_n^{\mathrm{Bayes}}=\mathbb E\sum_{t<n}(\mu_{a^\star}-U_t(a^\star))+\mathbb E\sum_{t<n}(U_t(A_t)-\mu_{A_t}).\)

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 and Lean reading notes

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

Exact Lean statement

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)))

Open in the declaration catalog Open source at line 362

Mathematics ↔ Lean

For the canonical latent-stream environment, every generated reward…

Lean declarationBanditRLProof.Thompson.canonicalLatentArmStreamTrajectory_reward_eq_rewardFromArmStream_ae

Compiled

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.

Mathematical reading. Formula renderer unavailable; readable fallback: 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.\(Y_t=Z_{A_t,N_{A_t}(t)}\quad\text{for all }t\text{ a.e.}\)

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 and Lean reading notes

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

Exact Lean statement

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 := Env) (K := K)) (env, stream)] UCB.rewardFromArmStream canonicalHistoryTrajectoryAction (fun _ => stream)

Open in the declaration catalog Open source at line 455

Maintainer contract

Open the canonical completion definition and blockers

Complete in the stationary canonical textbook scope when a probability prior and likelihood construct the posterior kernel, a measurable selector with the explicit pointwise IsOptimalMeanSelector contract gives posterior best-action pushforward and actual-recursive-trajectory probability matching, score transport yields Bayesian and clipped-UCB decompositions, a stationary Markov reward kernel constructs the augmented latent arm stream with a.e. generated-reward support, upper/lower confidence consumers compile, and the generated trajectory satisfies E[R_n^Bayes] <= (2K+1)(u-l)+8 sqrt(sigma^2 K n log n) under the exact optimality, measurable bounded-mean, and centered sub-Gaussian assumptions.

Remaining blockers

No remaining blocker inside this stationary canonical scope: the public canary types probability matching on the actual recursive history and concretely instantiates the final theorem with a one-arm stationary Gaussian Markov source while explicitly proving its mean-optimal selector contract. The items below remain separate extensions.

Chapter implementation status

The compact summary keeps the reading route visible. Open it for source-linked declarations and exact remaining gaps.

Open 7 implementation records6 compiled · 1 partial · 0 blocked · 0 planned

Milestone	Status	Lean declaration	Remaining gap
Posterior kernel equals the conditional environment law	Compiled	`BanditRLProof.PosteriorKernel.canonicalPosterior_kernel_ae_eq_condDistrib_of_pair_map_eq`	—
Canonical one-step probability matching	Compiled	`BanditRLProof.Thompson.canonicalSampler_condDistrib_action_ae_eq_bestAction`	—
Probability matching on the actual recursive trajectory	Compiled	`BanditRLProof.Thompson.uniformReferenceThompsonAlgorithm_trajectory_condDistrib_action_ae_eq_bestAction`	—
Bayesian regret and clipped-UCB decomposition	Compiled	`BanditRLProof.Thompson.integral_trajectoryBayesMeanRegret_eq_add_historyScoreBanditRLProof.Thompson.integral_trajectoryBayesMeanRegret_eq_add_clippedUCB`	—
Generated rewards align with the stationary latent arm stream	Compiled	`BanditRLProof.Thompson.canonicalLatentArmStreamTrajectory_reward_eq_rewardFromArmStream_ae`	—
Stationary latent-arm-stream Thompson regret	Compiled	`BanditRLProof.Thompson.IsOptimalMeanSelectorBanditRLProof.Thompson.stationaryLatentArmStreamCanonicalTrajectoryMeasure_integral_trajectoryBayesMeanRegret_le`	—
General Thompson/LML Bayesian port	Partial	`BanditRLProof.Thompson.stationaryLatentArmStreamCanonicalTrajectoryMeasure_integral_trajectoryBayesMeanRegret_le`	Add posterior-law producers for broader models. Close the exact upstream compatibility gate.

Open boundaries

Arbitrary nonstationary posterior models, contextual or linear Thompson sampling, posterior-sampling RL, and user-supplied posteriors without a law producer remain extensions.
Sharp problem-dependent or asymptotically optimal constants are not claimed by the compiled stationary terminal.
Exact LeanMachineLearning declaration/toolchain identity remains independently blocked; LML cards are retrieval evidence, not imported proof terms.

All Lean modules in this chapter

Open the complete module list (11 modules)

Module	Declarations	Project imports	Status
`BanditRLProof.Algorithms.Thompson`	14	2	Compiled
`BanditRLProof.Algorithms.ThompsonAlgorithmDensity`	11	1	Compiled
`BanditRLProof.Algorithms.ThompsonAlgorithmDensityProcess`	31	2	Compiled
`BanditRLProof.Algorithms.ThompsonBayesRegretDecomposition`	16	2	Compiled
`BanditRLProof.Algorithms.ThompsonCanonicalSampler`	14	1	Compiled
`BanditRLProof.Algorithms.ThompsonCanonicalTrajectory`	31	1	Compiled
`BanditRLProof.Algorithms.ThompsonClippedUCBScore`	20	3	Compiled
`BanditRLProof.Algorithms.ThompsonMeasurableTrajectory`	31	2	Compiled
`BanditRLProof.Algorithms.ThompsonRecursiveSampler`	15	1	Compiled
`BanditRLProof.Algorithms.ThompsonReferencePolicy`	17	2	Compiled
`BanditRLProof.Algorithms.ThompsonStationaryReward`	97	2	Compiled