LeanMachineLearning exposition

Learning.pullCount'🔗

Minimal Lean file

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