2.4. Online.Bandit.BayesRegret🔗

Bayesian regret

This file defines actionMean, bestAction, gap, and regret as random variables in a measurable space Ω. These definitions are useful when IsBayesAlgEnvSeq Q κ alg E A Y P.

Recall that IsBayesAlgEnvSeq Q κ alg E A Y P states that there is a measure P : Measure Ω such that the parameter E : Ω → 𝓔 has law Q and that the sequences of actions A : ℕ → Ω → 𝓐 and feedbacks Y : ℕ → Ω → 𝓨 are generated by the algorithm alg : Algorithm 𝓐 𝓨 interacting with an underlying environment that depends on E and κ (stationaryEnv (κ.sectR (E ω)))

Main definitions

actionMean κ E a: the mean feedback associated with action a : 𝓐 based on the parameter E, which defines the underlying stationary environment together with the kernel κ.
bestAction κ E: (one of) the action(s) with the highest associated mean feedback based on E.
gap κ E A n: the difference between the highest mean feedback associated with an action and the mean feedback associated with the action at time n based on E and the sequence of actions A.
regret κ E A n: the regret at time n based on E and the sequence of actions A. If IsBayesAlgEnvSeq Q κ alg E A Y P, then P[regret κ E A n] is the so-called Bayesian regret of algorithm alg under the prior Q.

Module LeanMachineLearning.Online.Bandit.BayesRegret contains 17 exposed declarations.

`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

`measurable_actionMean`🔗

LemmaLearning.IsBayesAlgEnvSeq.measurable_actionMean

Details

No docstring.

theorem

Learning.IsBayesAlgEnvSeq.measurable_actionMean.{u_1, u_2, u_4}
  {𝓔 : Type u_1} {𝓐 : Type u_2} {Ω : Type u_4} [MeasurableSpace 𝓔]
  [MeasurableSpace 𝓐] [MeasurableSpace Ω]
  {κ : ProbabilityTheory.Kernel (𝓔 × 𝓐) ℝ} {E : Ω → 𝓔} {a : 𝓐}
  (hE : Measurable E) : Measurable (actionMean κ E a)
Learning.IsBayesAlgEnvSeq.measurable_actionMean.{u_1,
    u_2, u_4}
  {𝓔 : Type u_1} {𝓐 : Type u_2}
  {Ω : Type u_4} [MeasurableSpace 𝓔]
  [MeasurableSpace 𝓐] [MeasurableSpace Ω]
  {κ : ProbabilityTheory.Kernel (𝓔 × 𝓐) ℝ}
  {E : Ω → 𝓔} {a : 𝓐}
  (hE : Measurable E) :
  Measurable (actionMean κ E a)

Code

lemma measurable_actionMean {κ : Kernel (𝓔 × 𝓐) ℝ} {E : Ω → 𝓔} {a : 𝓐} (hE : Measurable E) :
    Measurable (actionMean κ E a)

Type uses (1)

actionMean

Used by (4)

Actions: Source · Open Issue

Proof

stronglyMeasurable_id.integral_kernel.measurable.comp (by fun_prop)

`measurable_uncurry_actionMean_comp`🔗

LemmaLearning.IsBayesAlgEnvSeq.measurable_uncurry_actionMean_comp

Details

No docstring.

theorem

Learning.IsBayesAlgEnvSeq.measurable_uncurry_actionMean_comp.{u_1, u_2,
    u_4}
  {𝓔 : Type u_1} {𝓐 : Type u_2} {Ω : Type u_4} [MeasurableSpace 𝓔]
  [MeasurableSpace 𝓐] [MeasurableSpace Ω] [Countable 𝓐]
  [MeasurableSingletonClass 𝓐] {κ : ProbabilityTheory.Kernel (𝓔 × 𝓐) ℝ}
  {E : Ω → 𝓔} (hE : Measurable E) {f : Ω → 𝓐} (hf : Measurable f) :
  Measurable fun ω => actionMean κ E (f ω) ω
Learning.IsBayesAlgEnvSeq.measurable_uncurry_actionMean_comp.{u_1,
    u_2, u_4}
  {𝓔 : Type u_1} {𝓐 : Type u_2}
  {Ω : Type u_4} [MeasurableSpace 𝓔]
  [MeasurableSpace 𝓐] [MeasurableSpace Ω]
  [Countable 𝓐]
  [MeasurableSingletonClass 𝓐]
  {κ : ProbabilityTheory.Kernel (𝓔 × 𝓐) ℝ}
  {E : Ω → 𝓔} (hE : Measurable E)
  {f : Ω → 𝓐} (hf : Measurable f) :
  Measurable fun ω =>
    actionMean κ E (f ω) ω

Code

lemma measurable_uncurry_actionMean_comp [Countable 𝓐] [MeasurableSingletonClass 𝓐]
    {κ : Kernel (𝓔 × 𝓐) ℝ} {E : Ω → 𝓔} (hE : Measurable E) {f : Ω → 𝓐} (hf : Measurable f) :
    Measurable (fun ω ↦ actionMean κ E (f ω) ω)

Type uses (1)

actionMean

Body uses (1)

measurable_actionMean

Used by (3)

Actions: Source · Open Issue

Proof

by
  change Measurable ((fun aω ↦ actionMean κ E aω.1 aω.2) ∘ fun ω ↦ (f ω, ω))
  apply Measurable.comp _ (by fun_prop)
  exact measurable_from_prod_countable_right (fun _ ↦ measurable_actionMean hE)

`integrable_uncurry_actionMean_comp`🔗

LemmaLearning.IsBayesAlgEnvSeq.integrable_uncurry_actionMean_comp

Details

No docstring.

theorem

Learning.IsBayesAlgEnvSeq.integrable_uncurry_actionMean_comp.{u_1, u_2,
    u_4}
  {𝓔 : Type u_1} {𝓐 : Type u_2} {Ω : Type u_4} [MeasurableSpace 𝓔]
  [MeasurableSpace 𝓐] [MeasurableSpace Ω] [Countable 𝓐]
  [MeasurableSingletonClass 𝓐] {κ : ProbabilityTheory.Kernel (𝓔 × 𝓐) ℝ}
  {E : Ω → 𝓔} (hE : Measurable E) {f : Ω → 𝓐} (hf : Measurable f)
  {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P]
  {l u : ℝ}
  (hm : ∀ (e : 𝓔) (a : 𝓐), ∫ (x : ℝ), id x ∂κ (e, a) ∈ Set.Icc l u) :
  MeasureTheory.Integrable (fun ω => actionMean κ E (f ω) ω) P
Learning.IsBayesAlgEnvSeq.integrable_uncurry_actionMean_comp.{u_1,
    u_2, u_4}
  {𝓔 : Type u_1} {𝓐 : Type u_2}
  {Ω : Type u_4} [MeasurableSpace 𝓔]
  [MeasurableSpace 𝓐] [MeasurableSpace Ω]
  [Countable 𝓐]
  [MeasurableSingletonClass 𝓐]
  {κ : ProbabilityTheory.Kernel (𝓔 × 𝓐) ℝ}
  {E : Ω → 𝓔} (hE : Measurable E)
  {f : Ω → 𝓐} (hf : Measurable f)
  {P : MeasureTheory.Measure Ω}
  [MeasureTheory.IsFiniteMeasure P]
  {l u : ℝ}
  (hm :
    ∀ (e : 𝓔) (a : 𝓐),
      ∫ (x : ℝ), id x ∂κ (e, a) ∈
        Set.Icc l u) :
  MeasureTheory.Integrable
    (fun ω => actionMean κ E (f ω) ω) P

Code

lemma integrable_uncurry_actionMean_comp [Countable 𝓐] [MeasurableSingletonClass 𝓐]
    {κ : Kernel (𝓔 × 𝓐) ℝ} {E : Ω → 𝓔} (hE : Measurable E) {f : Ω → 𝓐} (hf : Measurable f)
    {P : Measure Ω} [IsFiniteMeasure P] {l u : ℝ} (hm : ∀ e a, (κ (e, a))[id] ∈ (Set.Icc l u)) :
    Integrable (fun ω ↦ actionMean κ E (f ω) ω) P

Type uses (1)

actionMean

Body uses (1)

measurable_uncurry_actionMean_comp

Used by (3)

Actions: Source · Open Issue

Proof

by
  refine ⟨(measurable_uncurry_actionMean_comp hE hf).aestronglyMeasurable, ?_⟩
  apply HasFiniteIntegral.of_bounded
  filter_upwards with ω using abs_le_max_abs_abs (hm (E ω) (f ω)).1 (hm (E ω) (f ω)).2

`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

`measurable_bestAction`🔗

LemmaLearning.IsBayesAlgEnvSeq.measurable_bestAction

Details

No docstring.

theorem

Learning.IsBayesAlgEnvSeq.measurable_bestAction.{u_1, u_2, u_4}
  {𝓔 : Type u_1} {𝓐 : Type u_2} {Ω : Type u_4} [MeasurableSpace 𝓔]
  [MeasurableSpace 𝓐] [MeasurableSpace Ω] [Nonempty 𝓐] [Fintype 𝓐]
  {κ : ProbabilityTheory.Kernel (𝓔 × 𝓐) ℝ} {E : Ω → 𝓔}
  (hE : Measurable E) : Measurable (bestAction κ E)
Learning.IsBayesAlgEnvSeq.measurable_bestAction.{u_1,
    u_2, u_4}
  {𝓔 : Type u_1} {𝓐 : Type u_2}
  {Ω : Type u_4} [MeasurableSpace 𝓔]
  [MeasurableSpace 𝓐] [MeasurableSpace Ω]
  [Nonempty 𝓐] [Fintype 𝓐]
  {κ : ProbabilityTheory.Kernel (𝓔 × 𝓐) ℝ}
  {E : Ω → 𝓔} (hE : Measurable E) :
  Measurable (bestAction κ E)

Code

lemma measurable_bestAction [Nonempty 𝓐] [Fintype 𝓐] {κ : Kernel (𝓔 × 𝓐) ℝ} {E : Ω → 𝓔}
    (hE : Measurable E) : Measurable (bestAction κ E)

Type uses (1)

bestAction

Body uses (4)

Used by (7)

Actions: Source · Open Issue

Proof

by
  unfold bestAction
  fun_prop

`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

`gap_nonneg_of_le`🔗

LemmaLearning.IsBayesAlgEnvSeq.gap_nonneg_of_le

Details

The gap is non-negative if the means are bounded by u : ℝ (even if 𝓐 is not Finite).

theorem

Learning.IsBayesAlgEnvSeq.gap_nonneg_of_le.{u_1, u_2, u_4}
  {𝓔 : Type u_1} {𝓐 : Type u_2} {Ω : Type u_4} [MeasurableSpace 𝓔]
  [MeasurableSpace 𝓐] {κ : ProbabilityTheory.Kernel (𝓔 × 𝓐) ℝ}
  {E : Ω → 𝓔} {A : ℕ → Ω → 𝓐} {n : ℕ} {ω : Ω} {u : ℝ}
  (h : ∀ (e : 𝓔) (a : 𝓐), ∫ (x : ℝ), id x ∂κ (e, a) ≤ u) :
  0 ≤ gap κ E A n ω
Learning.IsBayesAlgEnvSeq.gap_nonneg_of_le.{u_1,
    u_2, u_4}
  {𝓔 : Type u_1} {𝓐 : Type u_2}
  {Ω : Type u_4} [MeasurableSpace 𝓔]
  [MeasurableSpace 𝓐]
  {κ : ProbabilityTheory.Kernel (𝓔 × 𝓐) ℝ}
  {E : Ω → 𝓔} {A : ℕ → Ω → 𝓐} {n : ℕ}
  {ω : Ω} {u : ℝ}
  (h :
    ∀ (e : 𝓔) (a : 𝓐),
      ∫ (x : ℝ), id x ∂κ (e, a) ≤ u) :
  0 ≤ gap κ E A n ω

Code

lemma gap_nonneg_of_le {κ : Kernel (𝓔 × 𝓐) ℝ} {E : Ω → 𝓔} {A : ℕ → Ω → 𝓐} {n : ℕ} {ω : Ω} {u : ℝ}
    (h : ∀ e a, (κ (e, a))[id] ≤ u) : 0 ≤ gap κ E A n ω

Type uses (1)

gap

Body uses (1)

gap_nonneg_of_le

Used by (1)

integrable_gap

Actions: Source · Open Issue

Proof

Bandits.gap_nonneg_of_le (h (E ω))

`gap_le_of_mem_Icc`🔗

LemmaLearning.IsBayesAlgEnvSeq.gap_le_of_mem_Icc

Details

No docstring.

theorem

Learning.IsBayesAlgEnvSeq.gap_le_of_mem_Icc.{u_1, u_2, u_4}
  {𝓔 : Type u_1} {𝓐 : Type u_2} {Ω : Type u_4} [MeasurableSpace 𝓔]
  [MeasurableSpace 𝓐] [Nonempty 𝓐]
  {κ : ProbabilityTheory.Kernel (𝓔 × 𝓐) ℝ} {E : Ω → 𝓔} {A : ℕ → Ω → 𝓐}
  {n : ℕ} {ω : Ω} {l u : ℝ}
  (h : ∀ (e : 𝓔) (a : 𝓐), ∫ (x : ℝ), id x ∂κ (e, a) ∈ Set.Icc l u) :
  gap κ E A n ω ≤ u - l
Learning.IsBayesAlgEnvSeq.gap_le_of_mem_Icc.{u_1,
    u_2, u_4}
  {𝓔 : Type u_1} {𝓐 : Type u_2}
  {Ω : Type u_4} [MeasurableSpace 𝓔]
  [MeasurableSpace 𝓐] [Nonempty 𝓐]
  {κ : ProbabilityTheory.Kernel (𝓔 × 𝓐) ℝ}
  {E : Ω → 𝓔} {A : ℕ → Ω → 𝓐} {n : ℕ}
  {ω : Ω} {l u : ℝ}
  (h :
    ∀ (e : 𝓔) (a : 𝓐),
      ∫ (x : ℝ), id x ∂κ (e, a) ∈
        Set.Icc l u) :
  gap κ E A n ω ≤ u - l

Code

lemma gap_le_of_mem_Icc [Nonempty 𝓐] {κ : Kernel (𝓔 × 𝓐) ℝ} {E : Ω → 𝓔} {A : ℕ → Ω → 𝓐} {n : ℕ}
    {ω : Ω} {l u : ℝ} (h : ∀ e a, (κ (e, a))[id] ∈ Set.Icc l u) : gap κ E A n ω ≤ u - l

Type uses (1)

gap

Body uses (1)

gap_le_of_mem_Icc

Used by (1)

integrable_gap

Actions: Source · Open Issue

Proof

Bandits.gap_le_of_mem_Icc (h (E ω))

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

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

gap

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

`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

`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

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

`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 = fun ω => ∑ 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 = fun ω =>
    ∑ s ∈ Finset.range n, gap κ E A s ω

Code

lemma regret_eq_sum_gap' {κ : Kernel (𝓔 × 𝓐) ℝ} {E : Ω → 𝓔} {A : ℕ → Ω → 𝓐} {n : ℕ} :
    regret κ E A n = fun ω ↦ ∑ s ∈ range n, gap κ E A s ω

Type uses (2)

Body uses (1)

regret_eq_sum_gap

Used by (2)

Actions: Source · Open Issue

Proof

funext fun _ ↦ regret_eq_sum_gap

`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

`integrable_regret`🔗

LemmaLearning.IsBayesAlgEnvSeq.integrable_regret

Details

No docstring.

theorem

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

Code

lemma integrable_regret [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 (regret κ E A n) P

Type uses (1)

regret

Body uses (3)

Actions: Source · Open Issue

Proof

by
  rw [regret_eq_sum_gap']
  exact integrable_finsetSum _ (fun _ _ ↦ integrable_gap hE hA h)

2.4. Online.Bandit.BayesRegret🔗

actionMean🔗

measurable_actionMean🔗

measurable_uncurry_actionMean_comp🔗

integrable_uncurry_actionMean_comp🔗

bestAction🔗

measurable_bestAction🔗

gap🔗

gap_nonneg_of_le🔗

gap_le_of_mem_Icc🔗

gap_eq_sub🔗

measurable_gap🔗

integrable_gap🔗

regret🔗

regret_eq_sum_gap🔗

regret_eq_sum_gap'🔗

measurable_regret🔗

integrable_regret🔗

`actionMean`🔗

`measurable_actionMean`🔗

`measurable_uncurry_actionMean_comp`🔗

`integrable_uncurry_actionMean_comp`🔗

`bestAction`🔗

`measurable_bestAction`🔗

`gap`🔗

`gap_nonneg_of_le`🔗

`gap_le_of_mem_Icc`🔗

`gap_eq_sub`🔗

`measurable_gap`🔗

`integrable_gap`🔗

`regret`🔗

`regret_eq_sum_gap`🔗

`regret_eq_sum_gap'`🔗

`measurable_regret`🔗

`integrable_regret`🔗