LeanMachineLearning exposition

Learning.IsBayesAlgEnvSeq.measurable_bestAction๐Ÿ”—

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

measurable_bestAction๐Ÿ”—

LemmaLearning.IsBayesAlgEnvSeq.measurable_bestAction
Details

No docstring.

๐Ÿ”—theorem
Learning.IsBayesAlgEnvSeq.measurable_bestAction.{u_1, u_2, u_4}
  {๐“” : Type u_1} {๐“ : Type u_2} {ฮฉ : Type u_4} [MeasurableSpace ๐“”]
  [MeasurableSpace ๐“] [MeasurableSpace ฮฉ] [Nonempty ๐“] [Fintype ๐“]
  {ฮบ : ProbabilityTheory.Kernel (๐“” ร— ๐“) โ„} {E : ฮฉ โ†’ ๐“”}
  (hE : Measurable E) : Measurable (bestAction ฮบ E)
Learning.IsBayesAlgEnvSeq.measurable_bestAction.{u_1,
    u_2, u_4}
  {๐“” : Type u_1} {๐“ : Type u_2}
  {ฮฉ : Type u_4} [MeasurableSpace ๐“”]
  [MeasurableSpace ๐“] [MeasurableSpace ฮฉ]
  [Nonempty ๐“] [Fintype ๐“]
  {ฮบ : ProbabilityTheory.Kernel (๐“” ร— ๐“) โ„}
  {E : ฮฉ โ†’ ๐“”} (hE : Measurable E) :
  Measurable (bestAction ฮบ E)

Code

lemma measurable_bestAction [Nonempty ๐“] [Fintype ๐“] {ฮบ : Kernel (๐“” ร— ๐“) โ„} {E : ฮฉ โ†’ ๐“”}
    (hE : Measurable E) : Measurable (bestAction ฮบ E)
Type uses (1)
Body uses (4)
Used by (7)

Actions: Source ยท Open Issue

Proof
by
  unfold bestAction
  fun_prop

Dependency graph

Type dependencies (1)

bestAction๐Ÿ”—

DefinitionLearning.IsBayesAlgEnvSeq.bestAction
Details

A random variable that gives the action with the highest mean feedback.

๐Ÿ”—def
Learning.IsBayesAlgEnvSeq.bestAction.{u_1, u_2, u_4} {๐“” : Type u_1}
  {๐“ : Type u_2} {ฮฉ : Type u_4} [MeasurableSpace ๐“”] [MeasurableSpace ๐“]
  [Nonempty ๐“] [Fintype ๐“] (ฮบ : ProbabilityTheory.Kernel (๐“” ร— ๐“) โ„)
  (E : ฮฉ โ†’ ๐“”) (ฯ‰ : ฮฉ) : ๐“
Learning.IsBayesAlgEnvSeq.bestAction.{u_1,
    u_2, u_4}
  {๐“” : Type u_1} {๐“ : Type u_2}
  {ฮฉ : Type u_4} [MeasurableSpace ๐“”]
  [MeasurableSpace ๐“] [Nonempty ๐“]
  [Fintype ๐“]
  (ฮบ : ProbabilityTheory.Kernel (๐“” ร— ๐“) โ„)
  (E : ฮฉ โ†’ ๐“”) (ฯ‰ : ฮฉ) : ๐“

Code

noncomputable
def bestAction [Nonempty ๐“] [Fintype ๐“] (ฮบ : Kernel (๐“” ร— ๐“) โ„) (E : ฮฉ โ†’ ๐“”) (ฯ‰ : ฮฉ) : ๐“ :=
  argmax (fun a โ†ฆ actionMean ฮบ E a ฯ‰)
Body uses (2)
Used by (12)

Actions: Source ยท Open Issue

All dependencies, transitively (4)

max๐Ÿ”—

DefinitionFunction.max
Details

The maximum value of a tuple.

๐Ÿ”—def
Function.max.{u_1, u_2} {ฮน : Type u_1} {ฮฑ : Type u_2} [LinearOrder ฮฑ]
  [Fintype ฮน] [Nonempty ฮน] (f : ฮน โ†’ ฮฑ) : ฮฑ
Function.max.{u_1, u_2} {ฮน : Type u_1}
  {ฮฑ : Type u_2} [LinearOrder ฮฑ]
  [Fintype ฮน] [Nonempty ฮน] (f : ฮน โ†’ ฮฑ) : ฮฑ

Code

abbrev max : ฮฑ := univ.sup' univ_nonempty f
Used by (8)

Actions: Source ยท Open Issue

exists_argmax๐Ÿ”—

Lemmaexists_argmax
Details

No docstring.

๐Ÿ”—theorem
exists_argmax.{u_1, u_2} {ฮน : Type u_1} {ฮฑ : Type u_2} [LinearOrder ฮฑ]
  [Fintype ฮน] [Nonempty ฮน] (f : ฮน โ†’ ฮฑ) : โˆƒ i, f i = Function.max f
exists_argmax.{u_1, u_2} {ฮน : Type u_1}
  {ฮฑ : Type u_2} [LinearOrder ฮฑ]
  [Fintype ฮน] [Nonempty ฮน] (f : ฮน โ†’ ฮฑ) :
  โˆƒ i, f i = Function.max f

Code

lemma exists_argmax : โˆƒ i, f i = f.max
Type uses (1)
Used by (3)

Actions: Source ยท Open Issue

Proof
by
  obtain โŸจi, -, hiโŸฉ := Finset.exists_mem_eq_sup' (by simp : Finset.univ.Nonempty) f
  exact โŸจi, hi.symmโŸฉ

argmax๐Ÿ”—

Definitionargmax
Details

The index of the maximum value of a tuple.

๐Ÿ”—def
argmax.{u_1, u_2} {ฮน : Type u_1} {ฮฑ : Type u_2} [LinearOrder ฮฑ]
  [Fintype ฮน] [Nonempty ฮน] (f : ฮน โ†’ ฮฑ) : ฮน
argmax.{u_1, u_2} {ฮน : Type u_1}
  {ฮฑ : Type u_2} [LinearOrder ฮฑ]
  [Fintype ฮน] [Nonempty ฮน] (f : ฮน โ†’ ฮฑ) : ฮน

Code

noncomputable def argmax := (exists_argmax f).choose
Body uses (2)
Used by (17)

Actions: Source ยท Open Issue

actionMean๐Ÿ”—

DefinitionLearning.IsBayesAlgEnvSeq.actionMean
Details

A random variable that gives the mean feedback of action a.

๐Ÿ”—def
Learning.IsBayesAlgEnvSeq.actionMean.{u_1, u_2, u_4} {๐“” : Type u_1}
  {๐“ : Type u_2} {ฮฉ : Type u_4} [MeasurableSpace ๐“”] [MeasurableSpace ๐“]
  (ฮบ : ProbabilityTheory.Kernel (๐“” ร— ๐“) โ„) (E : ฮฉ โ†’ ๐“”) (a : ๐“) (ฯ‰ : ฮฉ) :
  โ„
Learning.IsBayesAlgEnvSeq.actionMean.{u_1,
    u_2, u_4}
  {๐“” : Type u_1} {๐“ : Type u_2}
  {ฮฉ : Type u_4} [MeasurableSpace ๐“”]
  [MeasurableSpace ๐“]
  (ฮบ : ProbabilityTheory.Kernel (๐“” ร— ๐“) โ„)
  (E : ฮฉ โ†’ ๐“”) (a : ๐“) (ฯ‰ : ฮฉ) : โ„

Code

noncomputable
def actionMean (ฮบ : Kernel (๐“” ร— ๐“) โ„) (E : ฮฉ โ†’ ๐“”) (a : ๐“) (ฯ‰ : ฮฉ) : โ„ := (ฮบ (E ฯ‰, a))[id]
Used by (12)

Actions: Source ยท Open Issue