`Learning.IsBayesAlgEnvSeq.measurable_regret`🔗

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_regret`🔗

LemmaLearning.IsBayesAlgEnvSeq.measurable_regret

Details

No docstring.

theorem

Learning.IsBayesAlgEnvSeq.measurable_regret.{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 (regret κ E A n)
Learning.IsBayesAlgEnvSeq.measurable_regret.{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 (regret κ E A n)

Code

lemma measurable_regret [Countable 𝓐] {κ : Kernel (𝓔 × 𝓐) ℝ} {E : Ω → 𝓔} {A : ℕ → Ω → 𝓐} {n : ℕ}
    (hE : Measurable E) (hA : ∀ t, Measurable (A t)) : Measurable (regret κ E A n)

Type uses (1)

regret

Body uses (3)

Actions: Source · Open Issue

Proof

by
  rw [regret_eq_sum_gap']
  fun_prop

Dependency graph

Type dependencies (1)

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

regret

Used by (6)

Actions: Source · Open Issue

All dependencies, transitively (1)

`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

Learning.IsBayesAlgEnvSeq.measurable_regret🔗

measurable_regret🔗

regret🔗

regret🔗

`Learning.IsBayesAlgEnvSeq.measurable_regret`🔗

`measurable_regret`🔗

`regret`🔗

`regret`🔗