`Learning.IsBayesAlgEnvSeq.gap_eq_sub`🔗

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

`gap_eq_sub`🔗

LemmaLearning.IsBayesAlgEnvSeq.gap_eq_sub

Details

No docstring.

theorem

Learning.IsBayesAlgEnvSeq.gap_eq_sub.{u_1, u_2, u_4} {𝓔 : Type u_1}
  {𝓐 : Type u_2} {Ω : Type u_4} [MeasurableSpace 𝓔] [MeasurableSpace 𝓐]
  [Nonempty 𝓐] [Fintype 𝓐] {κ : ProbabilityTheory.Kernel (𝓔 × 𝓐) ℝ}
  {E : Ω → 𝓔} {A : ℕ → Ω → 𝓐} {n : ℕ} {ω : Ω} :
  gap κ E A n ω =
    actionMean κ E (bestAction κ E ω) ω - actionMean κ E (A n ω) ω
Learning.IsBayesAlgEnvSeq.gap_eq_sub.{u_1,
    u_2, u_4}
  {𝓔 : Type u_1} {𝓐 : Type u_2}
  {Ω : Type u_4} [MeasurableSpace 𝓔]
  [MeasurableSpace 𝓐] [Nonempty 𝓐]
  [Fintype 𝓐]
  {κ : ProbabilityTheory.Kernel (𝓔 × 𝓐) ℝ}
  {E : Ω → 𝓔} {A : ℕ → Ω → 𝓐} {n : ℕ}
  {ω : Ω} :
  gap κ E A n ω =
    actionMean κ E (bestAction κ E ω) ω -
      actionMean κ E (A n ω) ω

Code

lemma gap_eq_sub [Nonempty 𝓐] [Fintype 𝓐] {κ : Kernel (𝓔 × 𝓐) ℝ} {E : Ω → 𝓔} {A : ℕ → Ω → 𝓐}
    {n : ℕ} {ω : Ω} : gap κ E A n ω =
      actionMean κ E (bestAction κ E ω) ω - actionMean κ E (A n ω) ω

Type uses (3)

Body uses (2)

Used by (1)

integral_regret_eq_add

Actions: Source · Open Issue

Proof

by
  rw [gap, Bandits.gap]
  congr
  apply le_antisymm
  · exact ciSup_le <| isMaxOn_argmax (fun a ↦ actionMean κ E a ω)
  · exact Finite.le_ciSup (fun a ↦ actionMean κ E a ω) _

Dependency graph

Type dependencies (3)

`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)

gap

Used by (10)

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

`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)

`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

`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)

max

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

Learning.IsBayesAlgEnvSeq.gap_eq_sub🔗

gap_eq_sub🔗

gap🔗

actionMean🔗

bestAction🔗

gap🔗

max🔗

exists_argmax🔗

argmax🔗

`Learning.IsBayesAlgEnvSeq.gap_eq_sub`🔗

`gap_eq_sub`🔗

`gap`🔗

`actionMean`🔗

`bestAction`🔗

`gap`🔗

`max`🔗

`exists_argmax`🔗

`argmax`🔗