Regret

Definitions of regret, gaps, pull counts

noncomputable def Bandits.regret {α : Type u_1} {mα : MeasurableSpace α} (ν : ProbabilityTheory.Kernel α ℝ) (k : ℕ → α) (t : ℕ) : ℝ

Regret of a sequence of pulls k : ℕ → α at time t for the reward kernel ν ; Kernel α ℝ.

Equations

• Bandits.regret ν k t = (↑t * ⨆ (a : α), ∫ (x : ℝ), id x ∂ν a) - ∑ s ∈ Finset.range t, ∫ (x : ℝ), id x ∂ν (k s)

noncomputable def Bandits.gap {α : Type u_1} {mα : MeasurableSpace α} (ν : ProbabilityTheory.Kernel α ℝ) (a : α) : ℝ

Gap of an arm a: difference between the highest mean of the arms and the mean of a.

Equations

• Bandits.gap ν a = (⨆ (i : α), ∫ (x : ℝ), id x ∂ν i) - ∫ (x : ℝ), id x ∂ν a

theorem Bandits.gap_nonneg {α : Type u_1} {mα : MeasurableSpace α} {ν : ProbabilityTheory.Kernel α ℝ} {a : α} [Fintype α] : 0 ≤ gap ν a

noncomputable def Bandits.pullCount {α : Type u_1} (k : ℕ → α) (a : α) (t : ℕ) : ℕ

Number of times arm a was pulled up to time t.

Equations

• Bandits.pullCount k a t = {s ∈ Finset.range t | k s = a}.card

theorem Bandits.sum_pullCount_mul {α : Type u_1} [Fintype α] (k : ℕ → α) (f : α → ℝ) (t : ℕ) : ∑ a : α, ↑(pullCount k a t) * f a = ∑ s ∈ Finset.range t, f (k s)

theorem Bandits.sum_pullCount {α : Type u_1} {k : ℕ → α} {t : ℕ} [Fintype α] : ∑ a : α, pullCount k a t = t

theorem Bandits.regret_eq_sum_pullCount_mul_gap {α : Type u_1} {mα : MeasurableSpace α} {ν : ProbabilityTheory.Kernel α ℝ} {k : ℕ → α} {t : ℕ} [Fintype α] : regret ν k t = ∑ a : α, ↑(pullCount k a t) * gap ν a

noncomputable def Bandits.bestArm {α : Type u_1} {mα : MeasurableSpace α} [Fintype α] [Nonempty α] (ν : ProbabilityTheory.Kernel α ℝ) : α

Arm with the highest mean.

Equations

• Bandits.bestArm ν = ⋯.choose

theorem Bandits.le_bestArm {α : Type u_1} {mα : MeasurableSpace α} {ν : ProbabilityTheory.Kernel α ℝ} [Fintype α] [Nonempty α] (a : α) : ∫ (x : ℝ), id x ∂ν a ≤ ∫ (x : ℝ), id x ∂ν (bestArm ν)

theorem Bandits.gap_eq_bestArm_sub {α : Type u_1} {mα : MeasurableSpace α} {ν : ProbabilityTheory.Kernel α ℝ} {a : α} [Fintype α] [Nonempty α] : gap ν a = ∫ (x : ℝ), id x ∂ν (bestArm ν) - ∫ (x : ℝ), id x ∂ν a