LeanMachineLearning exposition

Bandits.gap🔗

Minimal Lean file

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