`Bandits.UCB.gap_arm_le_two_mul_ucbWidth`🔗

This page has the declaration's own card below, then its dependency graph, then a card for each dependency (type dependencies first, then the rest of the transitive closure). For a theorem, the graph and the dependency cards only follow its statement's dependencies (its proof is replaced by sorry, so what it proves doesn't depend on how); for everything else, both the type and the body/value are followed, since their content is part of what later declarations build on.

Minimal Lean file

`gap_arm_le_two_mul_ucbWidth`🔗

LemmaBandits.UCB.gap_arm_le_two_mul_ucbWidth

Details

No docstring.

theorem

Bandits.UCB.gap_arm_le_two_mul_ucbWidth.{u_1} {K : ℕ} {c : ℝ}
  {ν : ProbabilityTheory.Kernel (Fin K) ℝ} {Ω : Type u_1}
  {A : ℕ → Ω → Fin K} {R : ℕ → Ω → ℝ} {n : ℕ} {ω : Ω} [Nonempty (Fin K)]
  (h_best :
    ∫ (x : ℝ), id x ∂ν (bestArm ν) ≤
      Learning.empMean A R (bestArm ν) n ω +
        ucbWidth A c (bestArm ν) n ω)
  (h_arm :
    Learning.empMean A R (A n ω) n ω - ucbWidth A c (A n ω) n ω ≤
      ∫ (x : ℝ), id x ∂ν (A n ω))
  (h_le :
    Learning.empMean A R (bestArm ν) n ω +
        ucbWidth A c (bestArm ν) n ω ≤
      Learning.empMean A R (A n ω) n ω + ucbWidth A c (A n ω) n ω) :
  gap ν (A n ω) ≤ 2 * ucbWidth A c (A n ω) n ω
Bandits.UCB.gap_arm_le_two_mul_ucbWidth.{u_1}
  {K : ℕ} {c : ℝ}
  {ν : ProbabilityTheory.Kernel (Fin K) ℝ}
  {Ω : Type u_1} {A : ℕ → Ω → Fin K}
  {R : ℕ → Ω → ℝ} {n : ℕ} {ω : Ω}
  [Nonempty (Fin K)]
  (h_best :
    ∫ (x : ℝ), id x ∂ν (bestArm ν) ≤
      Learning.empMean A R (bestArm ν) n
          ω +
        ucbWidth A c (bestArm ν) n ω)
  (h_arm :
    Learning.empMean A R (A n ω) n ω -
        ucbWidth A c (A n ω) n ω ≤
      ∫ (x : ℝ), id x ∂ν (A n ω))
  (h_le :
    Learning.empMean A R (bestArm ν) n ω +
        ucbWidth A c (bestArm ν) n ω ≤
      Learning.empMean A R (A n ω) n ω +
        ucbWidth A c (A n ω) n ω) :
  gap ν (A n ω) ≤
    2 * ucbWidth A c (A n ω) n ω

Code

lemma gap_arm_le_two_mul_ucbWidth [Nonempty (Fin K)]
    (h_best : (ν (bestArm ν))[id] ≤ empMean A R (bestArm ν) n ω + ucbWidth A c (bestArm ν) n ω)
    (h_arm : empMean A R (A n ω) n ω - ucbWidth A c (A n ω) n ω ≤ (ν (A n ω))[id])
    (h_le : empMean A R (bestArm ν) n ω + ucbWidth A c (bestArm ν) n ω ≤
      empMean A R (A n ω) n ω + ucbWidth A c (A n ω) n ω) :
    gap ν (A n ω) ≤ 2 * ucbWidth A c (A n ω) n ω

Type uses (4)

Body uses (1)

gap_eq_bestArm_sub

Used by (1)

pullCount_arm_le

Actions: Source · Open Issue

Proof

by
  rw [gap_eq_bestArm_sub, sub_le_iff_le_add']
  calc (ν (bestArm ν))[id]
  _ ≤ empMean A R (bestArm ν) n ω + ucbWidth A c (bestArm ν) n ω := h_best
  _ ≤ empMean A R (A n ω) n ω + ucbWidth A c (A n ω) n ω := h_le
  _ ≤ (ν (A n ω))[id] + 2 * ucbWidth A c (A n ω) n ω := by
    rw [two_mul, ← add_assoc]
    gcongr
    rwa [sub_le_iff_le_add] at h_arm

Dependency graph

Type dependencies (4)

`bestArm`🔗

DefinitionBandits.bestArm

Details

action with the highest mean.

def

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

Code

noncomputable def bestArm (ν : Kernel 𝓐 ℝ) : 𝓐 :=
  (exists_max_image univ (fun a ↦ (ν a)[id]) (univ_nonempty_iff.mpr inferInstance)).choose

Used by (18)

Actions: Source · Open Issue

`empMean`🔗

DefinitionLearning.empMean

Details

Empirical mean reward obtained when pulling action a up to time t (exclusive).

def

Learning.empMean.{u_1, u_3} {𝓐 : Type u_1} {Ω : Type u_3}
  [DecidableEq 𝓐] (A : ℕ → Ω → 𝓐) (R' : ℕ → Ω → ℝ) (a : 𝓐) (t : ℕ)
  (ω : Ω) : ℝ
Learning.empMean.{u_1, u_3} {𝓐 : Type u_1}
  {Ω : Type u_3} [DecidableEq 𝓐]
  (A : ℕ → Ω → 𝓐) (R' : ℕ → Ω → ℝ) (a : 𝓐)
  (t : ℕ) (ω : Ω) : ℝ

Code

noncomputable
def empMean (A : ℕ → Ω → 𝓐) (R' : ℕ → Ω → ℝ) (a : 𝓐) (t : ℕ) (ω : Ω) : ℝ :=
  sumRewards A R' a t ω / pullCount A a t ω

Body uses (2)

Used by (34)

Actions: Source · Open Issue

`ucbWidth`🔗

DefinitionBandits.UCB.ucbWidth

Details

The exploration bonus of the UCB algorithm, which corresponds to the width of a confidence interval.

def

Bandits.UCB.ucbWidth.{u_1} {K : ℕ} {Ω : Type u_1} (A : ℕ → Ω → Fin K)
  (c : ℝ) (a : Fin K) (n : ℕ) (ω : Ω) : ℝ
Bandits.UCB.ucbWidth.{u_1} {K : ℕ}
  {Ω : Type u_1} (A : ℕ → Ω → Fin K)
  (c : ℝ) (a : Fin K) (n : ℕ) (ω : Ω) : ℝ

Code

noncomputable def ucbWidth (A : ℕ → Ω → Fin K) (c : ℝ) (a : Fin K) (n : ℕ) (ω : Ω) : ℝ :=
  √(2 * c * log (n + 1) / pullCount A a n ω)

Body uses (1)

pullCount

Used by (16)

Actions: Source · Open Issue

`gap`🔗

DefinitionBandits.gap

Details

Gap of an action a: difference between the highest mean of the actions and the mean of a.

def

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

Code

noncomputable
def gap (ν : Kernel 𝓐 ℝ) (a : 𝓐) : ℝ := (⨆ i, (ν i)[id]) - (ν a)[id]

Used by (27)

Actions: Source · Open Issue

All dependencies, transitively (2)

`sumRewards`🔗

DefinitionLearning.sumRewards

Details

Sum of rewards obtained when pulling action a up to time t (exclusive).

def

Learning.sumRewards.{u_1, u_3} {𝓐 : Type u_1} {Ω : Type u_3}
  [DecidableEq 𝓐] (A : ℕ → Ω → 𝓐) (R' : ℕ → Ω → ℝ) (a : 𝓐) (t : ℕ)
  (ω : Ω) : ℝ
Learning.sumRewards.{u_1, u_3}
  {𝓐 : Type u_1} {Ω : Type u_3}
  [DecidableEq 𝓐] (A : ℕ → Ω → 𝓐)
  (R' : ℕ → Ω → ℝ) (a : 𝓐) (t : ℕ)
  (ω : Ω) : ℝ

Code

def sumRewards (A : ℕ → Ω → 𝓐) (R' : ℕ → Ω → ℝ) (a : 𝓐) (t : ℕ) (ω : Ω) : ℝ :=
  ∑ s ∈ range t, if A s ω = a then R' s ω else 0

Used by (44)

Actions: Source · Open Issue

`pullCount`🔗

DefinitionLearning.pullCount

Details

Number of times action a was chosen up to time t (excluding t).

def

Learning.pullCount.{u_1, u_3} {𝓐 : Type u_1} {Ω : Type u_3}
  [DecidableEq 𝓐] (A : ℕ → Ω → 𝓐) (a : 𝓐) (t : ℕ) (ω : Ω) : ℕ
Learning.pullCount.{u_1, u_3}
  {𝓐 : Type u_1} {Ω : Type u_3}
  [DecidableEq 𝓐] (A : ℕ → Ω → 𝓐) (a : 𝓐)
  (t : ℕ) (ω : Ω) : ℕ

Code

noncomputable
def pullCount (A : ℕ → Ω → 𝓐) (a : 𝓐) (t : ℕ) (ω : Ω) : ℕ :=
  #(filter (fun s ↦ A s ω = a) (range t))

Used by (146)

Actions: Source · Open Issue

Bandits.UCB.gap_arm_le_two_mul_ucbWidth🔗

gap_arm_le_two_mul_ucbWidth🔗

bestArm🔗

empMean🔗

ucbWidth🔗

gap🔗

sumRewards🔗

pullCount🔗

`Bandits.UCB.gap_arm_le_two_mul_ucbWidth`🔗

`gap_arm_le_two_mul_ucbWidth`🔗

`bestArm`🔗

`empMean`🔗

`ucbWidth`🔗

`gap`🔗

`sumRewards`🔗

`pullCount`🔗