`Bandits.UCB.pullCount_le_add_three`🔗

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

`pullCount_le_add_three`🔗

LemmaBandits.UCB.pullCount_le_add_three

Details

No docstring.

theorem

Bandits.UCB.pullCount_le_add_three.{u_1} {K : ℕ} {c : ℝ}
  {ν : ProbabilityTheory.Kernel (Fin K) ℝ} {Ω : Type u_1}
  {A : ℕ → Ω → Fin K} {R : ℕ → Ω → ℝ} [Nonempty (Fin K)] (a : Fin K)
  (n C : ℕ) (ω : Ω) :
  Learning.pullCount A a n ω ≤
    C + 1 +
          ∑ s ∈ Finset.range n,
            Set.indicator
              {s |
                A s ω = a ∧
                  C < Learning.pullCount A a s ω ∧
                    ∫ (x : ℝ), id x ∂ν (bestArm ν) ≤
                        Learning.empMean A R (bestArm ν) s ω +
                          ucbWidth A c (bestArm ν) s ω ∧
                      Learning.empMean A R (A s ω) s ω -
                          ucbWidth A c (A s ω) s ω ≤
                        ∫ (x : ℝ), id x ∂ν (A s ω)}
              1 s +
        ∑ s ∈ Finset.range n,
          Set.indicator
            {s |
              C < Learning.pullCount A a s ω ∧
                Learning.empMean A R (bestArm ν) s ω +
                    ucbWidth A c (bestArm ν) s ω <
                  ∫ (x : ℝ), id x ∂ν (bestArm ν)}
            1 s +
      ∑ s ∈ Finset.range n,
        Set.indicator
          {s |
            C < Learning.pullCount A a s ω ∧
              ∫ (x : ℝ), id x ∂ν a <
                Learning.empMean A R a s ω - ucbWidth A c a s ω}
          1 s
Bandits.UCB.pullCount_le_add_three.{u_1}
  {K : ℕ} {c : ℝ}
  {ν : ProbabilityTheory.Kernel (Fin K) ℝ}
  {Ω : Type u_1} {A : ℕ → Ω → Fin K}
  {R : ℕ → Ω → ℝ} [Nonempty (Fin K)]
  (a : Fin K) (n C : ℕ) (ω : Ω) :
  Learning.pullCount A a n ω ≤
    C + 1 +
          ∑ s ∈ Finset.range n,
            Set.indicator
              {s |
                A s ω = a ∧
                  C <
                      Learning.pullCount A
                        a s ω ∧
                    ∫ (x : ℝ),
                          id
                            x ∂ν
                            (bestArm ν) ≤
                        Learning.empMean A
                            R (bestArm ν)
                            s ω +
                          ucbWidth A c
                            (bestArm ν) s
                            ω ∧
                      Learning.empMean A R
                            (A s ω) s ω -
                          ucbWidth A c
                            (A s ω) s ω ≤
                        ∫ (x : ℝ),
                          id x ∂ν (A s ω)}
              1 s +
        ∑ s ∈ Finset.range n,
          Set.indicator
            {s |
              C <
                  Learning.pullCount A a s
                    ω ∧
                Learning.empMean A R
                      (bestArm ν) s ω +
                    ucbWidth A c
                      (bestArm ν) s ω <
                  ∫ (x : ℝ),
                    id x ∂ν (bestArm ν)}
            1 s +
      ∑ s ∈ Finset.range n,
        Set.indicator
          {s |
            C <
                Learning.pullCount A a s
                  ω ∧
              ∫ (x : ℝ), id x ∂ν a <
                Learning.empMean A R a s
                    ω -
                  ucbWidth A c a s ω}
          1 s

Code

lemma pullCount_le_add_three [Nonempty (Fin K)] (a : Fin K) (n C : ℕ) (ω : Ω) :
    pullCount A a n ω ≤ C + 1 +
      ∑ s ∈ range n, {s | A s ω = a ∧ C < pullCount A a s ω ∧
        (ν (bestArm ν))[id] ≤ empMean A R (bestArm ν) s ω + ucbWidth A c (bestArm ν) s ω ∧
        empMean A R (A s ω) s ω - ucbWidth A c (A s ω) s ω ≤ (ν (A s ω))[id]}.indicator 1 s +
      ∑ s ∈ range n,
        {s | C < pullCount A a s ω ∧ empMean A R (bestArm ν) s ω + ucbWidth A c (bestArm ν) s ω <
          (ν (bestArm ν))[id]}.indicator 1 s +
      ∑ s ∈ range n,
        {s | C < pullCount A a s ω ∧ (ν a)[id] <
          empMean A R a s ω - ucbWidth A c a s ω}.indicator 1 s

Type uses (4)

Body uses (1)

pullCount_le_add

Used by (1)

pullCount_le_add_three_ae

Actions: Source · Open Issue

Proof

by
  refine (pullCount_le_add a n C ω).trans ?_
  simp_rw [add_assoc]
  gcongr
  simp_rw [← add_assoc]
  let A' := {s | A s ω = a ∧ C < pullCount A a s ω}
  let B := {s | A s ω = a ∧ C < pullCount A a s ω ∧
        (ν (bestArm ν))[id] ≤ empMean A R (bestArm ν) s ω + ucbWidth A c (bestArm ν) s ω ∧
        empMean A R (A s ω) s ω - ucbWidth A c (A s ω) s ω ≤ (ν (A s ω))[id]}
  let C' := {s | C < pullCount A a s ω ∧
    empMean A R (bestArm ν) s ω + ucbWidth A c (bestArm ν) s ω < (ν (bestArm ν))[id]}
  let D := {s | C < pullCount A a s ω ∧ (ν a)[id] < empMean A R a s ω - ucbWidth A c a s ω}
  change ∑ s ∈ range n, A'.indicator 1 s ≤
    ∑ s ∈ range n, B.indicator 1 s + ∑ s ∈ range n, C'.indicator 1 s +
      ∑ s ∈ range n, D.indicator 1 s
  have h_union : A' ⊆ B ∪ C' ∪ D := by simp [A', B, C', D]; grind
  calc
    (∑ s ∈ range n, A'.indicator 1 s)
    _ ≤ (∑ s ∈ range n, (B ∪ C' ∪ D).indicator (fun _ ↦ (1 : ℕ)) s) := by
      gcongr with n hn
      by_cases h : n ∈ A'
      · have : n ∈ B ∪ C' ∪ D := h_union h
        simp [h, this]
      · simp [h]
    _ ≤ ∑ s ∈ range n, (B.indicator 1 s + C'.indicator 1 s + D.indicator 1 s) := by
      gcongr with s
      simp [Set.indicator_apply]
      grind
    _ = ∑ s ∈ range n, B.indicator 1 s + ∑ s ∈ range n, C'.indicator 1 s +
          ∑ s ∈ range n, D.indicator 1 s := by
      rw [Finset.sum_add_distrib, Finset.sum_add_distrib]

Dependency graph

Type dependencies (4)

`pullCount`🔗

DefinitionLearning.pullCount

Details

Number of times action a was chosen up to time t (excluding t).

def

Learning.pullCount.{u_1, u_3} {𝓐 : Type u_1} {Ω : Type u_3}
  [DecidableEq 𝓐] (A : ℕ → Ω → 𝓐) (a : 𝓐) (t : ℕ) (ω : Ω) : ℕ
Learning.pullCount.{u_1, u_3}
  {𝓐 : Type u_1} {Ω : Type u_3}
  [DecidableEq 𝓐] (A : ℕ → Ω → 𝓐) (a : 𝓐)
  (t : ℕ) (ω : Ω) : ℕ

Code

noncomputable
def pullCount (A : ℕ → Ω → 𝓐) (a : 𝓐) (t : ℕ) (ω : Ω) : ℕ :=
  #(filter (fun s ↦ A s ω = a) (range t))

Used by (146)

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

`empMean`🔗

DefinitionLearning.empMean

Details

Empirical mean reward obtained when pulling action a up to time t (exclusive).

def

Learning.empMean.{u_1, u_3} {𝓐 : Type u_1} {Ω : Type u_3}
  [DecidableEq 𝓐] (A : ℕ → Ω → 𝓐) (R' : ℕ → Ω → ℝ) (a : 𝓐) (t : ℕ)
  (ω : Ω) : ℝ
Learning.empMean.{u_1, u_3} {𝓐 : Type u_1}
  {Ω : Type u_3} [DecidableEq 𝓐]
  (A : ℕ → Ω → 𝓐) (R' : ℕ → Ω → ℝ) (a : 𝓐)
  (t : ℕ) (ω : Ω) : ℝ

Code

noncomputable
def empMean (A : ℕ → Ω → 𝓐) (R' : ℕ → Ω → ℝ) (a : 𝓐) (t : ℕ) (ω : Ω) : ℝ :=
  sumRewards A R' a t ω / pullCount A a t ω

Body uses (2)

Used by (34)

Actions: Source · Open Issue

`ucbWidth`🔗

DefinitionBandits.UCB.ucbWidth

Details

The exploration bonus of the UCB algorithm, which corresponds to the width of a confidence interval.

def

Bandits.UCB.ucbWidth.{u_1} {K : ℕ} {Ω : Type u_1} (A : ℕ → Ω → Fin K)
  (c : ℝ) (a : Fin K) (n : ℕ) (ω : Ω) : ℝ
Bandits.UCB.ucbWidth.{u_1} {K : ℕ}
  {Ω : Type u_1} (A : ℕ → Ω → Fin K)
  (c : ℝ) (a : Fin K) (n : ℕ) (ω : Ω) : ℝ

Code

noncomputable def ucbWidth (A : ℕ → Ω → Fin K) (c : ℝ) (a : Fin K) (n : ℕ) (ω : Ω) : ℝ :=
  √(2 * c * log (n + 1) / pullCount A a n ω)

Body uses (1)

pullCount

Used by (16)

Actions: Source · Open Issue

All dependencies, transitively (1)

`sumRewards`🔗

DefinitionLearning.sumRewards

Details

Sum of rewards obtained when pulling action a up to time t (exclusive).

def

Learning.sumRewards.{u_1, u_3} {𝓐 : Type u_1} {Ω : Type u_3}
  [DecidableEq 𝓐] (A : ℕ → Ω → 𝓐) (R' : ℕ → Ω → ℝ) (a : 𝓐) (t : ℕ)
  (ω : Ω) : ℝ
Learning.sumRewards.{u_1, u_3}
  {𝓐 : Type u_1} {Ω : Type u_3}
  [DecidableEq 𝓐] (A : ℕ → Ω → 𝓐)
  (R' : ℕ → Ω → ℝ) (a : 𝓐) (t : ℕ)
  (ω : Ω) : ℝ

Code

def sumRewards (A : ℕ → Ω → 𝓐) (R' : ℕ → Ω → ℝ) (a : 𝓐) (t : ℕ) (ω : Ω) : ℝ :=
  ∑ s ∈ range t, if A s ω = a then R' s ω else 0

Used by (44)

Actions: Source · Open Issue

Bandits.UCB.pullCount_le_add_three🔗

pullCount_le_add_three🔗

pullCount🔗

bestArm🔗

empMean🔗

ucbWidth🔗

sumRewards🔗

`Bandits.UCB.pullCount_le_add_three`🔗

`pullCount_le_add_three`🔗

`pullCount`🔗

`bestArm`🔗

`empMean`🔗

`ucbWidth`🔗

`sumRewards`🔗