LeanMachineLearning exposition

Learning.IsBayesAlgEnvSeq.regret_eq_sum_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

regret_eq_sum_gap๐Ÿ”—

LemmaLearning.IsBayesAlgEnvSeq.regret_eq_sum_gap
Details

No docstring.

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

Code

lemma regret_eq_sum_gap {ฮบ : Kernel (๐“” ร— ๐“) โ„} {E : ฮฉ โ†’ ๐“”} {A : โ„• โ†’ ฮฉ โ†’ ๐“} {n : โ„•} {ฯ‰ : ฮฉ} :
    regret ฮบ E A n ฯ‰ = โˆ‘ s โˆˆ range n, gap ฮบ E A s ฯ‰
Type uses (2)
Used by (2)

Actions: Source ยท Open Issue

Proof
by
  simp [regret, Bandits.regret, gap, Bandits.gap]

Dependency graph

Type dependencies (2)

regret๐Ÿ”—

DefinitionLearning.IsBayesAlgEnvSeq.regret
Details

A random variable that gives the regret at time n.

๐Ÿ”—def
Learning.IsBayesAlgEnvSeq.regret.{u_1, u_2, u_4} {๐“” : Type u_1}
  {๐“ : Type u_2} {ฮฉ : Type u_4} [MeasurableSpace ๐“”] [MeasurableSpace ๐“]
  (ฮบ : ProbabilityTheory.Kernel (๐“” ร— ๐“) โ„) (E : ฮฉ โ†’ ๐“”) (A : โ„• โ†’ ฮฉ โ†’ ๐“)
  (n : โ„•) (ฯ‰ : ฮฉ) : โ„
Learning.IsBayesAlgEnvSeq.regret.{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 regret (ฮบ : Kernel (๐“” ร— ๐“) โ„) (E : ฮฉ โ†’ ๐“”) (A : โ„• โ†’ ฮฉ โ†’ ๐“) (n : โ„•) (ฯ‰ : ฮฉ) : โ„ :=
  Bandits.regret (ฮบ.sectR (E ฯ‰)) A n ฯ‰
Body uses (1)
Used by (6)

Actions: Source ยท Open Issue

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 (2)

regret๐Ÿ”—

DefinitionBandits.regret
Details

Regret of a sequence of pulls k : โ„• โ†’ ๐“ at time t for the reward kernel ฮฝ ; Kernel ๐“ โ„.

๐Ÿ”—def
Bandits.regret.{u_1, u_2} {๐“ : Type u_1} {ฮฉ : Type u_2}
  {m๐“ : MeasurableSpace ๐“} (ฮฝ : ProbabilityTheory.Kernel ๐“ โ„)
  (A : โ„• โ†’ ฮฉ โ†’ ๐“) (t : โ„•) (ฯ‰ : ฮฉ) : โ„
Bandits.regret.{u_1, u_2} {๐“ : Type u_1}
  {ฮฉ : Type u_2} {m๐“ : MeasurableSpace ๐“}
  (ฮฝ : ProbabilityTheory.Kernel ๐“ โ„)
  (A : โ„• โ†’ ฮฉ โ†’ ๐“) (t : โ„•) (ฯ‰ : ฮฉ) : โ„

Code

noncomputable
def regret (ฮฝ : Kernel ๐“ โ„) (A : โ„• โ†’ ฮฉ โ†’ ๐“) (t : โ„•) (ฯ‰ : ฮฉ) : โ„ :=
  t * (โจ† a, (ฮฝ a)[id]) - โˆ‘ s โˆˆ range t, (ฮฝ (A s ฯ‰))[id]
Used by (11)

Actions: Source ยท Open Issue

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