2.7. Online.Bandit.Algorithms.TS🔗

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 hK Q κ: a Thompson sampling algorithm with actions in Fin K given hK : 0 < K, 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.

Module LeanMachineLearning.Online.Bandit.Algorithms.TS contains 6 exposed declarations.

`policy`🔗

DefinitionBandits.TS.policy

Details

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.

def

Bandits.TS.policy.{u_1} {K : ℕ} {𝓔 : Type u_1} [MeasurableSpace 𝓔]
  [StandardBorelSpace 𝓔] [Nonempty 𝓔] (hK : 0 < K)
  (Q : MeasureTheory.Measure 𝓔) [MeasureTheory.IsProbabilityMeasure Q]
  (κ : ProbabilityTheory.Kernel (𝓔 × Fin K) ℝ)
  [ProbabilityTheory.IsMarkovKernel κ] (n : ℕ) :
  ProbabilityTheory.Kernel (↥(Finset.Iic n) → Fin K × ℝ) (Fin K)
Bandits.TS.policy.{u_1} {K : ℕ}
  {𝓔 : Type u_1} [MeasurableSpace 𝓔]
  [StandardBorelSpace 𝓔] [Nonempty 𝓔]
  (hK : 0 < K)
  (Q : MeasureTheory.Measure 𝓔)
  [MeasureTheory.IsProbabilityMeasure Q]
  (κ :
    ProbabilityTheory.Kernel (𝓔 × Fin K)
      ℝ)
  [ProbabilityTheory.IsMarkovKernel κ]
  (n : ℕ) :
  ProbabilityTheory.Kernel
    (↥(Finset.Iic n) → Fin K × ℝ) (Fin K)

Code

noncomputable
def TS.policy (hK : 0 < K) (Q : Measure 𝓔) [IsProbabilityMeasure Q] (κ : Kernel (𝓔 × Fin K) ℝ)
    [IsMarkovKernel κ] (n : ℕ) : Kernel (Iic n → (Fin K) × ℝ) (Fin K) :=
  have : Nonempty (Fin K) := Fin.pos_iff_nonempty.mp hK
  (IT.bayesTrajMeasurePosterior Q κ uniformAlgorithm n).map (bestAction κ id)

Body uses (3)

Used by (2)

Actions: Source · Open Issue

`instIsMarkovKernelForallSubtypeNatMemFinsetIicProdFinRealPolicy`🔗

InstanceBandits.instIsMarkovKernelForallSubtypeNatMemFinsetIicProdFinRealPolicy

Details

No docstring.

theorem

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

Code

instance {hK : 0 < K} {Q : Measure 𝓔} [IsProbabilityMeasure Q] {κ : Kernel (𝓔 × Fin K) ℝ}
    [IsMarkovKernel κ] {n : ℕ} : IsMarkovKernel (TS.policy hK Q κ n)

Type uses (1)

policy

Body uses (5)

Used by (1)

tsAlgorithm

Actions: Source · Open Issue

Proof

Kernel.IsMarkovKernel.map _ (by fun_prop)

`initialPolicy`🔗

DefinitionBandits.TS.initialPolicy

Details

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

def

Bandits.TS.initialPolicy.{u_1} {K : ℕ} {𝓔 : Type u_1}
  [MeasurableSpace 𝓔] (hK : 0 < K) (Q : MeasureTheory.Measure 𝓔)
  (κ : ProbabilityTheory.Kernel (𝓔 × Fin K) ℝ) :
  MeasureTheory.Measure (Fin K)
Bandits.TS.initialPolicy.{u_1} {K : ℕ}
  {𝓔 : Type u_1} [MeasurableSpace 𝓔]
  (hK : 0 < K)
  (Q : MeasureTheory.Measure 𝓔)
  (κ :
    ProbabilityTheory.Kernel (𝓔 × Fin K)
      ℝ) :
  MeasureTheory.Measure (Fin K)

Code

noncomputable
def TS.initialPolicy (hK : 0 < K) (Q : Measure 𝓔) (κ : Kernel (𝓔 × Fin K) ℝ) : Measure (Fin K) :=
  have : Nonempty (Fin K) := Fin.pos_iff_nonempty.mp hK
  Q.map (bestAction κ id)

Body uses (1)

bestAction

Used by (2)

Actions: Source · Open Issue

`instIsProbabilityMeasureFinInitialPolicy`🔗

InstanceBandits.instIsProbabilityMeasureFinInitialPolicy

Details

No docstring.

theorem

Bandits.instIsProbabilityMeasureFinInitialPolicy.{u_1} {K : ℕ}
  {𝓔 : Type u_1} [MeasurableSpace 𝓔] {hK : 0 < K}
  {Q : MeasureTheory.Measure 𝓔} [MeasureTheory.IsProbabilityMeasure Q]
  {κ : ProbabilityTheory.Kernel (𝓔 × Fin K) ℝ} :
  MeasureTheory.IsProbabilityMeasure (TS.initialPolicy hK Q κ)
Bandits.instIsProbabilityMeasureFinInitialPolicy.{u_1}
  {K : ℕ} {𝓔 : Type u_1}
  [MeasurableSpace 𝓔] {hK : 0 < K}
  {Q : MeasureTheory.Measure 𝓔}
  [MeasureTheory.IsProbabilityMeasure Q]
  {κ :
    ProbabilityTheory.Kernel (𝓔 × Fin K)
      ℝ} :
  MeasureTheory.IsProbabilityMeasure
    (TS.initialPolicy hK Q κ)

Code

instance {hK : 0 < K} {Q : Measure 𝓔} [IsProbabilityMeasure Q] {κ : Kernel (𝓔 × Fin K) ℝ} :
    IsProbabilityMeasure (TS.initialPolicy hK Q κ)

Type uses (1)

initialPolicy

Body uses (2)

Used by (1)

tsAlgorithm

Actions: Source · Open Issue

Proof

Measure.isProbabilityMeasure_map (by fun_prop)

`tsAlgorithm`🔗

DefinitionBandits.tsAlgorithm

Details

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.

def

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

Code

noncomputable
def tsAlgorithm (hK : 0 < K) (Q : Measure 𝓔) [IsProbabilityMeasure Q] (κ : Kernel (𝓔 × Fin K) ℝ)
    [IsMarkovKernel κ] : Algorithm (Fin K) ℝ where
  policy := TS.policy hK Q κ
  p0 := TS.initialPolicy hK Q κ

Type uses (1)

Algorithm

Body uses (4)

Used by (4)

Actions: Source · Open Issue

`hasCondDistrib_action`🔗

LemmaBandits.TS.hasCondDistrib_action

Details

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.

theorem

Bandits.TS.hasCondDistrib_action.{u_1, u_2} {K : ℕ} [Nonempty (Fin 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] (hK : 0 < K)
  (h : Learning.IsBayesAlgEnvSeq Q κ (tsAlgorithm hK Q κ) E A R P)
  (n : ℕ) :
  ProbabilityTheory.HasCondDistrib (A (n + 1)) (Learning.history A R n)
    𝓛[Learning.IsBayesAlgEnvSeq.bestAction κ E | Learning.history A R n;
      P]
    P
Bandits.TS.hasCondDistrib_action.{u_1,
    u_2}
  {K : ℕ} [Nonempty (Fin 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]
  (hK : 0 < K)
  (h :
    Learning.IsBayesAlgEnvSeq Q κ
      (tsAlgorithm hK Q κ) E A R P)
  (n : ℕ) :
  ProbabilityTheory.HasCondDistrib
    (A (n + 1)) (Learning.history A R n)
    𝓛[Learning.IsBayesAlgEnvSeq.bestAction
        κ E |
      Learning.history A R n; P]
    P

Code

lemma TS.hasCondDistrib_action (hK : 0 < K) (h : IsBayesAlgEnvSeq Q κ (tsAlgorithm hK Q κ) E A R P)
    (n : ℕ) :
    HasCondDistrib (A (n + 1)) (history A R n)
      (condDistrib (bestAction κ E) (history A R n) P) P where
  aemeasurable

Type uses (4)

Body uses (14)

Used by (1)

integral_ucb_action_eq_integral_ucb_bestAction

Actions: Source · Open Issue

Proof

((measurable_history h.measurable_action h.measurable_feedback n).prodMk
      (h.measurable_action (n + 1))).aemeasurable
  map_eq := by
    have hm : Measurable (bestAction κ id) := by fun_prop
    rw [(h.hasCondDistrib_action' n).map_eq]
    refine Measure.compProd_congr ?_
    calc
      _ =ᵐ[P.map (history A R n)]
          (IT.bayesTrajMeasurePosterior Q κ uniformAlgorithm n).map (bestAction κ id) := by rfl
      _ =ᵐ[P.map (history A R n)]
          (condDistrib E (history A R n) P).map (bestAction κ id) := by
          filter_upwards [(h.hasCondDistrib_env_history
            (IT.isBayesAlgEnvSeq_bayesTrajMeasure Q κ uniformAlgorithm)
            absolutelyContinuous_uniformAlgorithm n).condDistrib_eq] with _ hc
          simp_rw [Kernel.map_apply _ hm, IT.bayesTrajMeasurePosterior, hc]
      _ =ᵐ[P.map (history A R n)]
          condDistrib (bestAction κ E) (history A R n) P :=
          (condDistrib_comp (history A R n) h.measurable_param.aemeasurable hm).symm

2.7. Online.Bandit.Algorithms.TS🔗

policy🔗

instIsMarkovKernelForallSubtypeNatMemFinsetIicProdFinRealPolicy🔗

initialPolicy🔗

instIsProbabilityMeasureFinInitialPolicy🔗

tsAlgorithm🔗

hasCondDistrib_action🔗

`policy`🔗

`instIsMarkovKernelForallSubtypeNatMemFinsetIicProdFinRealPolicy`🔗

`initialPolicy`🔗

`instIsProbabilityMeasureFinInitialPolicy`🔗

`tsAlgorithm`🔗

`hasCondDistrib_action`🔗