LeanMachineLearning exposition

Bandits.UCB.pullCount_arm_le🔗

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

pullCount_arm_le🔗

LemmaBandits.UCB.pullCount_arm_le
Details

No docstring.

🔗theorem
Bandits.UCB.pullCount_arm_le.{u_1} {K : ℕ} {c : ℝ}
  {ν : ProbabilityTheory.Kernel (Fin K) ℝ} {Ω : Type u_1}
  {A : ℕ → Ω → Fin K} {R : ℕ → Ω → ℝ} {n : ℕ} {ω : Ω} [Nonempty (Fin K)]
  (hc : 0 ≤ c)
  (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 ω)
  (h_gap_pos : 0 < gap ν (A n ω))
  (h_pull_pos : 0 < Learning.pullCount A (A n ω) n ω) :
  ↑(Learning.pullCount A (A n ω) n ω) ≤
    8 * c * Real.log (↑n + 1) / gap ν (A n ω) ^ 2
Bandits.UCB.pullCount_arm_le.{u_1} {K : ℕ}
  {c : ℝ}
  {ν : ProbabilityTheory.Kernel (Fin K) ℝ}
  {Ω : Type u_1} {A : ℕ → Ω → Fin K}
  {R : ℕ → Ω → ℝ} {n : ℕ} {ω : Ω}
  [Nonempty (Fin K)] (hc : 0 ≤ c)
  (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 ω)
  (h_gap_pos : 0 < gap ν (A n ω))
  (h_pull_pos :
    0 <
      Learning.pullCount A (A n ω) n ω) :
  ↑(Learning.pullCount A (A n ω) n ω) ≤
    8 * c * Real.log (↑n + 1) /
      gap ν (A n ω) ^ 2

Code

lemma pullCount_arm_le [Nonempty (Fin K)] (hc : 0 ≤ c)
    (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 ω)
    (h_gap_pos : 0 < gap ν (A n ω)) (h_pull_pos : 0 < pullCount A (A n ω) n ω) :
    pullCount A (A n ω) n ω ≤ 8 * c * log (n + 1) / gap ν (A n ω) ^ 2
Type uses (5)
Body uses (1)
Used by (1)

Actions: Source · Open Issue

Proof
by
  have h_gap_le := gap_arm_le_two_mul_ucbWidth h_best h_arm h_le
  rw [ucbWidth] at h_gap_le
  have h2 : (gap ν (A n ω)) ^ 2 ≤ (2 * √(2 * c * log (n + 1) / pullCount A (A n ω) n ω)) ^ 2 := by
    gcongr
  rw [mul_pow, sq_sqrt] at h2
  · have : (2 : ℝ) ^ 2 = 4 := by norm_num
    rw [this] at h2
    field_simp at h2 ⊢
    grind
  · have : 0 ≤ log (n + 1) := by simp [log_nonneg]
    positivity

Dependency graph

Type dependencies (5)

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)
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

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

All dependencies, transitively (1)

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