LeanMachineLearning exposition

Bandits.ArrayModel.probSpace🔗

Minimal Lean file

probSpace🔗

DefinitionBandits.ArrayModel.probSpace
Details

Probability space for the array model of stochastic bandits.

🔗def
Bandits.ArrayModel.probSpace.{u_1, u_2} (𝓐 : Type u_1) (R : Type u_2) :
  Type (max u_1 u_2)
Bandits.ArrayModel.probSpace.{u_1, u_2}
  (𝓐 : Type u_1) (R : Type u_2) :
  Type (max u_1 u_2)

Code

def probSpace : Type _ := (ℕ → I) × (ℕ → 𝓐 → R)
Used by (64)

Actions: Source · Open Issue