`Learning.IsBayesAlgEnvSeq.integrable_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

`integrable_gap`🔗

LemmaLearning.IsBayesAlgEnvSeq.integrable_gap

Details

No docstring.

theorem

Learning.IsBayesAlgEnvSeq.integrable_gap.{u_1, u_2, u_4} {𝓔 : Type u_1}
  {𝓐 : Type u_2} {Ω : Type u_4} [MeasurableSpace 𝓔] [MeasurableSpace 𝓐]
  [MeasurableSpace Ω] [Countable 𝓐] [Nonempty 𝓐]
  {κ : ProbabilityTheory.Kernel (𝓔 × 𝓐) ℝ} {E : Ω → 𝓔} {A : ℕ → Ω → 𝓐}
  {n : ℕ} {P : MeasureTheory.Measure Ω}
  [MeasureTheory.IsFiniteMeasure P] (hE : Measurable E)
  (hA : ∀ (t : ℕ), Measurable (A t)) {l u : ℝ}
  (h : ∀ (e : 𝓔) (a : 𝓐), ∫ (x : ℝ), id x ∂κ (e, a) ∈ Set.Icc l u) :
  MeasureTheory.Integrable (gap κ E A n) P
Learning.IsBayesAlgEnvSeq.integrable_gap.{u_1,
    u_2, u_4}
  {𝓔 : Type u_1} {𝓐 : Type u_2}
  {Ω : Type u_4} [MeasurableSpace 𝓔]
  [MeasurableSpace 𝓐] [MeasurableSpace Ω]
  [Countable 𝓐] [Nonempty 𝓐]
  {κ : ProbabilityTheory.Kernel (𝓔 × 𝓐) ℝ}
  {E : Ω → 𝓔} {A : ℕ → Ω → 𝓐} {n : ℕ}
  {P : MeasureTheory.Measure Ω}
  [MeasureTheory.IsFiniteMeasure P]
  (hE : Measurable E)
  (hA : ∀ (t : ℕ), Measurable (A t))
  {l u : ℝ}
  (h :
    ∀ (e : 𝓔) (a : 𝓐),
      ∫ (x : ℝ), id x ∂κ (e, a) ∈
        Set.Icc l u) :
  MeasureTheory.Integrable (gap κ E A n) P

Code

lemma integrable_gap [Countable 𝓐] [Nonempty 𝓐] {κ : Kernel (𝓔 × 𝓐) ℝ} {E : Ω → 𝓔}
    {A : ℕ → Ω → 𝓐} {n : ℕ} {P : Measure Ω} [IsFiniteMeasure P] (hE : Measurable E)
    (hA : ∀ t, Measurable (A t)) {l u : ℝ} (h : ∀ e a, (κ (e, a))[id] ∈ Set.Icc l u) :
    Integrable (gap κ E A n) P

Type uses (1)

gap

Body uses (3)

Used by (1)

integrable_regret

Actions: Source · Open Issue

Proof

by
  apply Integrable.of_bound (by fun_prop) (u - l)
  filter_upwards with ω
  rw [Real.norm_eq_abs, abs_of_nonneg (gap_nonneg_of_le (fun e a ↦ (h e a).2))]
  exact gap_le_of_mem_Icc h

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)

gap

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

Learning.IsBayesAlgEnvSeq.integrable_gap🔗

integrable_gap🔗

gap🔗

gap🔗

`Learning.IsBayesAlgEnvSeq.integrable_gap`🔗

`integrable_gap`🔗

`gap`🔗

`gap`🔗