`Learning.pullCount_le_add`🔗

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

LemmaLearning.pullCount_le_add

Details

No docstring.

theorem

Learning.pullCount_le_add.{u_1, u_3} {𝓐 : Type u_1} {Ω : Type u_3}
  [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} (a : 𝓐) (n C : ℕ) (ω : Ω) :
  pullCount A a n ω ≤
    C + 1 +
      ∑ s ∈ Finset.range n,
        Set.indicator {s | A s ω = a ∧ C < pullCount A a s ω} 1 s
Learning.pullCount_le_add.{u_1, u_3}
  {𝓐 : Type u_1} {Ω : Type u_3}
  [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} (a : 𝓐)
  (n C : ℕ) (ω : Ω) :
  pullCount A a n ω ≤
    C + 1 +
      ∑ s ∈ Finset.range n,
        Set.indicator
          {s |
            A s ω = a ∧
              C < pullCount A a s ω}
          1 s

Code

lemma pullCount_le_add (a : 𝓐) (n C : ℕ) (ω : Ω) :
    pullCount A a n ω ≤ C + 1 +
      ∑ s ∈ range n, {s | A s ω = a ∧ C < pullCount A a s ω}.indicator 1 s

Type uses (1)

pullCount

Body uses (1)

pullCount_eq_sum

Used by (1)

pullCount_le_add_three

Actions: Source · Open Issue

Proof

by
  rw [pullCount_eq_sum]
  calc ∑ s ∈ range n, if A s ω = a then 1 else 0
  _ ≤ ∑ s ∈ range n, ({s | A s ω = a ∧ pullCount A a s ω ≤ C}.indicator 1 s +
      {s | A s ω = a ∧ C < pullCount A a s ω}.indicator 1 s) := by
    gcongr with s hs
    simp [Set.indicator_apply]
    grind
  _ = ∑ s ∈ range n, {s | A s ω = a ∧ pullCount A a s ω ≤ C}.indicator 1 s +
      ∑ s ∈ range n, {s | A s ω = a ∧ C < pullCount A a s ω}.indicator 1 s := by
    rw [Finset.sum_add_distrib]
  _ ≤ C + 1 + ∑ s ∈ range n, {s | A s ω = a ∧ C < pullCount A a s ω}.indicator 1 s := by
    gcongr
    have h_le n : ∑ s ∈ range n, {s | A s ω = a ∧ pullCount A a s ω ≤ C}.indicator 1 s ≤
        pullCount A a n ω := by
      rw [pullCount_eq_sum]
      gcongr with s hs
      simp only [Set.indicator_apply, Set.mem_setOf_eq, Pi.one_apply]
      grind
    induction n with
    | zero => simp
    | succ n hn =>
      rw [Finset.sum_range_succ]
      rcases le_or_gt (pullCount A a n ω) C with h_pc | h_pc
      · have hn' : ∑ s ∈ range n, {s | A s ω = a ∧ pullCount A a s ω ≤ C}.indicator 1 s ≤ C :=
          (h_le n).trans h_pc
        grw [hn']
        gcongr
        simp only [Set.indicator_apply, Set.mem_setOf_eq, Pi.one_apply]
        grind
      · refine le_trans ?_ hn
        simp [h_pc]

Dependency graph

Type dependencies (1)

`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

Learning.pullCount_le_add🔗

pullCount_le_add🔗

pullCount🔗

`Learning.pullCount_le_add`🔗

`pullCount_le_add`🔗

`pullCount`🔗