LeanMachineLearning exposition

Bandits.UCB.ucbWidth_eq_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

ucbWidth_eq_ucbWidth'๐Ÿ”—

LemmaBandits.UCB.ucbWidth_eq_ucbWidth'
Details

No docstring.

๐Ÿ”—theorem
Bandits.UCB.ucbWidth_eq_ucbWidth'.{u_1} {K : โ„•} {ฮฉ : Type u_1}
  {A : โ„• โ†’ ฮฉ โ†’ Fin K} {R : โ„• โ†’ ฮฉ โ†’ โ„} (c : โ„) (a : Fin K) (n : โ„•)
  (ฯ‰ : ฮฉ) (hn : n โ‰  0) :
  ucbWidth A c a n ฯ‰ =
    ucbWidth' c (n - 1) (Learning.history A R (n - 1) ฯ‰) a
Bandits.UCB.ucbWidth_eq_ucbWidth'.{u_1}
  {K : โ„•} {ฮฉ : Type u_1}
  {A : โ„• โ†’ ฮฉ โ†’ Fin K} {R : โ„• โ†’ ฮฉ โ†’ โ„}
  (c : โ„) (a : Fin K) (n : โ„•) (ฯ‰ : ฮฉ)
  (hn : n โ‰  0) :
  ucbWidth A c a n ฯ‰ =
    ucbWidth' c (n - 1)
      (Learning.history A R (n - 1) ฯ‰) a

Code

lemma ucbWidth_eq_ucbWidth' (c : โ„) (a : Fin K) (n : โ„•) (ฯ‰ : ฮฉ) (hn : n โ‰  0) :
    ucbWidth A c a n ฯ‰ = ucbWidth' c (n - 1) (history A R (n - 1) ฯ‰) a
Type uses (3)
Body uses (3)
Used by (1)

Actions: Source ยท Open Issue

Proof
by
  simp only [ucbWidth, pullCount_eq_pullCount' (A := A) (R' := R) hn, Nat.cast_nonneg, sqrt_div',
    ucbWidth']
  congr 4
  norm_cast
  grind

Dependency graph

Type dependencies (3)

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

ucbWidth'๐Ÿ”—

DefinitionBandits.ucbWidth'
Details

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

๐Ÿ”—def
Bandits.ucbWidth' {K : โ„•} (c : โ„) (n : โ„•)
  (h : โ†ฅ(Finset.Iic n) โ†’ Fin K ร— โ„) (a : Fin K) : โ„
Bandits.ucbWidth' {K : โ„•} (c : โ„) (n : โ„•)
  (h : โ†ฅ(Finset.Iic n) โ†’ Fin K ร— โ„)
  (a : Fin K) : โ„

Code

noncomputable def ucbWidth' (c : โ„) (n : โ„•) (h : Iic n โ†’ Fin K ร— โ„) (a : Fin K) : โ„ :=
  โˆš(2 * c * log (n + 2) / pullCount' n h a)
Body uses (1)
Used by (6)

Actions: Source ยท Open Issue

history๐Ÿ”—

DefinitionLearning.history
Details

History of the algorithm-environment sequence up to time n.

๐Ÿ”—def
Learning.history.{u_1, u_2, u_3} {๐“ : Type u_1} {๐“จ : Type u_2}
  {ฮฉ : Type u_3} (A : โ„• โ†’ ฮฉ โ†’ ๐“) (Y : โ„• โ†’ ฮฉ โ†’ ๐“จ) (n : โ„•) (ฯ‰ : ฮฉ) :
  โ†ฅ(Finset.Iic n) โ†’ ๐“ ร— ๐“จ
Learning.history.{u_1, u_2, u_3}
  {๐“ : Type u_1} {๐“จ : Type u_2}
  {ฮฉ : Type u_3} (A : โ„• โ†’ ฮฉ โ†’ ๐“)
  (Y : โ„• โ†’ ฮฉ โ†’ ๐“จ) (n : โ„•) (ฯ‰ : ฮฉ) :
  โ†ฅ(Finset.Iic n) โ†’ ๐“ ร— ๐“จ

Code

def history (A : โ„• โ†’ ฮฉ โ†’ ๐“) (Y : โ„• โ†’ ฮฉ โ†’ ๐“จ) (n : โ„•) (ฯ‰ : ฮฉ) : Iic n โ†’ ๐“ ร— ๐“จ :=
  fun i โ†ฆ (A i ฯ‰, Y i ฯ‰)
Used by (72)

Actions: Source ยท Open Issue

All dependencies, transitively (2)

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

pullCount'๐Ÿ”—

DefinitionLearning.pullCount'
Details

Number of pulls of arm a up to (and including) time n. This is the number of entries in h in which the arm is a.

๐Ÿ”—def
Learning.pullCount'.{u_1, u_2} {๐“ : Type u_1} {R : Type u_2}
  [DecidableEq ๐“] (n : โ„•) (h : โ†ฅ(Finset.Iic n) โ†’ ๐“ ร— R) (a : ๐“) : โ„•
Learning.pullCount'.{u_1, u_2}
  {๐“ : Type u_1} {R : Type u_2}
  [DecidableEq ๐“] (n : โ„•)
  (h : โ†ฅ(Finset.Iic n) โ†’ ๐“ ร— R) (a : ๐“) :
  โ„•

Code

noncomputable
def pullCount' (n : โ„•) (h : Iic n โ†’ ๐“ ร— R) (a : ๐“) := #{s | (h s).1 = a}
Used by (29)

Actions: Source ยท Open Issue