Bandits.le_bestArm🔗

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

Bandits.le_bestArm.{u_1} {𝓐 : Type u_1} {m𝓐 : MeasurableSpace 𝓐}
  {ν : ProbabilityTheory.Kernel 𝓐 ℝ} [Fintype 𝓐] [Nonempty 𝓐] (a : 𝓐) :
  ∫ (x : ℝ), id x ∂ν a ≤ ∫ (x : ℝ), id x ∂ν (bestArm ν)
Bandits.le_bestArm.{u_1} {𝓐 : Type u_1}
  {m𝓐 : MeasurableSpace 𝓐}
  {ν : ProbabilityTheory.Kernel 𝓐 ℝ}
  [Fintype 𝓐] [Nonempty 𝓐] (a : 𝓐) :
  ∫ (x : ℝ), id x ∂ν a ≤
    ∫ (x : ℝ), id x ∂ν (bestArm ν)

lemma le_bestArm (a : 𝓐) : (ν a)[id] ≤ (ν (bestArm ν))[id]

(exists_max_image univ (fun a ↦ (ν a)[id])
    (univ_nonempty_iff.mpr inferInstance)).choose_spec.2 _ (mem_univ a)

Dependency graph

Type dependencies (1)

Bandits.bestArm.{u_1} {𝓐 : Type u_1} {m𝓐 : MeasurableSpace 𝓐}
  [Fintype 𝓐] [Nonempty 𝓐] (ν : ProbabilityTheory.Kernel 𝓐 ℝ) : 𝓐
Bandits.bestArm.{u_1} {𝓐 : Type u_1}
  {m𝓐 : MeasurableSpace 𝓐} [Fintype 𝓐]
  [Nonempty 𝓐]
  (ν : ProbabilityTheory.Kernel 𝓐 ℝ) : 𝓐

noncomputable def bestArm (ν : Kernel 𝓐 ℝ) : 𝓐 :=
  (exists_max_image univ (fun a ↦ (ν a)[id]) (univ_nonempty_iff.mpr inferInstance)).choose