LeanMachineLearning exposition

Learning.IsBayesAlgEnvSeq.measurable_gap๐Ÿ”—

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_gap๐Ÿ”—

LemmaLearning.IsBayesAlgEnvSeq.measurable_gap
Details

No docstring.

๐Ÿ”—theorem
Learning.IsBayesAlgEnvSeq.measurable_gap.{u_1, u_2, u_4} {๐“” : Type u_1}
  {๐“ : Type u_2} {ฮฉ : Type u_4} [MeasurableSpace ๐“”] [MeasurableSpace ๐“]
  [MeasurableSpace ฮฉ] [Countable ๐“]
  {ฮบ : ProbabilityTheory.Kernel (๐“” ร— ๐“) โ„} {E : ฮฉ โ†’ ๐“”} {A : โ„• โ†’ ฮฉ โ†’ ๐“}
  {n : โ„•} (hE : Measurable E) (hA : โˆ€ (t : โ„•), Measurable (A t)) :
  Measurable (gap ฮบ E A n)
Learning.IsBayesAlgEnvSeq.measurable_gap.{u_1,
    u_2, u_4}
  {๐“” : Type u_1} {๐“ : Type u_2}
  {ฮฉ : Type u_4} [MeasurableSpace ๐“”]
  [MeasurableSpace ๐“] [MeasurableSpace ฮฉ]
  [Countable ๐“]
  {ฮบ : ProbabilityTheory.Kernel (๐“” ร— ๐“) โ„}
  {E : ฮฉ โ†’ ๐“”} {A : โ„• โ†’ ฮฉ โ†’ ๐“} {n : โ„•}
  (hE : Measurable E)
  (hA : โˆ€ (t : โ„•), Measurable (A t)) :
  Measurable (gap ฮบ E A n)

Code

lemma measurable_gap [Countable ๐“] {ฮบ : Kernel (๐“” ร— ๐“) โ„} {E : ฮฉ โ†’ ๐“”} {A : โ„• โ†’ ฮฉ โ†’ ๐“} {n : โ„•}
    (hE : Measurable E) (hA : โˆ€ t, Measurable (A t)) : Measurable (gap ฮบ E A n)
Type uses (1)
Used by (2)

Actions: Source ยท Open Issue

Proof
(Measurable.iSup fun _ โ†ฆ stronglyMeasurable_id.integral_kernel.measurable.comp (by fun_prop)).sub
    (stronglyMeasurable_id.integral_kernel.measurable.comp (by fun_prop))

Dependency graph

Type dependencies (1)

gap๐Ÿ”—

DefinitionLearning.IsBayesAlgEnvSeq.gap
Details

A random variable that gives the gap at time n.

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

Code

noncomputable
def gap (ฮบ : Kernel (๐“” ร— ๐“) โ„) (E : ฮฉ โ†’ ๐“”) (A : โ„• โ†’ ฮฉ โ†’ ๐“) (n : โ„•) (ฯ‰ : ฮฉ) : โ„ :=
  Bandits.gap (ฮบ.sectR (E ฯ‰)) (A n ฯ‰)
Body uses (1)
Used by (10)

Actions: Source ยท Open Issue

All dependencies, transitively (1)

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