Thompson Sampling

This file defines the Thompson sampling algorithm. This algorithm samples an action according to its probability of being optimal under the posterior over environments given the history so far.

Main definitions

• tsAlgorithm Q κ: a Thompson sampling algorithm with actions in Fin K (for K ≠ 0), given a prior distribution over parameters Q : Measure 𝓔 and a Markov kernel κ : Kernel (𝓔 × Fin K) ℝ. This kernel defines how a parameter e : 𝓔 gives rise to a stationary environment: stationaryEnv (κ.sectR e) : Environment (Fin K) ℝ.

Main results

• hasCondDistrib_action : if Thompson sampling has the correct prior over environments, then the conditional distribution of the next action given the history so far is equal to the conditional distribution of the best action given the history so far.

noncomputable def Bandits.TS.policy {K : ℕ} {𝓔 : Type u_1} [MeasurableSpace 𝓔] [StandardBorelSpace 𝓔] [Nonempty 𝓔] [NeZero K] (Q : MeasureTheory.Measure 𝓔) [MeasureTheory.IsProbabilityMeasure Q] (κ : ProbabilityTheory.Kernel (𝓔 × Fin K) ℝ) [ProbabilityTheory.IsMarkovKernel κ] (n : ℕ) : ProbabilityTheory.Kernel (Learning.Hist Unit (Fin K) ℝ n × Unit) (Fin K)

The Thompson sampling policy samples an action according to its probability of being optimal under the posterior over environments given the history so far. The posterior under a uniform algorithm is used to avoid a circular definition.

Equations

• One or more equations did not get rendered due to their size.

instance Bandits.instIsMarkovKernelProdHistUnitFinRealPolicy {K : ℕ} {𝓔 : Type u_1} [MeasurableSpace 𝓔] [StandardBorelSpace 𝓔] [Nonempty 𝓔] [NeZero K] {Q : MeasureTheory.Measure 𝓔} [MeasureTheory.IsProbabilityMeasure Q] {κ : ProbabilityTheory.Kernel (𝓔 × Fin K) ℝ} [ProbabilityTheory.IsMarkovKernel κ] {n : ℕ} : ProbabilityTheory.IsMarkovKernel (TS.policy Q κ n)

noncomputable def Bandits.tsAlgorithm {K : ℕ} {𝓔 : Type u_1} [MeasurableSpace 𝓔] [StandardBorelSpace 𝓔] [Nonempty 𝓔] [NeZero K] (Q : MeasureTheory.Measure 𝓔) [MeasureTheory.IsProbabilityMeasure Q] (κ : ProbabilityTheory.Kernel (𝓔 × Fin K) ℝ) [ProbabilityTheory.IsMarkovKernel κ] : Learning.Algorithm Unit (Fin K) ℝ

The Thompson sampling algorithm with actions in Fin K, where Q : Measure 𝓔 is a prior distribution over parameters, and κ : Kernel (𝓔 × Fin K) ℝ is a Markov kernel that defines the stationary environment stationaryEnv (κ.sectR e) that corresponds to a parameter e : 𝓔.

At every time n, the Thompson sampling policy uses the posterior over the parameters given the history up to time n to derive the probability of each action being optimal. The action for time n is sampled according to these probabilities.

Equations

• Bandits.tsAlgorithm Q κ = { policy := Bandits.TS.policy Q κ, isMarkovKernel_policy := ⋯ }

theorem Bandits.TS.p0_tsAlgorithm {K : ℕ} [NeZero K] {𝓔 : Type u_2} [MeasurableSpace 𝓔] [StandardBorelSpace 𝓔] [Nonempty 𝓔] {Q : MeasureTheory.Measure 𝓔} [MeasureTheory.IsProbabilityMeasure Q] {κ : ProbabilityTheory.Kernel (𝓔 × Fin K) ℝ} [ProbabilityTheory.IsMarkovKernel κ] : (tsAlgorithm Q κ).p0 () = MeasureTheory.Measure.map (Learning.IsBayesAlgEnvSeq.bestAction κ id) Q

The first action of Thompson sampling is sampled according to its probability of being optimal under the prior over environments.

theorem Bandits.TS.hasCondDistrib_action {K : ℕ} [NeZero K] {Ω : Type u_1} [MeasurableSpace Ω] {𝓔 : Type u_2} [MeasurableSpace 𝓔] [StandardBorelSpace 𝓔] [Nonempty 𝓔] {E : Ω → 𝓔} {A : ℕ → Ω → Fin K} {R : ℕ → Ω → ℝ} {Q : MeasureTheory.Measure 𝓔} [MeasureTheory.IsProbabilityMeasure Q] {κ : ProbabilityTheory.Kernel (𝓔 × Fin K) ℝ} [ProbabilityTheory.IsMarkovKernel κ] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] (h : Learning.IsBayesAlgEnvSeq Q κ (tsAlgorithm Q κ) E A R P) (n : ℕ) : ProbabilityTheory.HasCondDistrib (A n) (Learning.history (Learning.noObs Ω) A R n) 𝓛[Learning.IsBayesAlgEnvSeq.bestAction κ E | Learning.history (Learning.noObs Ω) A R n; P] P

If Thompson sampling has the correct prior over environments, then the conditional distribution of the next action given the history so far is equal to the conditional distribution of the best action given the history so far.