`Bandits.probReal_sum_le_sum_streamMeasure`🔗

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

`probReal_sum_le_sum_streamMeasure`🔗

LemmaBandits.probReal_sum_le_sum_streamMeasure

Details

No docstring.

theorem

Bandits.probReal_sum_le_sum_streamMeasure.{u_1} {𝓐 : Type u_1}
  {m𝓐 : MeasurableSpace 𝓐} {ν : ProbabilityTheory.Kernel 𝓐 ℝ}
  [ProbabilityTheory.IsMarkovKernel ν] [Nonempty 𝓐] [Fintype 𝓐]
  {c : NNReal}
  (hν :
    ∀ (a : 𝓐),
      ProbabilityTheory.HasSubgaussianMGF
        (fun x => x - ∫ (x : ℝ), id x ∂ν a) c (ν a))
  (a : 𝓐) (m : ℕ) :
  MeasureTheory.Measure.real (streamMeasure ν)
      {ω |
        ∑ s ∈ Finset.range m, ω s (bestArm ν) ≤
          ∑ s ∈ Finset.range m, ω s a} ≤
    Real.exp (-↑m * gap ν a ^ 2 / (4 * ↑c))
Bandits.probReal_sum_le_sum_streamMeasure.{u_1}
  {𝓐 : Type u_1} {m𝓐 : MeasurableSpace 𝓐}
  {ν : ProbabilityTheory.Kernel 𝓐 ℝ}
  [ProbabilityTheory.IsMarkovKernel ν]
  [Nonempty 𝓐] [Fintype 𝓐] {c : NNReal}
  (hν :
    ∀ (a : 𝓐),
      ProbabilityTheory.HasSubgaussianMGF
        (fun x =>
          x - ∫ (x : ℝ), id x ∂ν a)
        c (ν a))
  (a : 𝓐) (m : ℕ) :
  MeasureTheory.Measure.real
      (streamMeasure ν)
      {ω |
        ∑ s ∈ Finset.range m,
            ω s (bestArm ν) ≤
          ∑ s ∈ Finset.range m, ω s a} ≤
    Real.exp
      (-↑m * gap ν a ^ 2 / (4 * ↑c))

Code

lemma probReal_sum_le_sum_streamMeasure [Fintype 𝓐] {c : ℝ≥0}
    (hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) c (ν a)) (a : 𝓐) (m : ℕ) :
    (streamMeasure ν).real
        {ω | ∑ s ∈ range m, ω s (bestArm ν) ≤ ∑ s ∈ range m, ω s a} ≤
      Real.exp (-↑m * gap ν a ^ 2 / (4 * c))

Type uses (3)

Body uses (9)

Used by (1)

probReal_sumRewards_le_sumRewards_le

Actions: Source · Open Issue

Proof

by
  by_cases ha : a = bestArm ν
  · simp [ha]
  refine (HasSubgaussianMGF.measure_sum_le_sum_le' (cX := fun _ ↦ c) (cY := fun _ ↦ c)
    ?_ ?_ ?_ ?_ ?_ ?_).trans_eq ?_
  · exact iIndepFun_eval_streamMeasure'' ν (bestArm ν)
  · exact iIndepFun_eval_streamMeasure'' ν a
  · intro i him
    simp_rw [integral_eval_streamMeasure]
    refine (hν (bestArm ν)).congr_identDistrib ?_
    exact (identDistrib_eval_eval_id_streamMeasure _ _ _).symm.sub_const _
  · intro i him
    simp_rw [integral_eval_streamMeasure]
    refine (hν a).congr_identDistrib ?_
    exact (identDistrib_eval_eval_id_streamMeasure _ _ _).symm.sub_const _
  · exact indepFun_eval_streamMeasure' ν (Ne.symm ha)
  · gcongr 1 with i him
    simp_rw [integral_eval_streamMeasure]
    exact le_bestArm a
  · congr 1
    simp_rw [integral_eval_streamMeasure]
    simp only [id_eq, sum_const, card_range, nsmul_eq_mul, NNReal.coe_mul, NNReal.coe_natCast,
      gap_eq_bestArm_sub, neg_mul]
    field_simp
    ring

Dependency graph

Type dependencies (3)

`streamMeasure`🔗

DefinitionBandits.streamMeasure

Details

Measure of an infinite stream of rewards from each action.

def

Bandits.streamMeasure.{u_1, u_2} {𝓐 : Type u_1} {R : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐} {mR : MeasurableSpace R}
  (ν : ProbabilityTheory.Kernel 𝓐 R) : MeasureTheory.Measure (ℕ → 𝓐 → R)
Bandits.streamMeasure.{u_1, u_2}
  {𝓐 : Type u_1} {R : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐}
  {mR : MeasurableSpace R}
  (ν : ProbabilityTheory.Kernel 𝓐 R) :
  MeasureTheory.Measure (ℕ → 𝓐 → R)

Code

noncomputable
def streamMeasure (ν : Kernel 𝓐 R) : Measure (ℕ → 𝓐 → R) :=
  Measure.infinitePi fun _ ↦ Measure.infinitePi ν

Used by (56)

Actions: Source · Open Issue

`bestArm`🔗

DefinitionBandits.bestArm

Details

action with the highest mean.

def

Bandits.bestArm.{u_1} {𝓐 : Type u_1} {m𝓐 : MeasurableSpace 𝓐}
  [Fintype 𝓐] [Nonempty 𝓐] (ν : ProbabilityTheory.Kernel 𝓐 ℝ) : 𝓐
Bandits.bestArm.{u_1} {𝓐 : Type u_1}
  {m𝓐 : MeasurableSpace 𝓐} [Fintype 𝓐]
  [Nonempty 𝓐]
  (ν : ProbabilityTheory.Kernel 𝓐 ℝ) : 𝓐

Code

noncomputable def bestArm (ν : Kernel 𝓐 ℝ) : 𝓐 :=
  (exists_max_image univ (fun a ↦ (ν a)[id]) (univ_nonempty_iff.mpr inferInstance)).choose

Used by (18)

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

Bandits.probReal_sum_le_sum_streamMeasure🔗

probReal_sum_le_sum_streamMeasure🔗

streamMeasure🔗

bestArm🔗

gap🔗

`Bandits.probReal_sum_le_sum_streamMeasure`🔗

`probReal_sum_le_sum_streamMeasure`🔗

`streamMeasure`🔗

`bestArm`🔗

`gap`🔗