LeanMachineLearning exposition

Bandits.ClippedUCB.ucb๐Ÿ”—

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

ucb๐Ÿ”—

DefinitionBandits.ClippedUCB.ucb
Details

Clipped upper confidence bound used in the regret analysis of Thompson sampling.

๐Ÿ”—def
Bandits.ClippedUCB.ucb.{u_1} {K : โ„•} {ฮฉ : Type u_1} (A : โ„• โ†’ ฮฉ โ†’ Fin K)
  (R : โ„• โ†’ ฮฉ โ†’ โ„) (l u ฯƒ2 ฮด : โ„) (a : Fin K) (n : โ„•) (ฯ‰ : ฮฉ) : โ„
Bandits.ClippedUCB.ucb.{u_1} {K : โ„•}
  {ฮฉ : Type u_1} (A : โ„• โ†’ ฮฉ โ†’ Fin K)
  (R : โ„• โ†’ ฮฉ โ†’ โ„) (l u ฯƒ2 ฮด : โ„)
  (a : Fin K) (n : โ„•) (ฯ‰ : ฮฉ) : โ„

Code

noncomputable
def ucb (A : โ„• โ†’ ฮฉ โ†’ Fin K) (R : โ„• โ†’ ฮฉ โ†’ โ„) (l u ฯƒ2 ฮด : โ„) (a : Fin K) (n : โ„•) (ฯ‰ : ฮฉ) : โ„ :=
  if pullCount A a n ฯ‰ = 0 then u
  else max l (min u (empMean A R a n ฯ‰ + โˆš(2 * ฯƒ2 * Real.log (1 / ฮด) / (pullCount A a n ฯ‰))))
Body uses (2)
Used by (12)

Actions: Source ยท Open Issue

Dependency graph

All dependencies, transitively (3)

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

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

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