Round-Robin algorithm #
That algorithm chooses each of finitely many actions in a round-robin fashion.
That is, if there are K actions numbered from 0 to K - 1, then at time n it chooses
he action n % K.
Main definitions #
roundRobinAlgorithm K: the Round-Robin algorithm onKactions.
noncomputable def
Learning.roundRobinAlgorithm
{𝓞 : Type u_1}
{𝓨 : Type u_2}
{m𝓞 : MeasurableSpace 𝓞}
{m𝓨 : MeasurableSpace 𝓨}
(K : ℕ)
[NeZero K]
:
The Round-Robin algorithm: deterministic algorithm that chooses action n % K at time n.
Equations
- Learning.roundRobinAlgorithm K = Learning.detAlgorithm (fun (n : ℕ) (x : Learning.Hist 𝓞 (Fin K) 𝓨 n × 𝓞) => Learning.RoundRobin.nextAction K n) ⋯
Instances For
theorem
Learning.RoundRobin.action_ae_eq
{𝓨 : Type u_2}
{m𝓨 : MeasurableSpace 𝓨}
{K : ℕ}
[NeZero K]
{ν : ProbabilityTheory.Kernel (Fin K) 𝓨}
[ProbabilityTheory.IsMarkovKernel ν]
{Ω : Type u_3}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure P]
{O : ℕ → Ω → Unit}
{A : ℕ → Ω → Fin K}
{Y : ℕ → Ω → 𝓨}
(n : ℕ)
(h : IsAlgEnvSeqUntil O A Y (roundRobinAlgorithm K) (stationaryEnv ν) P (n + 1))
:
A n =ᵐ[P] fun (x : Ω) => nextAction K n
The action chosen at time n is the action n % K.
theorem
Learning.RoundRobin.action_zero
{𝓨 : Type u_2}
{m𝓨 : MeasurableSpace 𝓨}
{K : ℕ}
[NeZero K]
{ν : ProbabilityTheory.Kernel (Fin K) 𝓨}
[ProbabilityTheory.IsMarkovKernel ν]
{Ω : Type u_3}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure P]
{O : ℕ → Ω → Unit}
{A : ℕ → Ω → Fin K}
{Y : ℕ → Ω → 𝓨}
(h : IsAlgEnvSeqUntil O A Y (roundRobinAlgorithm K) (stationaryEnv ν) P 1)
:
A 0 =ᵐ[P] fun (x : Ω) => 0
theorem
Learning.RoundRobin.pullCount_mul
{𝓨 : Type u_2}
{m𝓨 : MeasurableSpace 𝓨}
{K : ℕ}
[NeZero K]
{ν : ProbabilityTheory.Kernel (Fin K) 𝓨}
[ProbabilityTheory.IsMarkovKernel ν]
{Ω : Type u_3}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure P]
{O : ℕ → Ω → Unit}
{A : ℕ → Ω → Fin K}
{Y : ℕ → Ω → 𝓨}
(m : ℕ)
(h : IsAlgEnvSeqUntil O A Y (roundRobinAlgorithm K) (stationaryEnv ν) P (K * m))
(a : Fin K)
:
At time K * m, the number of times each action is chosen is equal to m.
theorem
Learning.RoundRobin.pullCount_eq_one
{𝓨 : Type u_2}
{m𝓨 : MeasurableSpace 𝓨}
{K : ℕ}
[NeZero K]
{ν : ProbabilityTheory.Kernel (Fin K) 𝓨}
[ProbabilityTheory.IsMarkovKernel ν]
{Ω : Type u_3}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure P]
{O : ℕ → Ω → Unit}
{A : ℕ → Ω → Fin K}
{Y : ℕ → Ω → 𝓨}
(h : IsAlgEnvSeqUntil O A Y (roundRobinAlgorithm K) (stationaryEnv ν) P K)
(a : Fin K)
:
pullCount A a K =ᵐ[P] fun (x : Ω) => 1
theorem
Learning.RoundRobin.time_gt_of_pullCount_gt_one
{𝓨 : Type u_2}
{m𝓨 : MeasurableSpace 𝓨}
{K : ℕ}
[NeZero K]
{ν : ProbabilityTheory.Kernel (Fin K) 𝓨}
[ProbabilityTheory.IsMarkovKernel ν]
{Ω : Type u_3}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure P]
{O : ℕ → Ω → Unit}
{A : ℕ → Ω → Fin K}
{Y : ℕ → Ω → 𝓨}
(h : IsAlgEnvSeqUntil O A Y (roundRobinAlgorithm K) (stationaryEnv ν) P K)
(a : Fin K)
:
theorem
Learning.RoundRobin.pullCount_pos_of_time_ge
{𝓨 : Type u_2}
{m𝓨 : MeasurableSpace 𝓨}
{K : ℕ}
[NeZero K]
{ν : ProbabilityTheory.Kernel (Fin K) 𝓨}
[ProbabilityTheory.IsMarkovKernel ν]
{Ω : Type u_3}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure P]
{O : ℕ → Ω → Unit}
{A : ℕ → Ω → Fin K}
{Y : ℕ → Ω → 𝓨}
(h : IsAlgEnvSeqUntil O A Y (roundRobinAlgorithm K) (stationaryEnv ν) P K)
:
theorem
Learning.RoundRobin.pullCount_pos_of_pullCount_gt_one
{𝓨 : Type u_2}
{m𝓨 : MeasurableSpace 𝓨}
{K : ℕ}
[NeZero K]
{ν : ProbabilityTheory.Kernel (Fin K) 𝓨}
[ProbabilityTheory.IsMarkovKernel ν]
{Ω : Type u_3}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure P]
{O : ℕ → Ω → Unit}
{A : ℕ → Ω → Fin K}
{Y : ℕ → Ω → 𝓨}
(h : IsAlgEnvSeqUntil O A Y (roundRobinAlgorithm K) (stationaryEnv ν) P K)
(a : Fin K)
: