SequentialLearning.FiniteActions

`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

`pullCount'`🔗

DefinitionLearning.pullCount'

Details

Number of pulls of arm a up to (and including) time n. This is the number of entries in h in which the arm is a.

def

Learning.pullCount'.{u_1, u_2} {𝓐 : Type u_1} {R : Type u_2}
  [DecidableEq 𝓐] (n : ℕ) (h : ↥(Finset.Iic n) → 𝓐 × R) (a : 𝓐) : ℕ
Learning.pullCount'.{u_1, u_2}
  {𝓐 : Type u_1} {R : Type u_2}
  [DecidableEq 𝓐] (n : ℕ)
  (h : ↥(Finset.Iic n) → 𝓐 × R) (a : 𝓐) :
  ℕ

Code

noncomputable
def pullCount' (n : ℕ) (h : Iic n → 𝓐 × R) (a : 𝓐) := #{s | (h s).1 = a}

Used by (29)

Actions: Source · Open Issue

`pullCount_zero`🔗

LemmaLearning.pullCount_zero

Details

No docstring.

theorem

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

Code

lemma pullCount_zero (a : 𝓐) : pullCount A a 0 = 0

Type uses (1)

pullCount

Used by (15)

Actions: Source · Open Issue

Proof

by ext; simp [pullCount]

`pullCount_zero_apply`🔗

LemmaLearning.pullCount_zero_apply

Details

No docstring.

theorem

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

Code

lemma pullCount_zero_apply (a : 𝓐) (ω : Ω) : pullCount A a 0 ω = 0

Type uses (1)

pullCount

Body uses (1)

pullCount_zero

Actions: Source · Open Issue

Proof

by simp

`pullCount_one`🔗

LemmaLearning.pullCount_one

Details

No docstring.

theorem

Learning.pullCount_one.{u_1, u_3} {𝓐 : Type u_1} {Ω : Type u_3}
  [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} {a : 𝓐} {ω : Ω} :
  pullCount A a 1 ω = if A 0 ω = a then 1 else 0
Learning.pullCount_one.{u_1, u_3}
  {𝓐 : Type u_1} {Ω : Type u_3}
  [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} {a : 𝓐}
  {ω : Ω} :
  pullCount A a 1 ω =
    if A 0 ω = a then 1 else 0

Code

lemma pullCount_one : pullCount A a 1 ω = if A 0 ω = a then 1 else 0

Type uses (1)

pullCount

Used by (3)

Actions: Source · Open Issue

Proof

by
  simp only [pullCount, range_one]
  split_ifs with h
  · rw [card_eq_one]
    refine ⟨0, by simp [h]⟩
  · simp [h]

`monotone_pullCount`🔗

LemmaLearning.monotone_pullCount

Details

No docstring.

theorem

Learning.monotone_pullCount.{u_1, u_3} {𝓐 : Type u_1} {Ω : Type u_3}
  [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} (a : 𝓐) (ω : Ω) :
  Monotone fun x => pullCount A a x ω
Learning.monotone_pullCount.{u_1, u_3}
  {𝓐 : Type u_1} {Ω : Type u_3}
  [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} (a : 𝓐)
  (ω : Ω) :
  Monotone fun x => pullCount A a x ω

Code

lemma monotone_pullCount (a : 𝓐) (ω : Ω) : Monotone (pullCount A a · ω)

Type uses (1)

pullCount

Used by (5)

Actions: Source · Open Issue

Proof

fun _ _ _ ↦ card_le_card (filter_subset_filter _ (by simpa))

`pullCount_mono`🔗

LemmaLearning.pullCount_mono

Details

No docstring.

theorem

Learning.pullCount_mono.{u_1, u_3} {𝓐 : Type u_1} {Ω : Type u_3}
  [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} (a : 𝓐) {n m : ℕ} (hnm : n ≤ m)
  (ω : Ω) : pullCount A a n ω ≤ pullCount A a m ω
Learning.pullCount_mono.{u_1, u_3}
  {𝓐 : Type u_1} {Ω : Type u_3}
  [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} (a : 𝓐)
  {n m : ℕ} (hnm : n ≤ m) (ω : Ω) :
  pullCount A a n ω ≤ pullCount A a m ω

Code

lemma pullCount_mono (a : 𝓐) {n m : ℕ} (hnm : n ≤ m) (ω : Ω) :
    pullCount A a n ω ≤ pullCount A a m ω

Type uses (1)

pullCount

Body uses (1)

monotone_pullCount

Used by (6)

Actions: Source · Open Issue

Proof

monotone_pullCount a ω hnm

`pullCount_action_eq_pullCount_add_one`🔗

LemmaLearning.pullCount_action_eq_pullCount_add_one

Details

No docstring.

theorem

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

Code

lemma pullCount_action_eq_pullCount_add_one (t : ℕ) (ω : Ω) :
    pullCount A (A t ω) (t + 1) ω = pullCount A (A t ω) t ω + 1

Type uses (1)

pullCount

Used by (7)

Actions: Source · Open Issue

Proof

by
  simp [pullCount, range_add_one, filter_insert]

`pullCount_eq_pullCount_of_action_ne`🔗

LemmaLearning.pullCount_eq_pullCount_of_action_ne

Details

No docstring.

theorem

Learning.pullCount_eq_pullCount_of_action_ne.{u_1, u_3} {𝓐 : Type u_1}
  {Ω : Type u_3} [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} {a : 𝓐} {t : ℕ} {ω : Ω}
  (ha : A t ω ≠ a) : pullCount A a (t + 1) ω = pullCount A a t ω
Learning.pullCount_eq_pullCount_of_action_ne.{u_1,
    u_3}
  {𝓐 : Type u_1} {Ω : Type u_3}
  [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} {a : 𝓐}
  {t : ℕ} {ω : Ω} (ha : A t ω ≠ a) :
  pullCount A a (t + 1) ω =
    pullCount A a t ω

Code

lemma pullCount_eq_pullCount_of_action_ne (ha : A t ω ≠ a) :
    pullCount A a (t + 1) ω = pullCount A a t ω

Type uses (1)

pullCount

Used by (5)

Actions: Source · Open Issue

Proof

by
  simp [pullCount, range_add_one, filter_insert, ha]

`pullCount_add_one`🔗

LemmaLearning.pullCount_add_one

Details

No docstring.

theorem

Learning.pullCount_add_one.{u_1, u_3} {𝓐 : Type u_1} {Ω : Type u_3}
  [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} {a : 𝓐} {t : ℕ} {ω : Ω} :
  pullCount A a (t + 1) ω =
    pullCount A a t ω + if A t ω = a then 1 else 0
Learning.pullCount_add_one.{u_1, u_3}
  {𝓐 : Type u_1} {Ω : Type u_3}
  [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} {a : 𝓐}
  {t : ℕ} {ω : Ω} :
  pullCount A a (t + 1) ω =
    pullCount A a t ω +
      if A t ω = a then 1 else 0

Code

lemma pullCount_add_one :
    pullCount A a (t + 1) ω = pullCount A a t ω + if A t ω = a then 1 else 0

Type uses (1)

pullCount

Body uses (2)

Used by (7)

Actions: Source · Open Issue

Proof

by
  split_ifs with h
  · rw [← h, pullCount_action_eq_pullCount_add_one]
  · rw [pullCount_eq_pullCount_of_action_ne h, add_zero]

`pullCount_eq_sum`🔗

LemmaLearning.pullCount_eq_sum

Details

No docstring.

theorem

Learning.pullCount_eq_sum.{u_1, u_3} {𝓐 : Type u_1} {Ω : Type u_3}
  [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} (a : 𝓐) (t : ℕ) (ω : Ω) :
  pullCount A a t ω = ∑ s ∈ Finset.range t, if A s ω = a then 1 else 0
Learning.pullCount_eq_sum.{u_1, u_3}
  {𝓐 : Type u_1} {Ω : Type u_3}
  [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} (a : 𝓐)
  (t : ℕ) (ω : Ω) :
  pullCount A a t ω =
    ∑ s ∈ Finset.range t,
      if A s ω = a then 1 else 0

Code

lemma pullCount_eq_sum (a : 𝓐) (t : ℕ) (ω : Ω) :
    pullCount A a t ω = ∑ s ∈ range t, if A s ω = a then 1 else 0

Type uses (1)

pullCount

Used by (8)

Actions: Source · Open Issue

Proof

by simp [pullCount]

`pullCount'_eq_sum`🔗

LemmaLearning.pullCount'_eq_sum

Details

No docstring.

theorem

Learning.pullCount'_eq_sum.{u_1, u_2} {𝓐 : Type u_1} {R : Type u_2}
  [DecidableEq 𝓐] (n : ℕ) (h : ↥(Finset.Iic n) → 𝓐 × R) (a : 𝓐) :
  pullCount' n h a = ∑ s, if Prod.fst (h s) = a then 1 else 0
Learning.pullCount'_eq_sum.{u_1, u_2}
  {𝓐 : Type u_1} {R : Type u_2}
  [DecidableEq 𝓐] (n : ℕ)
  (h : ↥(Finset.Iic n) → 𝓐 × R) (a : 𝓐) :
  pullCount' n h a =
    ∑ s,
      if Prod.fst (h s) = a then 1 else 0

Code

lemma pullCount'_eq_sum (n : ℕ) (h : Iic n → 𝓐 × R) (a : 𝓐) :
    pullCount' n h a = ∑ s : Iic n, if (h s).1 = a then 1 else 0

Type uses (1)

pullCount'

Used by (3)

Actions: Source · Open Issue

Proof

by simp [pullCount']

`pullCount_add_one_eq_pullCount'`🔗

LemmaLearning.pullCount_add_one_eq_pullCount'

Details

No docstring.

theorem

Learning.pullCount_add_one_eq_pullCount'.{u_1, u_2, u_3} {𝓐 : Type u_1}
  {R : Type u_2} {Ω : Type u_3} [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐}
  {R' : ℕ → Ω → R} {a : 𝓐} {n : ℕ} {ω : Ω} :
  pullCount A a (n + 1) ω =
    pullCount' n (fun i => (A (↑i) ω, R' (↑i) ω)) a
Learning.pullCount_add_one_eq_pullCount'.{u_1,
    u_2, u_3}
  {𝓐 : Type u_1} {R : Type u_2}
  {Ω : Type u_3} [DecidableEq 𝓐]
  {A : ℕ → Ω → 𝓐} {R' : ℕ → Ω → R} {a : 𝓐}
  {n : ℕ} {ω : Ω} :
  pullCount A a (n + 1) ω =
    pullCount' n
      (fun i => (A (↑i) ω, R' (↑i) ω)) a

Code

lemma pullCount_add_one_eq_pullCount' {n : ℕ} {ω : Ω} :
    pullCount A a (n + 1) ω = pullCount' n (fun i ↦ (A i ω, R' i ω)) a

Type uses (2)

Body uses (2)

Used by (5)

Actions: Source · Open Issue

Proof

by
  rw [pullCount_eq_sum, pullCount'_eq_sum]
  rw [Finset.sum_coe_sort (f := fun s ↦ if A s ω = a then 1 else 0) (Iic n)]
  congr with m
  simp only [mem_range, mem_Iic]
  grind

`pullCount_eq_pullCount'`🔗

LemmaLearning.pullCount_eq_pullCount'

Details

No docstring.

theorem

Learning.pullCount_eq_pullCount'.{u_1, u_2, u_3} {𝓐 : Type u_1}
  {R : Type u_2} {Ω : Type u_3} [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐}
  {R' : ℕ → Ω → R} {a : 𝓐} {n : ℕ} {ω : Ω} (hn : n ≠ 0) :
  pullCount A a n ω =
    pullCount' (n - 1) (fun i => (A (↑i) ω, R' (↑i) ω)) a
Learning.pullCount_eq_pullCount'.{u_1,
    u_2, u_3}
  {𝓐 : Type u_1} {R : Type u_2}
  {Ω : Type u_3} [DecidableEq 𝓐]
  {A : ℕ → Ω → 𝓐} {R' : ℕ → Ω → R} {a : 𝓐}
  {n : ℕ} {ω : Ω} (hn : n ≠ 0) :
  pullCount A a n ω =
    pullCount' (n - 1)
      (fun i => (A (↑i) ω, R' (↑i) ω)) a

Code

lemma pullCount_eq_pullCount' {n : ℕ} {ω : Ω} (hn : n ≠ 0) :
    pullCount A a n ω = pullCount' (n - 1) (fun i ↦ (A i ω, R' i ω)) a

Type uses (2)

Body uses (1)

pullCount_add_one_eq_pullCount'

Used by (4)

Actions: Source · Open Issue

Proof

by
  cases n with
  | zero => exact absurd rfl hn
  | succ n => simp [pullCount_add_one_eq_pullCount' (R' := R')]

`pullCount'_mono`🔗

LemmaLearning.pullCount'_mono

Details

No docstring.

theorem

Learning.pullCount'_mono.{u_1, u_2, u_3} {𝓐 : Type u_1} {R : Type u_2}
  {Ω : Type u_3} [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} {R' : ℕ → Ω → R}
  {a : 𝓐} {ω : Ω} {n m : ℕ} (hnm : n ≤ m) :
  pullCount' n (fun i => (A (↑i) ω, R' (↑i) ω)) a ≤
    pullCount' m (fun i => (A (↑i) ω, R' (↑i) ω)) a
Learning.pullCount'_mono.{u_1, u_2, u_3}
  {𝓐 : Type u_1} {R : Type u_2}
  {Ω : Type u_3} [DecidableEq 𝓐]
  {A : ℕ → Ω → 𝓐} {R' : ℕ → Ω → R} {a : 𝓐}
  {ω : Ω} {n m : ℕ} (hnm : n ≤ m) :
  pullCount' n
      (fun i => (A (↑i) ω, R' (↑i) ω)) a ≤
    pullCount' m
      (fun i => (A (↑i) ω, R' (↑i) ω)) a

Code

lemma pullCount'_mono {n m : ℕ} (hnm : n ≤ m) :
    pullCount' n (fun i ↦ (A i ω, R' i ω)) a ≤ pullCount' m (fun i ↦ (A i ω, R' i ω)) a

Type uses (1)

pullCount'

Body uses (3)

Actions: Source · Open Issue

Proof

by
  rw [← pullCount_add_one_eq_pullCount', ← pullCount_add_one_eq_pullCount']
  exact pullCount_mono a (by lia) _

`pullCount_le`🔗

LemmaLearning.pullCount_le

Details

No docstring.

theorem

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

Code

lemma pullCount_le (a : 𝓐) (t : ℕ) (ω : Ω) : pullCount A a t ω ≤ t

Type uses (1)

pullCount

Used by (4)

Actions: Source · Open Issue

Proof

(card_filter_le _ _).trans_eq (by simp)

`pullCount_congr`🔗

LemmaLearning.pullCount_congr

Details

No docstring.

theorem

Learning.pullCount_congr.{u_1, u_3} {𝓐 : Type u_1} {Ω : Type u_3}
  [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} {a : 𝓐} {n : ℕ} {ω ω' : Ω}
  (h_eq : ∀ i ≤ n, A i ω = A i ω') :
  pullCount A a (n + 1) ω = pullCount A a (n + 1) ω'
Learning.pullCount_congr.{u_1, u_3}
  {𝓐 : Type u_1} {Ω : Type u_3}
  [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} {a : 𝓐}
  {n : ℕ} {ω ω' : Ω}
  (h_eq : ∀ i ≤ n, A i ω = A i ω') :
  pullCount A a (n + 1) ω =
    pullCount A a (n + 1) ω'

Code

lemma pullCount_congr {ω' : Ω} (h_eq : ∀ i ≤ n, A i ω = A i ω') :
    pullCount A a (n + 1) ω = pullCount A a (n + 1) ω'

Type uses (1)

pullCount

Used by (1)

stepsUntil_eq_congr

Actions: Source · Open Issue

Proof

by
  unfold pullCount
  congr 1 with s
  simp only [mem_filter, mem_range, and_congr_right_iff]
  intro hs
  rw [Nat.lt_add_one_iff] at hs
  rw [h_eq s hs]

`pullCount_lt_of_forall_ne`🔗

LemmaLearning.pullCount_lt_of_forall_ne

Details

No docstring.

theorem

Learning.pullCount_lt_of_forall_ne.{u_1, u_3} {𝓐 : Type u_1}
  {Ω : Type u_3} [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} {a : 𝓐} {n t : ℕ}
  {ω : Ω} (h_lt : ∀ (s : ℕ), pullCount A a (s + 1) ω ≠ t) (ht : t ≠ 0) :
  pullCount A a n ω < t
Learning.pullCount_lt_of_forall_ne.{u_1,
    u_3}
  {𝓐 : Type u_1} {Ω : Type u_3}
  [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} {a : 𝓐}
  {n t : ℕ} {ω : Ω}
  (h_lt :
    ∀ (s : ℕ),
      pullCount A a (s + 1) ω ≠ t)
  (ht : t ≠ 0) : pullCount A a n ω < t

Code

lemma pullCount_lt_of_forall_ne (h_lt : ∀ s, pullCount A a (s + 1) ω ≠ t) (ht : t ≠ 0) :
    pullCount A a n ω < t

Type uses (1)

pullCount

Body uses (2)

Used by (1)

exists_pullCount_eq_of_le

Actions: Source · Open Issue

Proof

by
  induction n with
  | zero => simpa using ht.bot_lt
  | succ n hn =>
    specialize h_lt n
    rw [pullCount_add_one] at h_lt ⊢
    grind

`exists_pullCount_eq_of_le`🔗

LemmaLearning.exists_pullCount_eq_of_le

Details

No docstring.

theorem

Learning.exists_pullCount_eq_of_le.{u_1, u_3} {𝓐 : Type u_1}
  {Ω : Type u_3} [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} {a : 𝓐} {n t : ℕ}
  {ω : Ω} (hnm : t ≤ pullCount A a (n + 1) ω) (ht : t ≠ 0) :
  ∃ s, pullCount A a (s + 1) ω = t
Learning.exists_pullCount_eq_of_le.{u_1,
    u_3}
  {𝓐 : Type u_1} {Ω : Type u_3}
  [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} {a : 𝓐}
  {n t : ℕ} {ω : Ω}
  (hnm : t ≤ pullCount A a (n + 1) ω)
  (ht : t ≠ 0) :
  ∃ s, pullCount A a (s + 1) ω = t

Code

lemma exists_pullCount_eq_of_le (hnm : t ≤ pullCount A a (n + 1) ω) (ht : t ≠ 0) :
    ∃ s, pullCount A a (s + 1) ω = t

Type uses (1)

pullCount

Body uses (1)

pullCount_lt_of_forall_ne

Used by (1)

stepsUntil_eq_leastGE

Actions: Source · Open Issue

Proof

by
  by_contra! h_contra
  refine lt_irrefl (pullCount A a (n + 1) ω) ?_
  refine lt_of_lt_of_le ?_ hnm
  exact pullCount_lt_of_forall_ne h_contra ht

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

`measurable_pullCount`🔗

LemmaLearning.measurable_pullCount

Details

No docstring.

theorem

Learning.measurable_pullCount.{u_1, u_3} {𝓐 : Type u_1} {Ω : Type u_3}
  {m𝓐 : MeasurableSpace 𝓐} {mΩ : MeasurableSpace Ω} [DecidableEq 𝓐]
  {A : ℕ → Ω → 𝓐} [MeasurableSingletonClass 𝓐]
  (hA : ∀ (n : ℕ), Measurable (A n)) (a : 𝓐) (t : ℕ) :
  Measurable fun ω => pullCount A a t ω
Learning.measurable_pullCount.{u_1, u_3}
  {𝓐 : Type u_1} {Ω : Type u_3}
  {m𝓐 : MeasurableSpace 𝓐}
  {mΩ : MeasurableSpace Ω} [DecidableEq 𝓐]
  {A : ℕ → Ω → 𝓐}
  [MeasurableSingletonClass 𝓐]
  (hA : ∀ (n : ℕ), Measurable (A n))
  (a : 𝓐) (t : ℕ) :
  Measurable fun ω => pullCount A a t ω

Code

lemma measurable_pullCount [MeasurableSingletonClass 𝓐] (hA : ∀ n, Measurable (A n))
    (a : 𝓐) (t : ℕ) :
    Measurable (fun ω : Ω ↦ pullCount A a t ω)

Type uses (1)

pullCount

Body uses (1)

pullCount_eq_sum

Used by (15)

Actions: Source · Open Issue

Proof

by
  simp_rw [pullCount_eq_sum]
  have h_meas s : Measurable (fun ω : Ω ↦ if A s ω = a then 1 else 0) := by
    refine Measurable.ite ?_ (by fun_prop) (by fun_prop)
    exact (measurableSet_singleton _).preimage (by fun_prop)
  fun_prop

`measurable_uncurry_pullCount`🔗

LemmaLearning.measurable_uncurry_pullCount

Details

No docstring.

theorem

Learning.measurable_uncurry_pullCount.{u_1, u_3} {𝓐 : Type u_1}
  {Ω : Type u_3} {m𝓐 : MeasurableSpace 𝓐} {mΩ : MeasurableSpace Ω}
  [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} [MeasurableEq 𝓐]
  (hA : ∀ (n : ℕ), Measurable (A n)) (t : ℕ) :
  Measurable fun p => pullCount A (Prod.snd p) t (Prod.fst p)
Learning.measurable_uncurry_pullCount.{u_1,
    u_3}
  {𝓐 : Type u_1} {Ω : Type u_3}
  {m𝓐 : MeasurableSpace 𝓐}
  {mΩ : MeasurableSpace Ω} [DecidableEq 𝓐]
  {A : ℕ → Ω → 𝓐} [MeasurableEq 𝓐]
  (hA : ∀ (n : ℕ), Measurable (A n))
  (t : ℕ) :
  Measurable fun p =>
    pullCount A (Prod.snd p) t
      (Prod.fst p)

Code

lemma measurable_uncurry_pullCount [MeasurableEq 𝓐]
    (hA : ∀ n, Measurable (A n)) (t : ℕ) :
    Measurable (fun p : Ω × 𝓐 ↦ pullCount A p.2 t p.1)

Type uses (1)

pullCount

Body uses (1)

pullCount_eq_sum

Used by (5)

Actions: Source · Open Issue

Proof

by
  simp_rw [pullCount_eq_sum]
  have h_meas s : Measurable (fun h : Ω × 𝓐 ↦ if A s h.1 = h.2 then 1 else 0) := by
    refine Measurable.ite ?_ (by fun_prop) (by fun_prop)
    exact measurableSet_eq_fun (by fun_prop) (by fun_prop)
  fun_prop

`measurable_uncurry_pullCount_comp`🔗

LemmaLearning.measurable_uncurry_pullCount_comp

Details

No docstring.

theorem

Learning.measurable_uncurry_pullCount_comp.{u_1, u_3} {𝓐 : Type u_1}
  {Ω : Type u_3} {m𝓐 : MeasurableSpace 𝓐} {mΩ : MeasurableSpace Ω}
  [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} [Countable 𝓐]
  [MeasurableSingletonClass 𝓐] (hA : ∀ (n : ℕ), Measurable (A n))
  {f : Ω → 𝓐} (hf : Measurable f) {g : Ω → ℕ} (hg : Measurable g) :
  Measurable fun ω => pullCount A (f ω) (g ω) ω
Learning.measurable_uncurry_pullCount_comp.{u_1,
    u_3}
  {𝓐 : Type u_1} {Ω : Type u_3}
  {m𝓐 : MeasurableSpace 𝓐}
  {mΩ : MeasurableSpace Ω} [DecidableEq 𝓐]
  {A : ℕ → Ω → 𝓐} [Countable 𝓐]
  [MeasurableSingletonClass 𝓐]
  (hA : ∀ (n : ℕ), Measurable (A n))
  {f : Ω → 𝓐} (hf : Measurable f)
  {g : Ω → ℕ} (hg : Measurable g) :
  Measurable fun ω =>
    pullCount A (f ω) (g ω) ω

Code

lemma measurable_uncurry_pullCount_comp [Countable 𝓐] [MeasurableSingletonClass 𝓐]
    (hA : ∀ n, Measurable (A n)) {f : Ω → 𝓐} (hf : Measurable f) {g : Ω → ℕ} (hg : Measurable g) :
    Measurable (fun ω ↦ pullCount A (f ω) (g ω) ω)

Type uses (1)

pullCount

Body uses (1)

measurable_pullCount

Used by (6)

Actions: Source · Open Issue

Proof

by
  change Measurable ((fun aω ↦ pullCount A aω.1 (g aω.2) aω.2) ∘ fun ω ↦ (f ω, ω))
  apply Measurable.comp _ (by fun_prop)
  refine measurable_from_prod_countable_right fun a ↦ ?_
  change Measurable ((fun tω ↦ pullCount A a tω.1 tω.2) ∘ fun ω ↦ (g ω, ω))
  apply Measurable.comp _ (by fun_prop)
  exact measurable_from_prod_countable_right (fun t ↦ measurable_pullCount hA a t)

`measurable_pullCount'`🔗

LemmaLearning.measurable_pullCount'

Details

No docstring.

theorem

Learning.measurable_pullCount'.{u_1, u_2} {𝓐 : Type u_1} {R : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐} {mR : MeasurableSpace R} [DecidableEq 𝓐]
  [MeasurableSingletonClass 𝓐] (n : ℕ) (a : 𝓐) :
  Measurable fun h => pullCount' n h a
Learning.measurable_pullCount'.{u_1, u_2}
  {𝓐 : Type u_1} {R : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐}
  {mR : MeasurableSpace R} [DecidableEq 𝓐]
  [MeasurableSingletonClass 𝓐] (n : ℕ)
  (a : 𝓐) :
  Measurable fun h => pullCount' n h a

Code

lemma measurable_pullCount' [MeasurableSingletonClass 𝓐] (n : ℕ) (a : 𝓐) :
    Measurable (fun h : Iic n → 𝓐 × R ↦ pullCount' n h a)

Type uses (1)

pullCount'

Body uses (1)

pullCount'_eq_sum

Used by (3)

Actions: Source · Open Issue

Proof

by
  simp_rw [pullCount'_eq_sum]
  have h_meas s : Measurable (fun (h : Iic n → 𝓐 × R) ↦ if (h s).1 = a then 1 else 0) := by
    refine Measurable.ite ?_ (by fun_prop) (by fun_prop)
    exact (measurableSet_singleton _).preimage (by fun_prop)
  fun_prop

`measurable_uncurry_pullCount'`🔗

LemmaLearning.measurable_uncurry_pullCount'

Details

No docstring.

theorem

Learning.measurable_uncurry_pullCount'.{u_1, u_2} {𝓐 : Type u_1}
  {R : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {mR : MeasurableSpace R}
  [DecidableEq 𝓐] [MeasurableEq 𝓐] (n : ℕ) :
  Measurable fun p => pullCount' n (Prod.fst p) (Prod.snd p)
Learning.measurable_uncurry_pullCount'.{u_1,
    u_2}
  {𝓐 : Type u_1} {R : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐}
  {mR : MeasurableSpace R} [DecidableEq 𝓐]
  [MeasurableEq 𝓐] (n : ℕ) :
  Measurable fun p =>
    pullCount' n (Prod.fst p) (Prod.snd p)

Code

lemma measurable_uncurry_pullCount' [MeasurableEq 𝓐] (n : ℕ) :
    Measurable (fun p : (Iic n → 𝓐 × R) × 𝓐 ↦ pullCount' n p.1 p.2)

Type uses (1)

pullCount'

Body uses (1)

pullCount'_eq_sum

Used by (3)

Actions: Source · Open Issue

Proof

by
  simp_rw [pullCount'_eq_sum]
  have h_meas s : Measurable (fun h : (Iic n → 𝓐 × R) × 𝓐 ↦ if (h.1 s).1 = h.2 then 1 else 0) := by
    refine Measurable.ite ?_ (by fun_prop) (by fun_prop)
    exact measurableSet_eq_fun (by fun_prop) (by fun_prop)
  fun_prop

`adapted_pullCount_add_one`🔗

LemmaLearning.adapted_pullCount_add_one

Details

No docstring.

theorem

Learning.adapted_pullCount_add_one.{u_1, u_2, u_3} {𝓐 : Type u_1}
  {R : Type u_2} {Ω : Type u_3} {m𝓐 : MeasurableSpace 𝓐}
  {mR : MeasurableSpace R} {mΩ : MeasurableSpace Ω} [DecidableEq 𝓐]
  {A : ℕ → Ω → 𝓐} {R' : ℕ → Ω → R} [MeasurableSingletonClass 𝓐]
  (hA : ∀ (n : ℕ), Measurable (A n))
  (hR' : ∀ (n : ℕ), Measurable (R' n)) (a : 𝓐) :
  MeasureTheory.Adapted (IsAlgEnvSeq.filtration hA hR') fun n =>
    pullCount A a (n + 1)
Learning.adapted_pullCount_add_one.{u_1,
    u_2, u_3}
  {𝓐 : Type u_1} {R : Type u_2}
  {Ω : Type u_3} {m𝓐 : MeasurableSpace 𝓐}
  {mR : MeasurableSpace R}
  {mΩ : MeasurableSpace Ω} [DecidableEq 𝓐]
  {A : ℕ → Ω → 𝓐} {R' : ℕ → Ω → R}
  [MeasurableSingletonClass 𝓐]
  (hA : ∀ (n : ℕ), Measurable (A n))
  (hR' : ∀ (n : ℕ), Measurable (R' n))
  (a : 𝓐) :
  MeasureTheory.Adapted
    (IsAlgEnvSeq.filtration hA hR')
    fun n => pullCount A a (n + 1)

Code

lemma adapted_pullCount_add_one [MeasurableSingletonClass 𝓐]
    (hA : ∀ n, Measurable (A n)) (hR' : ∀ n, Measurable (R' n)) (a : 𝓐) :
    Adapted (IsAlgEnvSeq.filtration hA hR') (fun n ↦ pullCount A a (n + 1))

Type uses (2)

Body uses (5)

Used by (3)

Actions: Source · Open Issue

Proof

by
  intro n
  have : pullCount A a (n + 1) = (fun h : Iic n → 𝓐 × R ↦ pullCount' n h a) ∘
      (history A R' n) := by
    ext
    exact pullCount_add_one_eq_pullCount'
  rw [measurable_iff_comap_le]
  simp_rw [IsAlgEnvSeq.filtration, this]
  rw [← measurable_iff_comap_le]
  exact measurable_comp_comap _ (measurable_pullCount' n a)

`stronglyAdapted_pullCount_add_one`🔗

LemmaLearning.stronglyAdapted_pullCount_add_one

Details

No docstring.

theorem

Learning.stronglyAdapted_pullCount_add_one.{u_1, u_2, u_3}
  {𝓐 : Type u_1} {R : Type u_2} {Ω : Type u_3} {m𝓐 : MeasurableSpace 𝓐}
  {mR : MeasurableSpace R} {mΩ : MeasurableSpace Ω} [DecidableEq 𝓐]
  {A : ℕ → Ω → 𝓐} {R' : ℕ → Ω → R} [MeasurableSingletonClass 𝓐]
  (hA : ∀ (n : ℕ), Measurable (A n))
  (hR' : ∀ (n : ℕ), Measurable (R' n)) (a : 𝓐) :
  MeasureTheory.StronglyAdapted (IsAlgEnvSeq.filtration hA hR') fun n =>
    pullCount A a (n + 1)
Learning.stronglyAdapted_pullCount_add_one.{u_1,
    u_2, u_3}
  {𝓐 : Type u_1} {R : Type u_2}
  {Ω : Type u_3} {m𝓐 : MeasurableSpace 𝓐}
  {mR : MeasurableSpace R}
  {mΩ : MeasurableSpace Ω} [DecidableEq 𝓐]
  {A : ℕ → Ω → 𝓐} {R' : ℕ → Ω → R}
  [MeasurableSingletonClass 𝓐]
  (hA : ∀ (n : ℕ), Measurable (A n))
  (hR' : ∀ (n : ℕ), Measurable (R' n))
  (a : 𝓐) :
  MeasureTheory.StronglyAdapted
    (IsAlgEnvSeq.filtration hA hR')
    fun n => pullCount A a (n + 1)

Code

lemma stronglyAdapted_pullCount_add_one [MeasurableSingletonClass 𝓐]
    (hA : ∀ n, Measurable (A n)) (hR' : ∀ n, Measurable (R' n)) (a : 𝓐) :
    StronglyAdapted (IsAlgEnvSeq.filtration hA hR') (fun n ↦ pullCount A a (n + 1))

Type uses (2)

Body uses (1)

adapted_pullCount_add_one

Used by (1)

isPredictable_pullCount

Actions: Source · Open Issue

Proof

(adapted_pullCount_add_one hA hR' a).stronglyAdapted

`isPredictable_pullCount`🔗

LemmaLearning.isPredictable_pullCount

Details

No docstring.

theorem

Learning.isPredictable_pullCount.{u_1, u_2, u_3} {𝓐 : Type u_1}
  {R : Type u_2} {Ω : Type u_3} {m𝓐 : MeasurableSpace 𝓐}
  {mR : MeasurableSpace R} {mΩ : MeasurableSpace Ω} [DecidableEq 𝓐]
  {A : ℕ → Ω → 𝓐} {R' : ℕ → Ω → R} [MeasurableSingletonClass 𝓐]
  (hA : ∀ (n : ℕ), Measurable (A n))
  (hR' : ∀ (n : ℕ), Measurable (R' n)) (a : 𝓐) :
  MeasureTheory.IsStronglyPredictable (IsAlgEnvSeq.filtration hA hR')
    (pullCount A a)
Learning.isPredictable_pullCount.{u_1,
    u_2, u_3}
  {𝓐 : Type u_1} {R : Type u_2}
  {Ω : Type u_3} {m𝓐 : MeasurableSpace 𝓐}
  {mR : MeasurableSpace R}
  {mΩ : MeasurableSpace Ω} [DecidableEq 𝓐]
  {A : ℕ → Ω → 𝓐} {R' : ℕ → Ω → R}
  [MeasurableSingletonClass 𝓐]
  (hA : ∀ (n : ℕ), Measurable (A n))
  (hR' : ∀ (n : ℕ), Measurable (R' n))
  (a : 𝓐) :
  MeasureTheory.IsStronglyPredictable
    (IsAlgEnvSeq.filtration hA hR')
    (pullCount A a)

Code

lemma isPredictable_pullCount [MeasurableSingletonClass 𝓐]
    (hA : ∀ n, Measurable (A n)) (hR' : ∀ n, Measurable (R' n)) (a : 𝓐) :
    IsStronglyPredictable (IsAlgEnvSeq.filtration hA hR') (pullCount A a)

Type uses (2)

Body uses (2)

Used by (1)

isPredictable_empMean

Actions: Source · Open Issue

Proof

by
  rw [IsStronglyPredictable.iff_measurable_add_one]
  refine ⟨?_, stronglyAdapted_pullCount_add_one hA hR' a⟩
  simp only [pullCount_zero]
  fun_prop

`integrable_pullCount`🔗

LemmaLearning.integrable_pullCount

Details

No docstring.

theorem

Learning.integrable_pullCount.{u_1, u_3} {𝓐 : Type u_1} {Ω : Type u_3}
  {m𝓐 : MeasurableSpace 𝓐} {mΩ : MeasurableSpace Ω} [DecidableEq 𝓐]
  {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P]
  {A : ℕ → Ω → 𝓐} [MeasurableSingletonClass 𝓐]
  (hA : ∀ (n : ℕ), Measurable (A n)) (a : 𝓐) (n : ℕ) :
  MeasureTheory.Integrable (fun ω => ↑(pullCount A a n ω)) P
Learning.integrable_pullCount.{u_1, u_3}
  {𝓐 : Type u_1} {Ω : Type u_3}
  {m𝓐 : MeasurableSpace 𝓐}
  {mΩ : MeasurableSpace Ω} [DecidableEq 𝓐]
  {P : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure P]
  {A : ℕ → Ω → 𝓐}
  [MeasurableSingletonClass 𝓐]
  (hA : ∀ (n : ℕ), Measurable (A n))
  (a : 𝓐) (n : ℕ) :
  MeasureTheory.Integrable
    (fun ω => ↑(pullCount A a n ω)) P

Code

lemma integrable_pullCount [MeasurableSingletonClass 𝓐]
    (hA : ∀ n, Measurable (A n)) (a : 𝓐) (n : ℕ) :
    Integrable (fun ω ↦ (pullCount A a n ω : ℝ)) P

Type uses (1)

pullCount

Body uses (2)

Used by (2)

Actions: Source · Open Issue

Proof

by
  refine integrable_of_le_of_le (g₁ := 0) (g₂ := fun _ ↦ n) (by fun_prop)
    (ae_of_all _ fun ω ↦ by simp) (ae_of_all _ fun ω ↦ ?_) (integrable_const _) (integrable_const _)
  simp only [Nat.cast_le]
  exact pullCount_le a n ω

`stepsUntil`🔗

DefinitionLearning.stepsUntil

Details

Number of steps until action a was pulled exactly m times.

def

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

Code

noncomputable
def stepsUntil (A : ℕ → Ω → 𝓐) (a : 𝓐) (m : ℕ) (ω : Ω) : ℕ∞ :=
  sInf ((↑) '' {s | pullCount A a (s + 1) ω = m})

Body uses (1)

pullCount

Used by (46)

Actions: Source · Open Issue

`stepsUntil_eq_top_iff`🔗

LemmaLearning.stepsUntil_eq_top_iff

Details

No docstring.

theorem

Learning.stepsUntil_eq_top_iff.{u_1, u_3} {𝓐 : Type u_1} {Ω : Type u_3}
  [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} {a : 𝓐} {m : ℕ} {ω : Ω} :
  stepsUntil A a m ω = ⊤ ↔ ∀ (s : ℕ), pullCount A a (s + 1) ω ≠ m
Learning.stepsUntil_eq_top_iff.{u_1, u_3}
  {𝓐 : Type u_1} {Ω : Type u_3}
  [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} {a : 𝓐}
  {m : ℕ} {ω : Ω} :
  stepsUntil A a m ω = ⊤ ↔
    ∀ (s : ℕ), pullCount A a (s + 1) ω ≠ m

Code

lemma stepsUntil_eq_top_iff : stepsUntil A a m ω = ⊤ ↔ ∀ s, pullCount A a (s + 1) ω ≠ m

Type uses (2)

Used by (4)

Actions: Source · Open Issue

Proof

by
  simp [stepsUntil, sInf_eq_top]

`stepsUntil_ne_top`🔗

LemmaLearning.stepsUntil_ne_top

Details

No docstring.

theorem

Learning.stepsUntil_ne_top.{u_1, u_3} {𝓐 : Type u_1} {Ω : Type u_3}
  [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} {a : 𝓐} {m : ℕ} {ω : Ω}
  (h_exists : ∃ s, pullCount A a (s + 1) ω = m) : stepsUntil A a m ω ≠ ⊤
Learning.stepsUntil_ne_top.{u_1, u_3}
  {𝓐 : Type u_1} {Ω : Type u_3}
  [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} {a : 𝓐}
  {m : ℕ} {ω : Ω}
  (h_exists :
    ∃ s, pullCount A a (s + 1) ω = m) :
  stepsUntil A a m ω ≠ ⊤

Code

lemma stepsUntil_ne_top (h_exists : ∃ s, pullCount A a (s + 1) ω = m) : stepsUntil A a m ω ≠ ⊤

Type uses (2)

Body uses (1)

stepsUntil_eq_top_iff

Used by (1)

pullCount_lt_of_le_stepsUntil

Actions: Source · Open Issue

Proof

by
  simpa [stepsUntil_eq_top_iff]

`exists_pullCount_eq`🔗

LemmaLearning.exists_pullCount_eq

Details

No docstring.

theorem

Learning.exists_pullCount_eq.{u_1, u_3} {𝓐 : Type u_1} {Ω : Type u_3}
  [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} {a : 𝓐} {m : ℕ} {ω : Ω}
  (h' : stepsUntil A a m ω ≠ ⊤) : ∃ s, pullCount A a (s + 1) ω = m
Learning.exists_pullCount_eq.{u_1, u_3}
  {𝓐 : Type u_1} {Ω : Type u_3}
  [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} {a : 𝓐}
  {m : ℕ} {ω : Ω}
  (h' : stepsUntil A a m ω ≠ ⊤) :
  ∃ s, pullCount A a (s + 1) ω = m

Code

lemma exists_pullCount_eq (h' : stepsUntil A a m ω ≠ ⊤) :
    ∃ s, pullCount A a (s + 1) ω = m

Type uses (2)

Body uses (1)

stepsUntil_eq_top_iff

Used by (5)

Actions: Source · Open Issue

Proof

by
  by_contra! h_contra
  rw [← stepsUntil_eq_top_iff] at h_contra
  simp [h_contra] at h'

`stepsUntil_zero_of_ne`🔗

LemmaLearning.stepsUntil_zero_of_ne

Details

No docstring.

theorem

Learning.stepsUntil_zero_of_ne.{u_1, u_3} {𝓐 : Type u_1} {Ω : Type u_3}
  [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} {a : 𝓐} {ω : Ω} (hka : A 0 ω ≠ a) :
  stepsUntil A a 0 ω = 0
Learning.stepsUntil_zero_of_ne.{u_1, u_3}
  {𝓐 : Type u_1} {Ω : Type u_3}
  [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} {a : 𝓐}
  {ω : Ω} (hka : A 0 ω ≠ a) :
  stepsUntil A a 0 ω = 0

Code

lemma stepsUntil_zero_of_ne (hka : A 0 ω ≠ a) : stepsUntil A a 0 ω = 0

Type uses (1)

stepsUntil

Body uses (3)

Used by (3)

Actions: Source · Open Issue

Proof

by
  unfold stepsUntil
  simp_rw [← bot_eq_zero, sInf_eq_bot, bot_eq_zero]
  intro n hn
  refine ⟨0, ?_, hn⟩
  simp only [Set.mem_image, Set.mem_setOf_eq, Nat.cast_eq_zero, exists_eq_right, zero_add]
  rw [← zero_add 1, pullCount_eq_pullCount_of_action_ne hka]
  simp

`stepsUntil_zero_of_eq`🔗

LemmaLearning.stepsUntil_zero_of_eq

Details

No docstring.

theorem

Learning.stepsUntil_zero_of_eq.{u_1, u_3} {𝓐 : Type u_1} {Ω : Type u_3}
  [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} {a : 𝓐} {ω : Ω} (hka : A 0 ω = a) :
  stepsUntil A a 0 ω = ⊤
Learning.stepsUntil_zero_of_eq.{u_1, u_3}
  {𝓐 : Type u_1} {Ω : Type u_3}
  [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} {a : 𝓐}
  {ω : Ω} (hka : A 0 ω = a) :
  stepsUntil A a 0 ω = ⊤

Code

lemma stepsUntil_zero_of_eq (hka : A 0 ω = a) : stepsUntil A a 0 ω = ⊤

Type uses (1)

stepsUntil

Body uses (5)

Used by (2)

Actions: Source · Open Issue

Proof

by
  rw [stepsUntil_eq_top_iff]
  suffices 0 < pullCount A a 1 ω from fun _ ↦ (this.trans_le (monotone_pullCount _ _ (by lia))).ne'
  rw [← hka, ← zero_add 1, pullCount_action_eq_pullCount_add_one]
  simp

`stepsUntil_eq_dite`🔗

LemmaLearning.stepsUntil_eq_dite

Details

No docstring.

theorem

Learning.stepsUntil_eq_dite.{u_1, u_3} {𝓐 : Type u_1} {Ω : Type u_3}
  [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} (a : 𝓐) (m : ℕ) (ω : Ω)
  [Decidable (∃ s, pullCount A a (s + 1) ω = m)] :
  stepsUntil A a m ω =
    if h : ∃ s, pullCount A a (s + 1) ω = m then ↑(Nat.find h) else ⊤
Learning.stepsUntil_eq_dite.{u_1, u_3}
  {𝓐 : Type u_1} {Ω : Type u_3}
  [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} (a : 𝓐)
  (m : ℕ) (ω : Ω)
  [Decidable
      (∃ s,
        pullCount A a (s + 1) ω = m)] :
  stepsUntil A a m ω =
    if h :
        ∃ s,
          pullCount A a (s + 1) ω = m then
      ↑(Nat.find h)
    else ⊤

Code

lemma stepsUntil_eq_dite (a : 𝓐) (m : ℕ) (ω : Ω)
    [Decidable (∃ s, pullCount A a (s + 1) ω = m)] :
    stepsUntil A a m ω =
      if h : ∃ s, pullCount A a (s + 1) ω = m then (Nat.find h : ℕ∞) else ⊤

Type uses (2)

Used by (7)

Actions: Source · Open Issue

Proof

by
  unfold stepsUntil
  split_ifs with h'
  · refine le_antisymm ?_ ?_
    · refine sInf_le ?_
      simpa using Nat.find_spec h'
    · simp only [le_sInf_iff, Set.mem_image, Set.mem_setOf_eq, forall_exists_index, and_imp,
        forall_apply_eq_imp_iff₂, Nat.cast_le, Nat.find_le_iff]
      exact fun n hn ↦ ⟨n, le_rfl, hn⟩
  · push Not at h'
    suffices {s | pullCount A a (s + 1) ω = m} = ∅ by simp [this]
    ext s
    simpa using (h' s)

`stepsUntil_eq_leastGE`🔗

LemmaLearning.stepsUntil_eq_leastGE

Details

No docstring.

theorem

Learning.stepsUntil_eq_leastGE.{u_1, u_3} {𝓐 : Type u_1} {Ω : Type u_3}
  [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} {m : ℕ} (a : 𝓐) (hm : m ≠ 0) :
  stepsUntil A a m =
    MeasureTheory.leastGE (fun n ω => pullCount A a (n + 1) ω) m
Learning.stepsUntil_eq_leastGE.{u_1, u_3}
  {𝓐 : Type u_1} {Ω : Type u_3}
  [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} {m : ℕ}
  (a : 𝓐) (hm : m ≠ 0) :
  stepsUntil A a m =
    MeasureTheory.leastGE
      (fun n ω => pullCount A a (n + 1) ω)
      m

Code

lemma stepsUntil_eq_leastGE (a : 𝓐) (hm : m ≠ 0) :
    stepsUntil A a m = leastGE (fun n (ω : Ω) ↦ pullCount A a (n + 1) ω) m

Type uses (2)

Body uses (3)

Used by (2)

Actions: Source · Open Issue

Proof

by
  classical
  ext ω
  rw [stepsUntil_eq_dite]
  unfold leastGE hittingAfter
  simp only [Nat.bot_eq_zero, zero_le, Set.mem_Ici, true_and, ENat.some_eq_coe]
  have h_iff : (∃ s, pullCount A a (s + 1) ω = m) ↔ (∃ s, m ≤ pullCount A a (s + 1) ω) := by
    refine ⟨fun ⟨s, hs⟩ ↦ ⟨s, hs.ge⟩, fun ⟨s, hs⟩ ↦ ?_⟩
    exact exists_pullCount_eq_of_le hs hm
  by_cases h_exists : ∃ s, m ≤ pullCount A a (s + 1) ω
  swap; · simp_rw [h_iff]; simp [h_exists]
  rw [if_pos h_exists, dif_pos]
  swap; · rwa [h_iff]
  norm_cast
  rw [Nat.find_eq_iff]
  constructor
  · apply le_antisymm
    · by_contra! h_contra
      obtain ⟨s, hs⟩ : ∃ s, pullCount A a (s + 1) ω = m := exists_pullCount_eq_of_le h_contra.le hm
      rw [← hs] at h_contra
      refine h_contra.not_ge ?_
      gcongr
      exact csInf_le (by simp) (by simp)
    · exact Nat.sInf_mem (s := {j | m ≤ pullCount A a (j + 1) ω}) h_exists
  · intro n hn h_contra
    refine hn.not_ge ?_
    exact csInf_le (by simp) (by simp [h_contra])

`stepsUntil_mono`🔗

LemmaLearning.stepsUntil_mono

Details

No docstring.

theorem

Learning.stepsUntil_mono.{u_1, u_3} {𝓐 : Type u_1} {Ω : Type u_3}
  [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} (a : 𝓐) (ω : Ω) {n m : ℕ} (hn : n ≠ 0)
  (hnm : n ≤ m) : stepsUntil A a n ω ≤ stepsUntil A a m ω
Learning.stepsUntil_mono.{u_1, u_3}
  {𝓐 : Type u_1} {Ω : Type u_3}
  [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} (a : 𝓐)
  (ω : Ω) {n m : ℕ} (hn : n ≠ 0)
  (hnm : n ≤ m) :
  stepsUntil A a n ω ≤ stepsUntil A a m ω

Code

lemma stepsUntil_mono (a : 𝓐) (ω : Ω) {n m : ℕ} (hn : n ≠ 0) (hnm : n ≤ m) :
    stepsUntil A a n ω ≤ stepsUntil A a m ω

Type uses (1)

stepsUntil

Body uses (2)

Actions: Source · Open Issue

Proof

by
  rw [stepsUntil_eq_leastGE a hn, stepsUntil_eq_leastGE a (by lia)]
  simp_rw [leastGE]
  exact hittingAfter_anti (fun n ω ↦ (pullCount A a (n + 1) ω)) 0 (fun x ↦ by grind) ω

`stepsUntil_pullCount_le`🔗

LemmaLearning.stepsUntil_pullCount_le

Details

No docstring.

theorem

Learning.stepsUntil_pullCount_le.{u_1, u_3} {𝓐 : Type u_1}
  {Ω : Type u_3} [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} (ω : Ω) (a : 𝓐)
  (t : ℕ) : stepsUntil A a (pullCount A a (t + 1) ω) ω ≤ ↑t
Learning.stepsUntil_pullCount_le.{u_1,
    u_3}
  {𝓐 : Type u_1} {Ω : Type u_3}
  [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} (ω : Ω)
  (a : 𝓐) (t : ℕ) :
  stepsUntil A a (pullCount A a (t + 1) ω)
      ω ≤
    ↑t

Code

lemma stepsUntil_pullCount_le (ω : Ω) (a : 𝓐) (t : ℕ) :
    stepsUntil A a (pullCount A a (t + 1) ω) ω ≤ t

Type uses (2)

Used by (2)

Actions: Source · Open Issue

Proof

by
  rw [stepsUntil]
  exact csInf_le (OrderBot.bddBelow _) ⟨t, rfl, rfl⟩

`stepsUntil_pullCount_eq`🔗

LemmaLearning.stepsUntil_pullCount_eq

Details

No docstring.

theorem

Learning.stepsUntil_pullCount_eq.{u_1, u_3} {𝓐 : Type u_1}
  {Ω : Type u_3} [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} (ω : Ω) (t : ℕ) :
  stepsUntil A (A t ω) (pullCount A (A t ω) (t + 1) ω) ω = ↑t
Learning.stepsUntil_pullCount_eq.{u_1,
    u_3}
  {𝓐 : Type u_1} {Ω : Type u_3}
  [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} (ω : Ω)
  (t : ℕ) :
  stepsUntil A (A t ω)
      (pullCount A (A t ω) (t + 1) ω) ω =
    ↑t

Code

lemma stepsUntil_pullCount_eq (ω : Ω) (t : ℕ) :
    stepsUntil A (A t ω) (pullCount A (A t ω) (t + 1) ω) ω = t

Type uses (2)

Body uses (3)

Used by (1)

rewardByCount_pullCount_add_one_eq_reward

Actions: Source · Open Issue

Proof

by
  apply le_antisymm (stepsUntil_pullCount_le ω (A t ω) t)
  suffices ∀ t', pullCount A (A t ω) (t' + 1) ω = pullCount A (A t ω) t ω + 1 → t ≤ t' by
    simpa [stepsUntil, pullCount_action_eq_pullCount_add_one]
  exact fun t' h' ↦ Nat.le_of_lt_succ ((monotone_pullCount (A t ω) ω).reflect_lt
    (h' ▸ lt_add_one _))

`stepsUntil_one_of_eq`🔗

LemmaLearning.stepsUntil_one_of_eq

Details

If we pull action a at time 0, the first time at which it is pulled once is 0.

theorem

Learning.stepsUntil_one_of_eq.{u_1, u_3} {𝓐 : Type u_1} {Ω : Type u_3}
  [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} {a : 𝓐} {ω : Ω} (hka : A 0 ω = a) :
  stepsUntil A a 1 ω = 0
Learning.stepsUntil_one_of_eq.{u_1, u_3}
  {𝓐 : Type u_1} {Ω : Type u_3}
  [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} {a : 𝓐}
  {ω : Ω} (hka : A 0 ω = a) :
  stepsUntil A a 1 ω = 0

Code

lemma stepsUntil_one_of_eq (hka : A 0 ω = a) : stepsUntil A a 1 ω = 0

Type uses (1)

stepsUntil

Body uses (3)

Used by (1)

stepsUntil_eq_zero_iff

Actions: Source · Open Issue

Proof

by
  classical
  have h_pull : pullCount A a 1 ω = 1 := by simp [pullCount_one, hka]
  have h_le := stepsUntil_pullCount_le (A := A) ω a 0
  simpa [h_pull] using h_le

`stepsUntil_eq_zero_iff`🔗

LemmaLearning.stepsUntil_eq_zero_iff

Details

No docstring.

theorem

Learning.stepsUntil_eq_zero_iff.{u_1, u_3} {𝓐 : Type u_1} {Ω : Type u_3}
  [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} {a : 𝓐} {m : ℕ} {ω : Ω} :
  stepsUntil A a m ω = 0 ↔ m = 0 ∧ A 0 ω ≠ a ∨ m = 1 ∧ A 0 ω = a
Learning.stepsUntil_eq_zero_iff.{u_1, u_3}
  {𝓐 : Type u_1} {Ω : Type u_3}
  [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} {a : 𝓐}
  {m : ℕ} {ω : Ω} :
  stepsUntil A a m ω = 0 ↔
    m = 0 ∧ A 0 ω ≠ a ∨ m = 1 ∧ A 0 ω = a

Code

lemma stepsUntil_eq_zero_iff :
    stepsUntil A a m ω = 0 ↔ (m = 0 ∧ A 0 ω ≠ a) ∨ (m = 1 ∧ A 0 ω = a)

Type uses (1)

stepsUntil

Body uses (6)

Used by (3)

Actions: Source · Open Issue

Proof

by
  classical
  refine ⟨fun h' ↦ ?_, fun h' ↦ ?_⟩
  · have h_exists : ∃ s, pullCount A a (s + 1) ω = m := exists_pullCount_eq (by simp [h'])
    simp only [stepsUntil_eq_dite, h_exists, ↓reduceDIte, Nat.cast_eq_zero, Nat.find_eq_zero,
      zero_add] at h'
    rw [pullCount_one] at h'
    by_cases hka : A 0 ω = a <;> simp_all
  · cases h' with
  | inl h =>
    rw [h.1, stepsUntil_zero_of_ne h.2]
  | inr h =>
    rw [h.1]
    exact stepsUntil_one_of_eq h.2

`action_stepsUntil`🔗

LemmaLearning.action_stepsUntil

Details

No docstring.

theorem

Learning.action_stepsUntil.{u_1, u_3} {𝓐 : Type u_1} {Ω : Type u_3}
  [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} {a : 𝓐} {m : ℕ} {ω : Ω} (hm : m ≠ 0)
  (h_exists : ∃ s, pullCount A a (s + 1) ω = m) :
  A (ENat.toNat (stepsUntil A a m ω)) ω = a
Learning.action_stepsUntil.{u_1, u_3}
  {𝓐 : Type u_1} {Ω : Type u_3}
  [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} {a : 𝓐}
  {m : ℕ} {ω : Ω} (hm : m ≠ 0)
  (h_exists :
    ∃ s, pullCount A a (s + 1) ω = m) :
  A (ENat.toNat (stepsUntil A a m ω)) ω =
    a

Code

lemma action_stepsUntil (hm : m ≠ 0) (h_exists : ∃ s, pullCount A a (s + 1) ω = m) :
    A (stepsUntil A a m ω).toNat ω = a

Type uses (2)

Body uses (3)

Used by (1)

action_eq_of_stepsUntil_eq_coe

Actions: Source · Open Issue

Proof

by
  classical
  simp only [stepsUntil_eq_dite, h_exists, ↓reduceDIte, ENat.toNat_coe]
  have h_spec := Nat.find_spec h_exists
  have h_spec' n := Nat.find_min h_exists (m := n)
  by_cases h_zero : Nat.find h_exists = 0
  · simp only [h_zero, zero_add, not_lt_zero, IsEmpty.forall_iff, implies_true] at *
    by_contra h_ne
    rw [← zero_add 1, pullCount_eq_pullCount_of_action_ne h_ne] at h_spec
    simp only [pullCount_zero] at h_spec
    exact hm h_spec.symm
  have h_pos : 0 < Nat.find h_exists := Nat.pos_of_ne_zero h_zero
  by_contra h_ne
  refine h_spec' (Nat.find h_exists - 1) ?_ ?_
  · simp [h_pos]
  rw [Nat.sub_add_cancel (by omega)]
  rwa [← pullCount_eq_pullCount_of_action_ne]
  exact h_ne

`action_eq_of_stepsUntil_eq_coe`🔗

LemmaLearning.action_eq_of_stepsUntil_eq_coe

Details

No docstring.

theorem

Learning.action_eq_of_stepsUntil_eq_coe.{u_1, u_3} {𝓐 : Type u_1}
  {Ω : Type u_3} [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} {a : 𝓐} {m n : ℕ}
  {ω : Ω} (hm : m ≠ 0) (h : stepsUntil A a m ω = ↑n) : A n ω = a
Learning.action_eq_of_stepsUntil_eq_coe.{u_1,
    u_3}
  {𝓐 : Type u_1} {Ω : Type u_3}
  [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} {a : 𝓐}
  {m n : ℕ} {ω : Ω} (hm : m ≠ 0)
  (h : stepsUntil A a m ω = ↑n) :
  A n ω = a

Code

lemma action_eq_of_stepsUntil_eq_coe (hm : m ≠ 0) (h : stepsUntil A a m ω = n) :
    A n ω = a

Type uses (1)

stepsUntil

Body uses (3)

Used by (2)

Actions: Source · Open Issue

Proof

by
  have : n = (stepsUntil A a m ω).toNat := by simp [h]
  rw [this]
  have h_exists : ∃ s, pullCount A a (s + 1) ω = m := exists_pullCount_eq (by simp [h])
  exact action_stepsUntil hm h_exists

`pullCount_stepsUntil_add_one`🔗

LemmaLearning.pullCount_stepsUntil_add_one

Details

No docstring.

theorem

Learning.pullCount_stepsUntil_add_one.{u_1, u_3} {𝓐 : Type u_1}
  {Ω : Type u_3} [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} {a : 𝓐} {m : ℕ} {ω : Ω}
  (h_exists : ∃ s, pullCount A a (s + 1) ω = m) :
  pullCount A a (ENat.toNat (stepsUntil A a m ω + 1)) ω = m
Learning.pullCount_stepsUntil_add_one.{u_1,
    u_3}
  {𝓐 : Type u_1} {Ω : Type u_3}
  [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} {a : 𝓐}
  {m : ℕ} {ω : Ω}
  (h_exists :
    ∃ s, pullCount A a (s + 1) ω = m) :
  pullCount A a
      (ENat.toNat
        (stepsUntil A a m ω + 1))
      ω =
    m

Code

lemma pullCount_stepsUntil_add_one (h_exists : ∃ s, pullCount A a (s + 1) ω = m) :
    pullCount A a (stepsUntil A a m ω + 1).toNat ω = m

Type uses (2)

Body uses (1)

stepsUntil_eq_dite

Used by (3)

Actions: Source · Open Issue

Proof

by
  classical
  have h_eq := stepsUntil_eq_dite (A := A) a m ω
  simp only [h_exists, ↓reduceDIte] at h_eq
  have h' := Nat.find_spec h_exists
  rw [h_eq]
  rw [ENat.toNat_add (by simp) (by simp)]
  simp only [ENat.toNat_coe, ENat.toNat_one]
  exact h'

`pullCount_stepsUntil`🔗

LemmaLearning.pullCount_stepsUntil

Details

No docstring.

theorem

Learning.pullCount_stepsUntil.{u_1, u_3} {𝓐 : Type u_1} {Ω : Type u_3}
  [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} {a : 𝓐} {m : ℕ} {ω : Ω} (hm : m ≠ 0)
  (h_exists : ∃ s, pullCount A a (s + 1) ω = m) :
  pullCount A a (ENat.toNat (stepsUntil A a m ω)) ω = m - 1
Learning.pullCount_stepsUntil.{u_1, u_3}
  {𝓐 : Type u_1} {Ω : Type u_3}
  [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} {a : 𝓐}
  {m : ℕ} {ω : Ω} (hm : m ≠ 0)
  (h_exists :
    ∃ s, pullCount A a (s + 1) ω = m) :
  pullCount A a
      (ENat.toNat (stepsUntil A a m ω))
      ω =
    m - 1

Code

lemma pullCount_stepsUntil (hm : m ≠ 0) (h_exists : ∃ s, pullCount A a (s + 1) ω = m) :
    pullCount A a (stepsUntil A a m ω).toNat ω = m - 1

Type uses (2)

Body uses (4)

Used by (1)

pullCount_eq_of_stepsUntil_eq_coe

Actions: Source · Open Issue

Proof

by
  have h_action := action_eq_of_stepsUntil_eq_coe (A := A) (n := (stepsUntil A a m ω).toNat)
    (a := a) (ω := ω) hm ?_
  swap; · symm; simpa [stepsUntil_eq_top_iff]
  have h_add_one := pullCount_stepsUntil_add_one h_exists
  nth_rw 1 [← h_action] at h_add_one
  rw [ENat.toNat_add ?_ (by simp), ENat.toNat_one, pullCount_action_eq_pullCount_add_one]
    at h_add_one
  swap; · simpa [stepsUntil_eq_top_iff]
  grind

`pullCount_lt_of_le_stepsUntil`🔗

LemmaLearning.pullCount_lt_of_le_stepsUntil

Details

No docstring.

theorem

Learning.pullCount_lt_of_le_stepsUntil.{u_1, u_3} {𝓐 : Type u_1}
  {Ω : Type u_3} [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} (a : 𝓐) {n m : ℕ}
  (ω : Ω) (h_exists : ∃ s, pullCount A a (s + 1) ω = m)
  (hn : ↑n < stepsUntil A a m ω) : pullCount A a (n + 1) ω < m
Learning.pullCount_lt_of_le_stepsUntil.{u_1,
    u_3}
  {𝓐 : Type u_1} {Ω : Type u_3}
  [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} (a : 𝓐)
  {n m : ℕ} (ω : Ω)
  (h_exists :
    ∃ s, pullCount A a (s + 1) ω = m)
  (hn : ↑n < stepsUntil A a m ω) :
  pullCount A a (n + 1) ω < m

Code

lemma pullCount_lt_of_le_stepsUntil (a : 𝓐) {n m : ℕ} (ω : Ω)
    (h_exists : ∃ s, pullCount A a (s + 1) ω = m) (hn : n < stepsUntil A a m ω) :
    pullCount A a (n + 1) ω < m

Type uses (2)

Body uses (4)

Used by (1)

stepsUntil_eq_iff

Actions: Source · Open Issue

Proof

by
  classical
  have h_eq := stepsUntil_eq_dite (A := A) a m ω
  simp only [h_exists, ↓reduceDIte] at h_eq
  rw [← ENat.coe_toNat (stepsUntil_ne_top h_exists)] at hn
  refine lt_of_le_of_ne ?_ ?_
  · calc pullCount A a (n + 1) ω
    _ ≤ pullCount A a (stepsUntil A a m ω + 1).toNat ω := by
      refine monotone_pullCount a ω ?_
      rw [ENat.toNat_add (stepsUntil_ne_top h_exists) (by simp)]
      simp only [ENat.toNat_one, add_le_add_iff_right]
      exact mod_cast hn.le
    _ = m := pullCount_stepsUntil_add_one h_exists
  · refine Nat.find_min h_exists (m := n) ?_
    suffices n < (stepsUntil A a m ω).toNat by
      rwa [h_eq, ENat.toNat_coe] at this
    exact mod_cast hn

`pullCount_eq_of_stepsUntil_eq_coe`🔗

LemmaLearning.pullCount_eq_of_stepsUntil_eq_coe

Details

No docstring.

theorem

Learning.pullCount_eq_of_stepsUntil_eq_coe.{u_1, u_3} {𝓐 : Type u_1}
  {Ω : Type u_3} [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} {a : 𝓐} {m n : ℕ}
  {ω : Ω} (hm : m ≠ 0) (h : stepsUntil A a m ω = ↑n) :
  pullCount A a n ω = m - 1
Learning.pullCount_eq_of_stepsUntil_eq_coe.{u_1,
    u_3}
  {𝓐 : Type u_1} {Ω : Type u_3}
  [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} {a : 𝓐}
  {m n : ℕ} {ω : Ω} (hm : m ≠ 0)
  (h : stepsUntil A a m ω = ↑n) :
  pullCount A a n ω = m - 1

Code

lemma pullCount_eq_of_stepsUntil_eq_coe {ω : Ω} (hm : m ≠ 0)
    (h : stepsUntil A a m ω = n) :
    pullCount A a n ω = m - 1

Type uses (2)

Body uses (2)

Actions: Source · Open Issue

Proof

by
  have : n = (stepsUntil A a m ω).toNat := by simp [h]
  rw [this, pullCount_stepsUntil hm]
  exact exists_pullCount_eq (by simp [h])

`pullCount_add_one_eq_of_stepsUntil_eq_coe`🔗

LemmaLearning.pullCount_add_one_eq_of_stepsUntil_eq_coe

Details

No docstring.

theorem

Learning.pullCount_add_one_eq_of_stepsUntil_eq_coe.{u_1, u_3}
  {𝓐 : Type u_1} {Ω : Type u_3} [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} {a : 𝓐}
  {m n : ℕ} {ω : Ω} (h : stepsUntil A a m ω = ↑n) :
  pullCount A a (n + 1) ω = m
Learning.pullCount_add_one_eq_of_stepsUntil_eq_coe.{u_1,
    u_3}
  {𝓐 : Type u_1} {Ω : Type u_3}
  [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} {a : 𝓐}
  {m n : ℕ} {ω : Ω}
  (h : stepsUntil A a m ω = ↑n) :
  pullCount A a (n + 1) ω = m

Code

lemma pullCount_add_one_eq_of_stepsUntil_eq_coe {ω : Ω}
    (h : stepsUntil A a m ω = n) :
    pullCount A a (n + 1) ω = m

Type uses (2)

Body uses (2)

Used by (1)

stepsUntil_eq_iff

Actions: Source · Open Issue

Proof

by
  have : n + 1 = (stepsUntil A a m ω + 1).toNat := by
    rw [ENat.toNat_add (by simp [h]) (by simp)]; simp [h]
  rw [this, pullCount_stepsUntil_add_one]
  exact exists_pullCount_eq (by simp [h])

`stepsUntil_eq_iff`🔗

LemmaLearning.stepsUntil_eq_iff

Details

No docstring.

theorem

Learning.stepsUntil_eq_iff.{u_1, u_3} {𝓐 : Type u_1} {Ω : Type u_3}
  [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} {a : 𝓐} {m : ℕ} {ω : Ω} (n : ℕ) :
  stepsUntil A a m ω = ↑n ↔
    pullCount A a (n + 1) ω = m ∧ ∀ k < n, pullCount A a (k + 1) ω < m
Learning.stepsUntil_eq_iff.{u_1, u_3}
  {𝓐 : Type u_1} {Ω : Type u_3}
  [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} {a : 𝓐}
  {m : ℕ} {ω : Ω} (n : ℕ) :
  stepsUntil A a m ω = ↑n ↔
    pullCount A a (n + 1) ω = m ∧
      ∀ k < n, pullCount A a (k + 1) ω < m

Code

lemma stepsUntil_eq_iff {ω : Ω} (n : ℕ) :
    stepsUntil A a m ω = n ↔
      pullCount A a (n + 1) ω = m ∧ (∀ k < n, pullCount A a (k + 1) ω < m)

Type uses (2)

Body uses (4)

Used by (2)

Actions: Source · Open Issue

Proof

by
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · have h_exists : ∃ s, pullCount A a (s + 1) ω = m := exists_pullCount_eq (by simp [h])
    refine ⟨pullCount_add_one_eq_of_stepsUntil_eq_coe h, fun k hk ↦ ?_⟩
    exact pullCount_lt_of_le_stepsUntil a ω h_exists (by rw [h]; exact mod_cast hk)
  · classical
    rw [stepsUntil_eq_dite a m ω, dif_pos ⟨n, h.1⟩]
    simp only [Nat.cast_inj]
    rw [Nat.find_eq_iff]
    exact ⟨h.1, fun k hk ↦ (h.2 k hk).ne⟩

`stepsUntil_eq_iff'`🔗

LemmaLearning.stepsUntil_eq_iff'

Details

No docstring.

theorem

Learning.stepsUntil_eq_iff'.{u_1, u_3} {𝓐 : Type u_1} {Ω : Type u_3}
  [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} {a : 𝓐} {m : ℕ} {ω : Ω} (hm : m ≠ 0)
  (n : ℕ) :
  stepsUntil A a m ω = ↑n ↔ A n ω = a ∧ pullCount A a n ω = m - 1
Learning.stepsUntil_eq_iff'.{u_1, u_3}
  {𝓐 : Type u_1} {Ω : Type u_3}
  [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} {a : 𝓐}
  {m : ℕ} {ω : Ω} (hm : m ≠ 0) (n : ℕ) :
  stepsUntil A a m ω = ↑n ↔
    A n ω = a ∧ pullCount A a n ω = m - 1

Code

lemma stepsUntil_eq_iff' {ω : Ω} (hm : m ≠ 0) (n : ℕ) :
    stepsUntil A a m ω = n ↔ A n ω = a ∧ pullCount A a n ω = m - 1

Type uses (2)

Body uses (5)

Used by (1)

measurable_comap_indicator_stepsUntil_eq

Actions: Source · Open Issue

Proof

by
  by_cases hn : n = 0
  · simp [hn, stepsUntil_eq_zero_iff, hm]
    grind
  rw [stepsUntil_eq_iff n]
  refine ⟨fun ⟨h1, h2⟩ ↦ ⟨?_, ?_⟩, fun ⟨h1, h2⟩ ↦ ⟨?_, fun k hk ↦ ?_⟩⟩
  · rw [pullCount_add_one] at h1
    specialize h2 (n - 1) (by lia)
    grind
  · rw [pullCount_add_one] at h1
    specialize h2 (n - 1) (by lia)
    grind
  · rw [pullCount_add_one, h1, h2]
    grind
  · rw [Nat.lt_iff_le_pred (by grind)]
    rw [← h2]
    refine monotone_pullCount a ω ?_
    grind

`stepsUntil_eq_congr`🔗

LemmaLearning.stepsUntil_eq_congr

Details

No docstring.

theorem

Learning.stepsUntil_eq_congr.{u_1, u_3} {𝓐 : Type u_1} {Ω : Type u_3}
  [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} {a : 𝓐} {m n : ℕ} {ω ω' : Ω}
  (h_eq : ∀ i ≤ n, A i ω = A i ω') :
  stepsUntil A a m ω = ↑n ↔ stepsUntil A a m ω' = ↑n
Learning.stepsUntil_eq_congr.{u_1, u_3}
  {𝓐 : Type u_1} {Ω : Type u_3}
  [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} {a : 𝓐}
  {m n : ℕ} {ω ω' : Ω}
  (h_eq : ∀ i ≤ n, A i ω = A i ω') :
  stepsUntil A a m ω = ↑n ↔
    stepsUntil A a m ω' = ↑n

Code

lemma stepsUntil_eq_congr {ω' : Ω} (h_eq : ∀ i ≤ n, A i ω = A i ω') :
    stepsUntil A a m ω = n ↔ stepsUntil A a m ω' = n

Type uses (1)

stepsUntil

Body uses (3)

Actions: Source · Open Issue

Proof

by
  simp_rw [stepsUntil_eq_iff n]
  congr! 1
  · rw [pullCount_congr h_eq]
  · congr! 3 with k hk
    rw [pullCount_congr]
    grind

`isStoppingTime_stepsUntil`🔗

LemmaLearning.isStoppingTime_stepsUntil

Details

No docstring.

theorem

Learning.isStoppingTime_stepsUntil.{u_1, u_2, u_3} {𝓐 : Type u_1}
  {R : Type u_2} {Ω : Type u_3} {m𝓐 : MeasurableSpace 𝓐}
  {mR : MeasurableSpace R} {mΩ : MeasurableSpace Ω} [DecidableEq 𝓐]
  {A : ℕ → Ω → 𝓐} {R' : ℕ → Ω → R} {m : ℕ} [MeasurableSingletonClass 𝓐]
  (hA : ∀ (n : ℕ), Measurable (A n))
  (hR' : ∀ (n : ℕ), Measurable (R' n)) (a : 𝓐) (hm : m ≠ 0) :
  MeasureTheory.IsStoppingTime (IsAlgEnvSeq.filtration hA hR')
    (stepsUntil A a m)
Learning.isStoppingTime_stepsUntil.{u_1,
    u_2, u_3}
  {𝓐 : Type u_1} {R : Type u_2}
  {Ω : Type u_3} {m𝓐 : MeasurableSpace 𝓐}
  {mR : MeasurableSpace R}
  {mΩ : MeasurableSpace Ω} [DecidableEq 𝓐]
  {A : ℕ → Ω → 𝓐} {R' : ℕ → Ω → R} {m : ℕ}
  [MeasurableSingletonClass 𝓐]
  (hA : ∀ (n : ℕ), Measurable (A n))
  (hR' : ∀ (n : ℕ), Measurable (R' n))
  (a : 𝓐) (hm : m ≠ 0) :
  MeasureTheory.IsStoppingTime
    (IsAlgEnvSeq.filtration hA hR')
    (stepsUntil A a m)

Code

lemma isStoppingTime_stepsUntil [MeasurableSingletonClass 𝓐]
    (hA : ∀ n, Measurable (A n)) (hR' : ∀ n, Measurable (R' n)) (a : 𝓐) (hm : m ≠ 0) :
    IsStoppingTime (IsAlgEnvSeq.filtration hA hR') (stepsUntil A a m)

Type uses (2)

Body uses (3)

Actions: Source · Open Issue

Proof

by
  rw [stepsUntil_eq_leastGE _ hm]
  refine StronglyAdapted.isStoppingTime_leastGE _ fun n ↦ ?_
  suffices StronglyMeasurable[IsAlgEnvSeq.filtration hA hR' n] (pullCount A a (n + 1)) by
    fun_prop
  refine Measurable.stronglyMeasurable ?_
  exact adapted_pullCount_add_one hA hR' a n

`measurable_stepsUntil`🔗

LemmaLearning.measurable_stepsUntil

Details

No docstring.

theorem

Learning.measurable_stepsUntil.{u_1, u_3} {𝓐 : Type u_1} {Ω : Type u_3}
  {m𝓐 : MeasurableSpace 𝓐} {mΩ : MeasurableSpace Ω} [DecidableEq 𝓐]
  {A : ℕ → Ω → 𝓐} [MeasurableSingletonClass 𝓐]
  (hA : ∀ (n : ℕ), Measurable (A n)) (a : 𝓐) (m : ℕ) :
  Measurable (stepsUntil A a m)
Learning.measurable_stepsUntil.{u_1, u_3}
  {𝓐 : Type u_1} {Ω : Type u_3}
  {m𝓐 : MeasurableSpace 𝓐}
  {mΩ : MeasurableSpace Ω} [DecidableEq 𝓐]
  {A : ℕ → Ω → 𝓐}
  [MeasurableSingletonClass 𝓐]
  (hA : ∀ (n : ℕ), Measurable (A n))
  (a : 𝓐) (m : ℕ) :
  Measurable (stepsUntil A a m)

Code

lemma measurable_stepsUntil [MeasurableSingletonClass 𝓐]
    (hA : ∀ n, Measurable (A n)) (a : 𝓐) (m : ℕ) :
    Measurable (stepsUntil A a m)

Type uses (1)

stepsUntil

Body uses (4)

Used by (4)

Actions: Source · Open Issue

Proof

by
  classical
  have h_union : {h' : Ω | ∃ s, pullCount A a (s + 1) h' = m}
      = ⋃ s : ℕ, {h' | pullCount A a (s + 1) h' = m} := by ext; simp
  have h_meas_set : MeasurableSet {h' : Ω | ∃ s, pullCount A a (s + 1) h' = m} := by
    rw [h_union]
    refine MeasurableSet.iUnion fun s ↦ (measurableSet_singleton _).preimage ?_
    exact measurable_pullCount hA a (s + 1)
  suffices Measurable fun k ↦ if h : k ∈ {k' | ∃ s, pullCount A a (s + 1) k' = m}
      then (Nat.find h : ℕ∞) else ⊤ by
    convert this with ω
    rw [stepsUntil_eq_dite a m ω]
    rfl
  refine Measurable.dite (s := {k' : Ω | ∃ s, pullCount A a (s + 1) k' = m})
    (f := fun x ↦ (Nat.find x.2 : ℕ∞)) (g := fun _ ↦ ⊤) ?_ (by fun_prop) h_meas_set
  refine Measurable.coe_nat_enat ?_
  refine measurable_find _ fun k ↦ ?_
  suffices MeasurableSet {x : Ω | pullCount A a (k + 1) x = m} by
    have : Subtype.val '' {x : {k' : Ω |
          ∃ s, pullCount A a (s + 1) k' = m} | pullCount A a (k + 1) (x : Ω) = m}
        = {x : Ω | pullCount A a (k + 1) x = m} := by
      ext x
      simp only [Set.mem_setOf_eq, Set.coe_setOf, Set.mem_image, Subtype.exists, exists_and_left,
        exists_prop, exists_eq_right_right, and_iff_left_iff_imp]
      exact fun h ↦ ⟨_, h⟩
    refine (MeasurableEmbedding.subtype_coe h_meas_set).measurableSet_image.mp ?_
    rw [this]
    exact (measurableSet_singleton _).preimage (by fun_prop)
  exact (measurableSet_singleton _).preimage (by fun_prop)

`measurable_stepsUntil'`🔗

LemmaLearning.measurable_stepsUntil'

Details

No docstring.

theorem

Learning.measurable_stepsUntil'.{u_1, u_2, u_3} {𝓐 : Type u_1}
  {R : Type u_2} {Ω : Type u_3} {m𝓐 : MeasurableSpace 𝓐}
  {mR : MeasurableSpace R} {mΩ : MeasurableSpace Ω} [DecidableEq 𝓐]
  {A : ℕ → Ω → 𝓐} [MeasurableSingletonClass 𝓐]
  (hA : ∀ (n : ℕ), Measurable (A n)) (a : 𝓐) (m : ℕ) :
  Measurable fun ω => stepsUntil A a m (Prod.fst ω)
Learning.measurable_stepsUntil'.{u_1, u_2,
    u_3}
  {𝓐 : Type u_1} {R : Type u_2}
  {Ω : Type u_3} {m𝓐 : MeasurableSpace 𝓐}
  {mR : MeasurableSpace R}
  {mΩ : MeasurableSpace Ω} [DecidableEq 𝓐]
  {A : ℕ → Ω → 𝓐}
  [MeasurableSingletonClass 𝓐]
  (hA : ∀ (n : ℕ), Measurable (A n))
  (a : 𝓐) (m : ℕ) :
  Measurable fun ω =>
    stepsUntil A a m (Prod.fst ω)

Code

lemma measurable_stepsUntil' [MeasurableSingletonClass 𝓐]
    (hA : ∀ n, Measurable (A n)) (a : 𝓐) (m : ℕ) :
    Measurable (fun ω : Ω × (ℕ → 𝓐 → R) ↦ stepsUntil A a m ω.1)

Type uses (1)

stepsUntil

Body uses (1)

measurable_stepsUntil

Used by (1)

measurable_rewardByCount

Actions: Source · Open Issue

Proof

(measurable_stepsUntil hA a m).comp measurable_fst

`measurable_comap_indicator_stepsUntil_eq`🔗

LemmaLearning.measurable_comap_indicator_stepsUntil_eq

Details

No docstring.

theorem

Learning.measurable_comap_indicator_stepsUntil_eq.{u_1, u_2, u_3}
  {𝓐 : Type u_1} {R : Type u_2} {Ω : Type u_3} {m𝓐 : MeasurableSpace 𝓐}
  {mR : MeasurableSpace R} {mΩ : MeasurableSpace Ω} [DecidableEq 𝓐]
  {A : ℕ → Ω → 𝓐} {R' : ℕ → Ω → R} [MeasurableSingletonClass 𝓐]
  (hA : ∀ (n : ℕ), Measurable (A n))
  (hR' : ∀ (n : ℕ), Measurable (R' n)) (a : 𝓐) (m n : ℕ) :
  Measurable (Set.indicator {ω | stepsUntil A a m ω = ↑n} fun x => 1)
Learning.measurable_comap_indicator_stepsUntil_eq.{u_1,
    u_2, u_3}
  {𝓐 : Type u_1} {R : Type u_2}
  {Ω : Type u_3} {m𝓐 : MeasurableSpace 𝓐}
  {mR : MeasurableSpace R}
  {mΩ : MeasurableSpace Ω} [DecidableEq 𝓐]
  {A : ℕ → Ω → 𝓐} {R' : ℕ → Ω → R}
  [MeasurableSingletonClass 𝓐]
  (hA : ∀ (n : ℕ), Measurable (A n))
  (hR' : ∀ (n : ℕ), Measurable (R' n))
  (a : 𝓐) (m n : ℕ) :
  Measurable
    (Set.indicator
      {ω | stepsUntil A a m ω = ↑n}
      fun x => 1)

Code

lemma measurable_comap_indicator_stepsUntil_eq [MeasurableSingletonClass 𝓐]
    (hA : ∀ n, Measurable (A n)) (hR' : ∀ n, Measurable (R' n)) (a : 𝓐) (m n : ℕ) :
    Measurable[MeasurableSpace.comap
        (fun ω : Ω ↦ (history A R' (n-1) ω, A n ω)) inferInstance]
      ({ω | stepsUntil A a m ω = ↑n}.indicator fun _ ↦ 1)

Type uses (2)

Body uses (8)

Used by (3)

Actions: Source · Open Issue

Proof

by
  by_cases hm : m = 0
  · simp only [hm]
    by_cases hn : n = 0
    · subst hn
      simp only [CharP.cast_eq_zero, stepsUntil_eq_zero_iff, ne_eq, true_and, zero_ne_one,
        false_and, or_false]
      refine Measurable.indicator measurable_const ?_
      refine (measurableSet_singleton _).compl.preimage ?_
      rw [measurable_iff_comap_le, Prod.instMeasurableSpace, MeasurableSpace.comap_prodMk]
      exact le_sup_of_le_right le_rfl
    · have : {ω | stepsUntil A a 0 ω = n} = ∅ := by
        ext ω
        by_cases ha : A 0 ω = a
        · simp [stepsUntil_zero_of_eq ha]
        · simp only [Set.mem_setOf_eq, stepsUntil_zero_of_ne ha, Set.mem_empty_iff_false,
            iff_false]
          norm_cast
          exact Ne.symm hn
      simp [this]
  simp_rw [stepsUntil_eq_iff' hm]
  refine Measurable.indicator measurable_const ?_
  refine ((measurableSet_singleton _).preimage ?_).inter ((measurableSet_singleton _).preimage ?_)
  · rw [measurable_iff_comap_le, Prod.instMeasurableSpace, MeasurableSpace.comap_prodMk]
    exact le_sup_of_le_right le_rfl
  · rw [measurable_iff_comap_le, Prod.instMeasurableSpace, MeasurableSpace.comap_prodMk]
    refine le_sup_of_le_left ?_
    rw [← measurable_iff_comap_le]
    by_cases hn : n = 0
    · simp only [hn, pullCount_zero]
      exact measurable_const
    have h_meas := adapted_pullCount_add_one hA hR' a (n - 1)
    have : 1 ≤ n := by grind
    convert h_meas using 1
    · rfl
    · simp [Nat.sub_add_cancel this]

`measurable_indicator_stepsUntil_eq`🔗

LemmaLearning.measurable_indicator_stepsUntil_eq

Details

No docstring.

theorem

Learning.measurable_indicator_stepsUntil_eq.{u_1, u_2, u_3}
  {𝓐 : Type u_1} {R : Type u_2} {Ω : Type u_3} {m𝓐 : MeasurableSpace 𝓐}
  {mR : MeasurableSpace R} {mΩ : MeasurableSpace Ω} [DecidableEq 𝓐]
  {A : ℕ → Ω → 𝓐} {R' : ℕ → Ω → R} [MeasurableSingletonClass 𝓐]
  (hA : ∀ (n : ℕ), Measurable (A n))
  (hR' : ∀ (n : ℕ), Measurable (R' n)) (a : 𝓐) (m n : ℕ) :
  Measurable (Set.indicator {ω | stepsUntil A a m ω = ↑n} fun x => 1)
Learning.measurable_indicator_stepsUntil_eq.{u_1,
    u_2, u_3}
  {𝓐 : Type u_1} {R : Type u_2}
  {Ω : Type u_3} {m𝓐 : MeasurableSpace 𝓐}
  {mR : MeasurableSpace R}
  {mΩ : MeasurableSpace Ω} [DecidableEq 𝓐]
  {A : ℕ → Ω → 𝓐} {R' : ℕ → Ω → R}
  [MeasurableSingletonClass 𝓐]
  (hA : ∀ (n : ℕ), Measurable (A n))
  (hR' : ∀ (n : ℕ), Measurable (R' n))
  (a : 𝓐) (m n : ℕ) :
  Measurable
    (Set.indicator
      {ω | stepsUntil A a m ω = ↑n}
      fun x => 1)

Code

lemma measurable_indicator_stepsUntil_eq [MeasurableSingletonClass 𝓐]
    (hA : ∀ n, Measurable (A n)) (hR' : ∀ n, Measurable (R' n)) (a : 𝓐) (m n : ℕ) :
    Measurable ({ω : Ω | stepsUntil A a m ω = ↑n}.indicator fun _ ↦ 1)

Type uses (1)

stepsUntil

Body uses (3)

Used by (1)

condIndepFun_reward_stepsUntil_action

Actions: Source · Open Issue

Proof

by
  refine (measurable_comap_indicator_stepsUntil_eq hA hR' a m n).mono ?_ le_rfl
  refine Measurable.comap_le ?_
  fun_prop

`measurableSet_stepsUntil_eq_zero`🔗

LemmaLearning.measurableSet_stepsUntil_eq_zero

Details

No docstring.

theorem

Learning.measurableSet_stepsUntil_eq_zero.{u_1, u_3} {𝓐 : Type u_1}
  {Ω : Type u_3} {m𝓐 : MeasurableSpace 𝓐} [DecidableEq 𝓐]
  {A : ℕ → Ω → 𝓐} [MeasurableSingletonClass 𝓐] (a : 𝓐) (m : ℕ) :
  MeasurableSet {ω | stepsUntil A a m ω = 0}
Learning.measurableSet_stepsUntil_eq_zero.{u_1,
    u_3}
  {𝓐 : Type u_1} {Ω : Type u_3}
  {m𝓐 : MeasurableSpace 𝓐} [DecidableEq 𝓐]
  {A : ℕ → Ω → 𝓐}
  [MeasurableSingletonClass 𝓐] (a : 𝓐)
  (m : ℕ) :
  MeasurableSet
    {ω | stepsUntil A a m ω = 0}

Code

lemma measurableSet_stepsUntil_eq_zero [MeasurableSingletonClass 𝓐] (a : 𝓐) (m : ℕ) :
    MeasurableSet[MeasurableSpace.comap (A 0) inferInstance]
      {ω : Ω | stepsUntil A a m ω = 0}

Type uses (1)

stepsUntil

Body uses (1)

stepsUntil_eq_zero_iff

Used by (2)

Actions: Source · Open Issue

Proof

by
  simp only [stepsUntil_eq_zero_iff (a := a) (m := m), ne_eq]
  by_cases hm : m = 0
  · simp only [hm, true_and, zero_ne_one, false_and, or_false]
    refine (measurableSet_singleton _).compl.preimage ?_
    rw [measurable_iff_comap_le]
  by_cases hm1 : m = 1
  swap; · simp [hm, hm1]
  simp only [hm1, one_ne_zero, false_and, true_and, false_or]
  refine (measurableSet_singleton _).preimage ?_
  rw [measurable_iff_comap_le]

`measurable_comap_indicator_stepsUntil_eq_zero`🔗

LemmaLearning.measurable_comap_indicator_stepsUntil_eq_zero

Details

No docstring.

theorem

Learning.measurable_comap_indicator_stepsUntil_eq_zero.{u_1, u_3}
  {𝓐 : Type u_1} {Ω : Type u_3} {m𝓐 : MeasurableSpace 𝓐} [DecidableEq 𝓐]
  {A : ℕ → Ω → 𝓐} [MeasurableSingletonClass 𝓐] (a : 𝓐) (m : ℕ) :
  Measurable (Set.indicator {ω | stepsUntil A a m ω = 0} fun x => 1)
Learning.measurable_comap_indicator_stepsUntil_eq_zero.{u_1,
    u_3}
  {𝓐 : Type u_1} {Ω : Type u_3}
  {m𝓐 : MeasurableSpace 𝓐} [DecidableEq 𝓐]
  {A : ℕ → Ω → 𝓐}
  [MeasurableSingletonClass 𝓐] (a : 𝓐)
  (m : ℕ) :
  Measurable
    (Set.indicator
      {ω | stepsUntil A a m ω = 0}
      fun x => 1)

Code

lemma measurable_comap_indicator_stepsUntil_eq_zero [MeasurableSingletonClass 𝓐] (a : 𝓐) (m : ℕ) :
    Measurable[MeasurableSpace.comap (A 0) inferInstance]
      ({ω | stepsUntil A a m ω = 0}.indicator fun _ ↦ 1)

Type uses (1)

stepsUntil

Body uses (1)

measurableSet_stepsUntil_eq_zero

Used by (1)

condIndepFun_reward_stepsUntil_action'

Actions: Source · Open Issue

Proof

by
  rw [measurable_indicator_const_iff]
  exact measurableSet_stepsUntil_eq_zero a m

`measurableSet_stepsUntil_eq`🔗

LemmaLearning.measurableSet_stepsUntil_eq

Details

No docstring.

theorem

Learning.measurableSet_stepsUntil_eq.{u_1, u_2, u_3} {𝓐 : Type u_1}
  {R : Type u_2} {Ω : Type u_3} {m𝓐 : MeasurableSpace 𝓐}
  {mR : MeasurableSpace R} {mΩ : MeasurableSpace Ω} [DecidableEq 𝓐]
  {A : ℕ → Ω → 𝓐} {R' : ℕ → Ω → R} [MeasurableSingletonClass 𝓐]
  (hA : ∀ (n : ℕ), Measurable (A n))
  (hR' : ∀ (n : ℕ), Measurable (R' n)) (a : 𝓐) (m n : ℕ) :
  MeasurableSet {ω | stepsUntil A a m ω = ↑n}
Learning.measurableSet_stepsUntil_eq.{u_1,
    u_2, u_3}
  {𝓐 : Type u_1} {R : Type u_2}
  {Ω : Type u_3} {m𝓐 : MeasurableSpace 𝓐}
  {mR : MeasurableSpace R}
  {mΩ : MeasurableSpace Ω} [DecidableEq 𝓐]
  {A : ℕ → Ω → 𝓐} {R' : ℕ → Ω → R}
  [MeasurableSingletonClass 𝓐]
  (hA : ∀ (n : ℕ), Measurable (A n))
  (hR' : ∀ (n : ℕ), Measurable (R' n))
  (a : 𝓐) (m n : ℕ) :
  MeasurableSet
    {ω | stepsUntil A a m ω = ↑n}

Code

lemma measurableSet_stepsUntil_eq [MeasurableSingletonClass 𝓐]
    (hA : ∀ n, Measurable (A n)) (hR' : ∀ n, Measurable (R' n)) (a : 𝓐) (m n : ℕ) :
    MeasurableSet[MeasurableSpace.comap (fun ω : Ω ↦ (history A R' (n-1) ω, A n ω))
        inferInstance]
      {ω : Ω | stepsUntil A a m ω = ↑n}

Type uses (2)

Body uses (1)

measurable_comap_indicator_stepsUntil_eq

Used by (1)

isStoppingTime_stepsUntil_filtrationAction

Actions: Source · Open Issue

Proof

by
  let mProd := MeasurableSpace.comap
    (fun ω : Ω ↦ (history A R' (n-1) ω, A n ω)) inferInstance
  suffices Measurable[mProd] ({ω | stepsUntil A a m ω = ↑n}.indicator fun x ↦ 1) by
    rwa [measurable_indicator_const_iff] at this
  exact measurable_comap_indicator_stepsUntil_eq hA hR' a m n

`isStoppingTime_stepsUntil_filtrationAction`🔗

LemmaLearning.isStoppingTime_stepsUntil_filtrationAction

Details

stepsUntil a m is a stopping time with respect to the filtration filtrationAction.

theorem

Learning.isStoppingTime_stepsUntil_filtrationAction.{u_1, u_2, u_3}
  {𝓐 : Type u_1} {R : Type u_2} {Ω : Type u_3} {m𝓐 : MeasurableSpace 𝓐}
  {mR : MeasurableSpace R} {mΩ : MeasurableSpace Ω} [DecidableEq 𝓐]
  {A : ℕ → Ω → 𝓐} {R' : ℕ → Ω → R} [MeasurableSingletonClass 𝓐]
  (hA : ∀ (n : ℕ), Measurable (A n))
  (hR' : ∀ (n : ℕ), Measurable (R' n)) (a : 𝓐) (m : ℕ) :
  MeasureTheory.IsStoppingTime (IsAlgEnvSeq.filtrationAction hA hR')
    (stepsUntil A a m)
Learning.isStoppingTime_stepsUntil_filtrationAction.{u_1,
    u_2, u_3}
  {𝓐 : Type u_1} {R : Type u_2}
  {Ω : Type u_3} {m𝓐 : MeasurableSpace 𝓐}
  {mR : MeasurableSpace R}
  {mΩ : MeasurableSpace Ω} [DecidableEq 𝓐]
  {A : ℕ → Ω → 𝓐} {R' : ℕ → Ω → R}
  [MeasurableSingletonClass 𝓐]
  (hA : ∀ (n : ℕ), Measurable (A n))
  (hR' : ∀ (n : ℕ), Measurable (R' n))
  (a : 𝓐) (m : ℕ) :
  MeasureTheory.IsStoppingTime
    (IsAlgEnvSeq.filtrationAction hA hR')
    (stepsUntil A a m)

Code

lemma isStoppingTime_stepsUntil_filtrationAction [MeasurableSingletonClass 𝓐]
    (hA : ∀ n, Measurable (A n)) (hR' : ∀ n, Measurable (R' n)) (a : 𝓐) (m : ℕ) :
    IsStoppingTime (IsAlgEnvSeq.filtrationAction hA hR') (stepsUntil A a m)

Type uses (2)

Body uses (4)

Actions: Source · Open Issue

Proof

by
  refine isStoppingTime_of_measurableSet_eq fun n ↦ ?_
  by_cases hn : n = 0
  · subst hn
    simp only [WithTop.coe_zero]
    exact measurableSet_stepsUntil_eq_zero a m
  · rw [IsAlgEnvSeq.filtrationAction_eq_comap _ hn]
    exact measurableSet_stepsUntil_eq hA hR' a m n

`rewardByCount`🔗

DefinitionLearning.rewardByCount

Details

Reward obtained when pulling action a for the m-th time. If it is never pulled m times, the reward is given by the second component of ω, which in applications will be indepedent with same law.

def

Learning.rewardByCount.{u_1, u_2, u_3} {𝓐 : Type u_1} {R : Type u_2}
  {Ω : Type u_3} [DecidableEq 𝓐] (A : ℕ → Ω → 𝓐) (R' : ℕ → Ω → R)
  (a : 𝓐) (m : ℕ) (ω : Ω × (ℕ → 𝓐 → R)) : R
Learning.rewardByCount.{u_1, u_2, u_3}
  {𝓐 : Type u_1} {R : Type u_2}
  {Ω : Type u_3} [DecidableEq 𝓐]
  (A : ℕ → Ω → 𝓐) (R' : ℕ → Ω → R) (a : 𝓐)
  (m : ℕ) (ω : Ω × (ℕ → 𝓐 → R)) : R

Code

noncomputable
def rewardByCount (A : ℕ → Ω → 𝓐) (R' : ℕ → Ω → R) (a : 𝓐) (m : ℕ) (ω : Ω × (ℕ → 𝓐 → R)) : R :=
  match (stepsUntil A a m ω.1) with
  | ⊤ => ω.2 m a
  | (n : ℕ) => R' n ω.1

Body uses (1)

stepsUntil

Used by (15)

Actions: Source · Open Issue

`rewardByCount_eq_ite`🔗

LemmaLearning.rewardByCount_eq_ite

Details

No docstring.

theorem

Learning.rewardByCount_eq_ite.{u_1, u_2, u_3} {𝓐 : Type u_1}
  {R : Type u_2} {Ω : Type u_3} [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐}
  {R' : ℕ → Ω → R} (a : 𝓐) (m : ℕ) (ω : Ω × (ℕ → 𝓐 → R)) :
  rewardByCount A R' a m ω =
    if stepsUntil A a m (Prod.fst ω) = ⊤ then Prod.snd ω m a
    else R' (ENat.toNat (stepsUntil A a m (Prod.fst ω))) (Prod.fst ω)
Learning.rewardByCount_eq_ite.{u_1, u_2,
    u_3}
  {𝓐 : Type u_1} {R : Type u_2}
  {Ω : Type u_3} [DecidableEq 𝓐]
  {A : ℕ → Ω → 𝓐} {R' : ℕ → Ω → R} (a : 𝓐)
  (m : ℕ) (ω : Ω × (ℕ → 𝓐 → R)) :
  rewardByCount A R' a m ω =
    if
        stepsUntil A a m (Prod.fst ω) =
          ⊤ then
      Prod.snd ω m a
    else
      R'
        (ENat.toNat
          (stepsUntil A a m (Prod.fst ω)))
        (Prod.fst ω)

Code

lemma rewardByCount_eq_ite (a : 𝓐) (m : ℕ) (ω : Ω × (ℕ → 𝓐 → R)) :
    rewardByCount A R' a m ω =
      if (stepsUntil A a m ω.1) = ⊤ then ω.2 m a else R' (stepsUntil A a m ω.1).toNat ω.1

Type uses (2)

Used by (6)

Actions: Source · Open Issue

Proof

by
  unfold rewardByCount
  cases stepsUntil A a m ω.1
  · simp; rfl
  · simp

`rewardByCount_eq_add`🔗

LemmaLearning.rewardByCount_eq_add

Details

No docstring.

theorem

Learning.rewardByCount_eq_add.{u_1, u_2, u_3} {𝓐 : Type u_1}
  {R : Type u_2} {Ω : Type u_3} [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐}
  {R' : ℕ → Ω → R} [AddMonoid R] (a : 𝓐) (m : ℕ) :
  rewardByCount A R' a m =
    (Set.indicator {ω | stepsUntil A a m (Prod.fst ω) ≠ ⊤} fun ω =>
        R' (ENat.toNat (stepsUntil A a m (Prod.fst ω))) (Prod.fst ω)) +
      Set.indicator {ω | stepsUntil A a m (Prod.fst ω) = ⊤} fun ω =>
        Prod.snd ω m a
Learning.rewardByCount_eq_add.{u_1, u_2,
    u_3}
  {𝓐 : Type u_1} {R : Type u_2}
  {Ω : Type u_3} [DecidableEq 𝓐]
  {A : ℕ → Ω → 𝓐} {R' : ℕ → Ω → R}
  [AddMonoid R] (a : 𝓐) (m : ℕ) :
  rewardByCount A R' a m =
    (Set.indicator
        {ω |
          stepsUntil A a m (Prod.fst ω) ≠
            ⊤}
        fun ω =>
        R'
          (ENat.toNat
            (stepsUntil A a m
              (Prod.fst ω)))
          (Prod.fst ω)) +
      Set.indicator
        {ω |
          stepsUntil A a m (Prod.fst ω) =
            ⊤}
        fun ω => Prod.snd ω m a

Code

lemma rewardByCount_eq_add [AddMonoid R] (a : 𝓐) (m : ℕ) :
    rewardByCount A R' a m =
      {ω : Ω × (ℕ → 𝓐 → R) | stepsUntil A a m ω.1 ≠ ⊤}.indicator
          (fun ω ↦ R' (stepsUntil A a m ω.1).toNat ω.1)
        + {ω | stepsUntil A a m ω.1 = ⊤}.indicator (fun ω ↦ ω.2 m a)

Type uses (2)

Body uses (1)

rewardByCount_eq_ite

Actions: Source · Open Issue

Proof

by
  ext ω
  simp only [rewardByCount_eq_ite, ne_eq, Pi.add_apply, Set.indicator_apply, Set.mem_setOf_eq,
    ite_not]
  grind

`rewardByCount_of_stepsUntil_eq_top`🔗

LemmaLearning.rewardByCount_of_stepsUntil_eq_top

Details

No docstring.

theorem

Learning.rewardByCount_of_stepsUntil_eq_top.{u_1, u_2, u_3}
  {𝓐 : Type u_1} {R : Type u_2} {Ω : Type u_3} [DecidableEq 𝓐]
  {A : ℕ → Ω → 𝓐} {R' : ℕ → Ω → R} {a : 𝓐} {m : ℕ} {ω : Ω × (ℕ → 𝓐 → R)}
  (h : stepsUntil A a m (Prod.fst ω) = ⊤) :
  rewardByCount A R' a m ω = Prod.snd ω m a
Learning.rewardByCount_of_stepsUntil_eq_top.{u_1,
    u_2, u_3}
  {𝓐 : Type u_1} {R : Type u_2}
  {Ω : Type u_3} [DecidableEq 𝓐]
  {A : ℕ → Ω → 𝓐} {R' : ℕ → Ω → R} {a : 𝓐}
  {m : ℕ} {ω : Ω × (ℕ → 𝓐 → R)}
  (h :
    stepsUntil A a m (Prod.fst ω) = ⊤) :
  rewardByCount A R' a m ω =
    Prod.snd ω m a

Code

lemma rewardByCount_of_stepsUntil_eq_top (h : stepsUntil A a m ω.1 = ⊤) :
    rewardByCount A R' a m ω = ω.2 m a

Type uses (2)

Body uses (1)

rewardByCount_eq_ite

Used by (1)

condDistrib_rewardByCount_stepsUntil

Actions: Source · Open Issue

Proof

by simp [rewardByCount_eq_ite, h]

`rewardByCount_of_stepsUntil_ne_top`🔗

LemmaLearning.rewardByCount_of_stepsUntil_ne_top

Details

No docstring.

theorem

Learning.rewardByCount_of_stepsUntil_ne_top.{u_1, u_2, u_3}
  {𝓐 : Type u_1} {R : Type u_2} {Ω : Type u_3} [DecidableEq 𝓐]
  {A : ℕ → Ω → 𝓐} {R' : ℕ → Ω → R} {a : 𝓐} {m : ℕ} {ω : Ω × (ℕ → 𝓐 → R)}
  (h : stepsUntil A a m (Prod.fst ω) ≠ ⊤) :
  rewardByCount A R' a m ω =
    R' (ENat.toNat (stepsUntil A a m (Prod.fst ω))) (Prod.fst ω)
Learning.rewardByCount_of_stepsUntil_ne_top.{u_1,
    u_2, u_3}
  {𝓐 : Type u_1} {R : Type u_2}
  {Ω : Type u_3} [DecidableEq 𝓐]
  {A : ℕ → Ω → 𝓐} {R' : ℕ → Ω → R} {a : 𝓐}
  {m : ℕ} {ω : Ω × (ℕ → 𝓐 → R)}
  (h :
    stepsUntil A a m (Prod.fst ω) ≠ ⊤) :
  rewardByCount A R' a m ω =
    R'
      (ENat.toNat
        (stepsUntil A a m (Prod.fst ω)))
      (Prod.fst ω)

Code

lemma rewardByCount_of_stepsUntil_ne_top (h : stepsUntil A a m ω.1 ≠ ⊤) :
    rewardByCount A R' a m ω = R' (stepsUntil A a m ω.1).toNat ω.1

Type uses (2)

Body uses (1)

rewardByCount_eq_ite

Used by (1)

rewardByCount_eq_stoppedValue

Actions: Source · Open Issue

Proof

by
  simp [rewardByCount_eq_ite, h]

`rewardByCount_eq_stoppedValue`🔗

LemmaLearning.rewardByCount_eq_stoppedValue

Details

No docstring.

theorem

Learning.rewardByCount_eq_stoppedValue.{u_1, u_2, u_3} {𝓐 : Type u_1}
  {R : Type u_2} {Ω : Type u_3} [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐}
  {R' : ℕ → Ω → R} {a : 𝓐} {m : ℕ} {ω : Ω × (ℕ → 𝓐 → R)}
  (h : stepsUntil A a m (Prod.fst ω) ≠ ⊤) :
  rewardByCount A R' a m ω =
    MeasureTheory.stoppedValue R' (stepsUntil A a m) (Prod.fst ω)
Learning.rewardByCount_eq_stoppedValue.{u_1,
    u_2, u_3}
  {𝓐 : Type u_1} {R : Type u_2}
  {Ω : Type u_3} [DecidableEq 𝓐]
  {A : ℕ → Ω → 𝓐} {R' : ℕ → Ω → R} {a : 𝓐}
  {m : ℕ} {ω : Ω × (ℕ → 𝓐 → R)}
  (h :
    stepsUntil A a m (Prod.fst ω) ≠ ⊤) :
  rewardByCount A R' a m ω =
    MeasureTheory.stoppedValue R'
      (stepsUntil A a m) (Prod.fst ω)

Code

lemma rewardByCount_eq_stoppedValue (h : stepsUntil A a m ω.1 ≠ ⊤) :
    rewardByCount A R' a m ω = stoppedValue R' (stepsUntil A a m) ω.1

Type uses (2)

Body uses (1)

rewardByCount_of_stepsUntil_ne_top

Actions: Source · Open Issue

Proof

by
  rw [rewardByCount_of_stepsUntil_ne_top h, stoppedValue]
  lift stepsUntil A a m ω.1 to ℕ using h with n
  simp

`rewardByCount_of_stepsUntil_eq_coe`🔗

LemmaLearning.rewardByCount_of_stepsUntil_eq_coe

Details

No docstring.

theorem

Learning.rewardByCount_of_stepsUntil_eq_coe.{u_1, u_2, u_3}
  {𝓐 : Type u_1} {R : Type u_2} {Ω : Type u_3} [DecidableEq 𝓐]
  {A : ℕ → Ω → 𝓐} {R' : ℕ → Ω → R} {a : 𝓐} {m n : ℕ}
  {ω : Ω × (ℕ → 𝓐 → R)} (h : stepsUntil A a m (Prod.fst ω) = ↑n) :
  rewardByCount A R' a m ω = R' n (Prod.fst ω)
Learning.rewardByCount_of_stepsUntil_eq_coe.{u_1,
    u_2, u_3}
  {𝓐 : Type u_1} {R : Type u_2}
  {Ω : Type u_3} [DecidableEq 𝓐]
  {A : ℕ → Ω → 𝓐} {R' : ℕ → Ω → R} {a : 𝓐}
  {m n : ℕ} {ω : Ω × (ℕ → 𝓐 → R)}
  (h :
    stepsUntil A a m (Prod.fst ω) = ↑n) :
  rewardByCount A R' a m ω =
    R' n (Prod.fst ω)

Code

lemma rewardByCount_of_stepsUntil_eq_coe (h : stepsUntil A a m ω.1 = n) :
    rewardByCount A R' a m ω = R' n ω.1

Type uses (2)

Body uses (1)

rewardByCount_eq_ite

Used by (1)

condDistrib_rewardByCount_stepsUntil

Actions: Source · Open Issue

Proof

by simp [rewardByCount_eq_ite, h]

`rewardByCount_zero`🔗

LemmaLearning.rewardByCount_zero

Details

The value at 0 does not matter (it would be the "zeroth" reward). It should be considered a junk value.

theorem

Learning.rewardByCount_zero.{u_1, u_2, u_3} {𝓐 : Type u_1}
  {R : Type u_2} {Ω : Type u_3} [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐}
  {R' : ℕ → Ω → R} (a : 𝓐) (ω : Ω × (ℕ → 𝓐 → R)) :
  rewardByCount A R' a 0 ω =
    if A 0 (Prod.fst ω) = a then Prod.snd ω 0 a else R' 0 (Prod.fst ω)
Learning.rewardByCount_zero.{u_1, u_2,
    u_3}
  {𝓐 : Type u_1} {R : Type u_2}
  {Ω : Type u_3} [DecidableEq 𝓐]
  {A : ℕ → Ω → 𝓐} {R' : ℕ → Ω → R} (a : 𝓐)
  (ω : Ω × (ℕ → 𝓐 → R)) :
  rewardByCount A R' a 0 ω =
    if A 0 (Prod.fst ω) = a then
      Prod.snd ω 0 a
    else R' 0 (Prod.fst ω)

Code

lemma rewardByCount_zero (a : 𝓐) (ω : Ω × (ℕ → 𝓐 → R)) :
    rewardByCount A R' a 0 ω = if A 0 ω.1 = a then ω.2 0 a else R' 0 ω.1

Type uses (1)

rewardByCount

Body uses (4)

Actions: Source · Open Issue

Proof

by
  rw [rewardByCount_eq_ite]
  by_cases ha : A 0 ω.1 = a
  · simp [ha, stepsUntil_zero_of_eq]
  · simp [stepsUntil_zero_of_ne, ha]

`rewardByCount_pullCount_add_one_eq_reward`🔗

LemmaLearning.rewardByCount_pullCount_add_one_eq_reward

Details

No docstring.

theorem

Learning.rewardByCount_pullCount_add_one_eq_reward.{u_1, u_2, u_3}
  {𝓐 : Type u_1} {R : Type u_2} {Ω : Type u_3} [DecidableEq 𝓐]
  {A : ℕ → Ω → 𝓐} {R' : ℕ → Ω → R} (t : ℕ) (ω : Ω × (ℕ → 𝓐 → R)) :
  rewardByCount A R' (A t (Prod.fst ω))
      (pullCount A (A t (Prod.fst ω)) t (Prod.fst ω) + 1) ω =
    R' t (Prod.fst ω)
Learning.rewardByCount_pullCount_add_one_eq_reward.{u_1,
    u_2, u_3}
  {𝓐 : Type u_1} {R : Type u_2}
  {Ω : Type u_3} [DecidableEq 𝓐]
  {A : ℕ → Ω → 𝓐} {R' : ℕ → Ω → R} (t : ℕ)
  (ω : Ω × (ℕ → 𝓐 → R)) :
  rewardByCount A R' (A t (Prod.fst ω))
      (pullCount A (A t (Prod.fst ω)) t
          (Prod.fst ω) +
        1)
      ω =
    R' t (Prod.fst ω)

Code

lemma rewardByCount_pullCount_add_one_eq_reward (t : ℕ) (ω : Ω × (ℕ → 𝓐 → R)) :
    rewardByCount A R' (A t ω.1) (pullCount A (A t ω.1) t ω.1 + 1) ω = R' t ω.1

Type uses (2)

Body uses (3)

Used by (1)

sum_rewardByCount_eq_sumRewards

Actions: Source · Open Issue

Proof

by
  rw [rewardByCount, ← pullCount_action_eq_pullCount_add_one, stepsUntil_pullCount_eq]

`measurable_rewardByCount`🔗

LemmaLearning.measurable_rewardByCount

Details

No docstring.

theorem

Learning.measurable_rewardByCount.{u_1, u_2, u_3} {𝓐 : Type u_1}
  {R : Type u_2} {Ω : Type u_3} {m𝓐 : MeasurableSpace 𝓐}
  {mR : MeasurableSpace R} {mΩ : MeasurableSpace Ω} [DecidableEq 𝓐]
  {A : ℕ → Ω → 𝓐} {R' : ℕ → Ω → R} [MeasurableSingletonClass 𝓐]
  (hA : ∀ (n : ℕ), Measurable (A n))
  (hR' : ∀ (n : ℕ), Measurable (R' n)) (a : 𝓐) (m : ℕ) :
  Measurable fun ω => rewardByCount A R' a m ω
Learning.measurable_rewardByCount.{u_1,
    u_2, u_3}
  {𝓐 : Type u_1} {R : Type u_2}
  {Ω : Type u_3} {m𝓐 : MeasurableSpace 𝓐}
  {mR : MeasurableSpace R}
  {mΩ : MeasurableSpace Ω} [DecidableEq 𝓐]
  {A : ℕ → Ω → 𝓐} {R' : ℕ → Ω → R}
  [MeasurableSingletonClass 𝓐]
  (hA : ∀ (n : ℕ), Measurable (A n))
  (hR' : ∀ (n : ℕ), Measurable (R' n))
  (a : 𝓐) (m : ℕ) :
  Measurable fun ω =>
    rewardByCount A R' a m ω

Code

lemma measurable_rewardByCount [MeasurableSingletonClass 𝓐]
    (hA : ∀ n, Measurable (A n)) (hR' : ∀ n, Measurable (R' n)) (a : 𝓐) (m : ℕ) :
    Measurable (fun ω : Ω × (ℕ → 𝓐 → R) ↦ rewardByCount A R' a m ω)

Type uses (1)

rewardByCount

Body uses (4)

Used by (4)

Actions: Source · Open Issue

Proof

by
  simp_rw [rewardByCount_eq_ite]
  refine Measurable.ite ?_ ?_ ?_
  · exact (measurableSet_singleton _).preimage <| measurable_stepsUntil' hA a m
  · fun_prop
  · change Measurable ((fun p : ℕ × Ω ↦ R' p.1 p.2)
      ∘ (fun ω : Ω × (ℕ → 𝓐 → R) ↦ ((stepsUntil A a m ω.1).toNat, ω.1)))
    have : Measurable fun ω : Ω × (ℕ → 𝓐 → R) ↦ ((stepsUntil A a m ω.1).toNat, ω.1) :=
      (measurable_stepsUntil' hA a m).toNat.prodMk (by fun_prop)
    refine Measurable.comp ?_ this
    refine measurable_from_prod_countable_right fun n ↦ ?_
    simp only
    fun_prop

`sum_pullCount_mul`🔗

LemmaLearning.sum_pullCount_mul

Details

No docstring.

theorem

Learning.sum_pullCount_mul.{u_1, u_2, u_3} {𝓐 : Type u_1} {R : Type u_2}
  {Ω : Type u_3} [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} [Fintype 𝓐]
  [Semiring R] (ω : Ω) (f : 𝓐 → R) (t : ℕ) :
  ∑ a, ↑(pullCount A a t ω) * f a = ∑ s ∈ Finset.range t, f (A s ω)
Learning.sum_pullCount_mul.{u_1, u_2, u_3}
  {𝓐 : Type u_1} {R : Type u_2}
  {Ω : Type u_3} [DecidableEq 𝓐]
  {A : ℕ → Ω → 𝓐} [Fintype 𝓐] [Semiring R]
  (ω : Ω) (f : 𝓐 → R) (t : ℕ) :
  ∑ a, ↑(pullCount A a t ω) * f a =
    ∑ s ∈ Finset.range t, f (A s ω)

Code

lemma sum_pullCount_mul [Fintype 𝓐] [Semiring R] (ω : Ω) (f : 𝓐 → R) (t : ℕ) :
    ∑ a, pullCount A a t ω * f a = ∑ s ∈ range t, f (A s ω)

Type uses (1)

pullCount

Used by (2)

Actions: Source · Open Issue

Proof

by
  unfold pullCount
  classical
  simp_rw [card_eq_sum_ones]
  push_cast
  simp_rw [sum_mul, one_mul]
  exact sum_fiberwise' (range t) (A · ω) f

`sum_pullCount`🔗

LemmaLearning.sum_pullCount

Details

No docstring.

theorem

Learning.sum_pullCount.{u_1, u_3} {𝓐 : Type u_1} {Ω : Type u_3}
  [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} {t : ℕ} [Fintype 𝓐] {ω : Ω} :
  ∑ a, pullCount A a t ω = t
Learning.sum_pullCount.{u_1, u_3}
  {𝓐 : Type u_1} {Ω : Type u_3}
  [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} {t : ℕ}
  [Fintype 𝓐] {ω : Ω} :
  ∑ a, pullCount A a t ω = t

Code

lemma sum_pullCount [Fintype 𝓐] {ω : Ω} : ∑ a, pullCount A a t ω = t

Type uses (1)

pullCount

Body uses (1)

sum_pullCount_mul

Used by (1)

sum_ucb_sub_mean_le

Actions: Source · Open Issue

Proof

by
  suffices ∑ a, pullCount A a t ω * (1 : ℝ) = t by norm_cast at this; simpa
  rw [sum_pullCount_mul]
  simp

`sum_comp_pullCount`🔗

LemmaLearning.sum_comp_pullCount

Details

No docstring.

theorem

Learning.sum_comp_pullCount.{u_1, u_2, u_3} {𝓐 : Type u_1}
  {R : Type u_2} {Ω : Type u_3} [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐}
  [Fintype 𝓐] [AddCommMonoid R] (f : ℕ → R) (t : ℕ) (ω : Ω) :
  ∑ s ∈ Finset.range t, f (pullCount A (A s ω) s ω) =
    ∑ a, ∑ j ∈ Finset.range (pullCount A a t ω), f j
Learning.sum_comp_pullCount.{u_1, u_2,
    u_3}
  {𝓐 : Type u_1} {R : Type u_2}
  {Ω : Type u_3} [DecidableEq 𝓐]
  {A : ℕ → Ω → 𝓐} [Fintype 𝓐]
  [AddCommMonoid R] (f : ℕ → R) (t : ℕ)
  (ω : Ω) :
  ∑ s ∈ Finset.range t,
      f (pullCount A (A s ω) s ω) =
    ∑ a,
      ∑
        j ∈
          Finset.range
            (pullCount A a t ω),
        f j

Code

lemma sum_comp_pullCount [Fintype 𝓐] [AddCommMonoid R] (f : ℕ → R) (t : ℕ) (ω : Ω) :
    ∑ s ∈ range t, f (pullCount A (A s ω) s ω) = ∑ a, ∑ j ∈ range (pullCount A a t ω), f j

Type uses (1)

pullCount

Body uses (2)

Used by (1)

sum_ucb_sub_mean_le

Actions: Source · Open Issue

Proof

by
  induction t with
  | zero => simp
  | succ n ih =>
    have hf : f (pullCount A (A n ω) n ω) =
      ∑ a, if A n ω = a then f (pullCount A a n ω) else 0 := by simp
    simp_rw [sum_range_succ, ih, hf, ← sum_add_distrib, pullCount_add_one]
    congr 1 with a
    split_ifs
    · simp [sum_range_succ]
    · simp

`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

`sumRewards'`🔗

DefinitionLearning.sumRewards'

Details

Sum of rewards of arm a up to (and including) time n.

def

Learning.sumRewards'.{u_1} {𝓐 : Type u_1} [DecidableEq 𝓐] (n : ℕ)
  (h : ↥(Finset.Iic n) → 𝓐 × ℝ) (a : 𝓐) : ℝ
Learning.sumRewards'.{u_1} {𝓐 : Type u_1}
  [DecidableEq 𝓐] (n : ℕ)
  (h : ↥(Finset.Iic n) → 𝓐 × ℝ) (a : 𝓐) :
  ℝ

Code

noncomputable
def sumRewards' (n : ℕ) (h : Iic n → 𝓐 × ℝ) (a : 𝓐) :=
  ∑ s, if (h s).1 = a then (h s).2 else 0

Used by (9)

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

`empMean'`🔗

DefinitionLearning.empMean'

Details

Empirical mean of arm a at time n.

def

Learning.empMean'.{u_1} {𝓐 : Type u_1} [DecidableEq 𝓐] (n : ℕ)
  (h : ↥(Finset.Iic n) → 𝓐 × ℝ) (a : 𝓐) : ℝ
Learning.empMean'.{u_1} {𝓐 : Type u_1}
  [DecidableEq 𝓐] (n : ℕ)
  (h : ↥(Finset.Iic n) → 𝓐 × ℝ) (a : 𝓐) :
  ℝ

Code

noncomputable
def empMean' (n : ℕ) (h : Iic n → 𝓐 × ℝ) (a : 𝓐) :=
  (sumRewards' n h a) / (pullCount' n h a)

Body uses (2)

Used by (18)

Actions: Source · Open Issue

`sumRewards_zero`🔗

LemmaLearning.sumRewards_zero

Details

No docstring.

theorem

Learning.sumRewards_zero.{u_1, u_3} {𝓐 : Type u_1} {Ω : Type u_3}
  [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} {a : 𝓐} {R' : ℕ → Ω → ℝ} :
  sumRewards A R' a 0 = 0
Learning.sumRewards_zero.{u_1, u_3}
  {𝓐 : Type u_1} {Ω : Type u_3}
  [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} {a : 𝓐}
  {R' : ℕ → Ω → ℝ} :
  sumRewards A R' a 0 = 0

Code

lemma sumRewards_zero {R' : ℕ → Ω → ℝ} : sumRewards A R' a 0 = 0

Type uses (1)

sumRewards

Used by (3)

Actions: Source · Open Issue

Proof

by ext; simp [sumRewards]

`sumRewards_add_one`🔗

LemmaLearning.sumRewards_add_one

Details

No docstring.

theorem

Learning.sumRewards_add_one.{u_1, u_3} {𝓐 : Type u_1} {Ω : Type u_3}
  [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} {a : 𝓐} {t : ℕ} {ω : Ω}
  {R' : ℕ → Ω → ℝ} :
  sumRewards A R' a (t + 1) ω =
    sumRewards A R' a t ω + if A t ω = a then R' t ω else 0
Learning.sumRewards_add_one.{u_1, u_3}
  {𝓐 : Type u_1} {Ω : Type u_3}
  [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} {a : 𝓐}
  {t : ℕ} {ω : Ω} {R' : ℕ → Ω → ℝ} :
  sumRewards A R' a (t + 1) ω =
    sumRewards A R' a t ω +
      if A t ω = a then R' t ω else 0

Code

lemma sumRewards_add_one {R' : ℕ → Ω → ℝ} :
    sumRewards A R' a (t + 1) ω = sumRewards A R' a t ω + if A t ω = a then R' t ω else 0

Type uses (1)

sumRewards

Used by (3)

Actions: Source · Open Issue

Proof

by
  unfold sumRewards
  rw [sum_range_succ]

`sumRewards_eq_of_pullCount_eq`🔗

LemmaLearning.sumRewards_eq_of_pullCount_eq

Details

No docstring.

theorem

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

Code

lemma sumRewards_eq_of_pullCount_eq {R' : ℕ → Ω → ℝ} {s t : ℕ}
    (h_eq : pullCount A a s ω = pullCount A a t ω) :
    sumRewards A R' a s ω = sumRewards A R' a t ω

Type uses (2)

Body uses (3)

Actions: Source · Open Issue

Proof

by
  wlog hst : s ≤ t
  · have hts : t ≤ s := by lia
    exact (this h_eq.symm hts).symm
  induction t, hst using Nat.le_induction with
  | base => rfl
  | succ t hst' ih =>
    have h_mono' : pullCount A a t ω ≤ pullCount A a (t + 1) ω := pullCount_mono a (Nat.le_succ t) ω
    have h_eq_t : pullCount A a s ω = pullCount A a t ω :=
      le_antisymm (pullCount_mono a hst' ω) (h_eq ▸ h_mono')
    have hne : A t ω ≠ a := by
      intro ha
      have h1 := ha ▸ pullCount_action_eq_pullCount_add_one (A := A) t ω
      lia
    rw [sumRewards_add_one, if_neg hne, add_zero, ih h_eq_t]

`sumRewards_eq_pullCount_mul_empMean`🔗

LemmaLearning.sumRewards_eq_pullCount_mul_empMean

Details

No docstring.

theorem

Learning.sumRewards_eq_pullCount_mul_empMean.{u_1, u_3} {𝓐 : Type u_1}
  {Ω : Type u_3} [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} {a : 𝓐} {t : ℕ}
  {R' : ℕ → Ω → ℝ} {ω : Ω} (h_pull : pullCount A a t ω ≠ 0) :
  sumRewards A R' a t ω = ↑(pullCount A a t ω) * empMean A R' a t ω
Learning.sumRewards_eq_pullCount_mul_empMean.{u_1,
    u_3}
  {𝓐 : Type u_1} {Ω : Type u_3}
  [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} {a : 𝓐}
  {t : ℕ} {R' : ℕ → Ω → ℝ} {ω : Ω}
  (h_pull : pullCount A a t ω ≠ 0) :
  sumRewards A R' a t ω =
    ↑(pullCount A a t ω) *
      empMean A R' a t ω

Code

lemma sumRewards_eq_pullCount_mul_empMean {R' : ℕ → Ω → ℝ} {ω : Ω}
    (h_pull : pullCount A a t ω ≠ 0) :
    sumRewards A R' a t ω = pullCount A a t ω * empMean A R' a t ω

Type uses (3)

Used by (1)

sumRewards_bestArm_le_of_arm_mul_eq

Actions: Source · Open Issue

Proof

by unfold empMean; field_simp

`sum_rewardByCount_eq_sumRewards`🔗

LemmaLearning.sum_rewardByCount_eq_sumRewards

Details

No docstring.

theorem

Learning.sum_rewardByCount_eq_sumRewards.{u_1, u_3} {𝓐 : Type u_1}
  {Ω : Type u_3} [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} {R' : ℕ → Ω → ℝ}
  (a : 𝓐) (t : ℕ) (ω : Ω × (ℕ → 𝓐 → ℝ)) :
  ∑ m ∈ Finset.Icc 1 (pullCount A a t (Prod.fst ω)),
      rewardByCount A R' a m ω =
    sumRewards A R' a t (Prod.fst ω)
Learning.sum_rewardByCount_eq_sumRewards.{u_1,
    u_3}
  {𝓐 : Type u_1} {Ω : Type u_3}
  [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐}
  {R' : ℕ → Ω → ℝ} (a : 𝓐) (t : ℕ)
  (ω : Ω × (ℕ → 𝓐 → ℝ)) :
  ∑
      m ∈
        Finset.Icc 1
          (pullCount A a t (Prod.fst ω)),
      rewardByCount A R' a m ω =
    sumRewards A R' a t (Prod.fst ω)

Code

lemma sum_rewardByCount_eq_sumRewards {R' : ℕ → Ω → ℝ} (a : 𝓐) (t : ℕ) (ω : Ω × (ℕ → 𝓐 → ℝ)) :
    ∑ m ∈ Icc 1 (pullCount A a t ω.1), rewardByCount A R' a m ω = sumRewards A R' a t ω.1

Type uses (3)

Body uses (3)

Actions: Source · Open Issue

Proof

by
  induction t with
  | zero => simp [pullCount, sumRewards]
  | succ t ht =>
    by_cases hta : A t ω.1 = a
    · rw [← hta] at ht ⊢
      rw [pullCount_action_eq_pullCount_add_one, sum_Icc_succ_top (Nat.le_add_left 1 _), ht]
      unfold sumRewards
      rw [sum_range_succ, if_pos rfl, rewardByCount_pullCount_add_one_eq_reward]
    · unfold sumRewards
      rwa [pullCount_eq_pullCount_of_action_ne hta, sum_range_succ, if_neg hta, add_zero]

`sumRewards_add_one_eq_sumRewards'`🔗

LemmaLearning.sumRewards_add_one_eq_sumRewards'

Details

No docstring.

theorem

Learning.sumRewards_add_one_eq_sumRewards'.{u_1, u_3} {𝓐 : Type u_1}
  {Ω : Type u_3} [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} {a : 𝓐}
  {R' : ℕ → Ω → ℝ} {n : ℕ} {ω : Ω} :
  sumRewards A R' a (n + 1) ω =
    sumRewards' n (fun i => (A (↑i) ω, R' (↑i) ω)) a
Learning.sumRewards_add_one_eq_sumRewards'.{u_1,
    u_3}
  {𝓐 : Type u_1} {Ω : Type u_3}
  [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} {a : 𝓐}
  {R' : ℕ → Ω → ℝ} {n : ℕ} {ω : Ω} :
  sumRewards A R' a (n + 1) ω =
    sumRewards' n
      (fun i => (A (↑i) ω, R' (↑i) ω)) a

Code

lemma sumRewards_add_one_eq_sumRewards' {R' : ℕ → Ω → ℝ} {n : ℕ} {ω : Ω} :
    sumRewards A R' a (n + 1) ω = sumRewards' n (fun i ↦ (A i ω, R' i ω)) a

Type uses (2)

Used by (2)

Actions: Source · Open Issue

Proof

by
  unfold sumRewards sumRewards'
  rw [Finset.sum_coe_sort (f := fun s ↦ if A s ω = a then R' s ω else 0) (Iic n)]
  congr with m
  simp only [mem_range, mem_Iic]
  grind

`sumRewards_eq_sumRewards'`🔗

LemmaLearning.sumRewards_eq_sumRewards'

Details

No docstring.

theorem

Learning.sumRewards_eq_sumRewards'.{u_1, u_3} {𝓐 : Type u_1}
  {Ω : Type u_3} [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} {a : 𝓐}
  {R' : ℕ → Ω → ℝ} {n : ℕ} {ω : Ω} (hn : n ≠ 0) :
  sumRewards A R' a n ω =
    sumRewards' (n - 1) (fun i => (A (↑i) ω, R' (↑i) ω)) a
Learning.sumRewards_eq_sumRewards'.{u_1,
    u_3}
  {𝓐 : Type u_1} {Ω : Type u_3}
  [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} {a : 𝓐}
  {R' : ℕ → Ω → ℝ} {n : ℕ} {ω : Ω}
  (hn : n ≠ 0) :
  sumRewards A R' a n ω =
    sumRewards' (n - 1)
      (fun i => (A (↑i) ω, R' (↑i) ω)) a

Code

lemma sumRewards_eq_sumRewards' {R' : ℕ → Ω → ℝ} {n : ℕ} {ω : Ω} (hn : n ≠ 0) :
    sumRewards A R' a n ω = sumRewards' (n - 1) (fun i ↦ (A i ω, R' i ω)) a

Type uses (2)

Body uses (1)

sumRewards_add_one_eq_sumRewards'

Used by (1)

empMean_eq_empMean'

Actions: Source · Open Issue

Proof

by
  cases n with
  | zero => exact absurd rfl hn
  | succ n => simp [sumRewards_add_one_eq_sumRewards']

`empMean_add_one_eq_empMean'`🔗

LemmaLearning.empMean_add_one_eq_empMean'

Details

No docstring.

theorem

Learning.empMean_add_one_eq_empMean'.{u_1, u_3} {𝓐 : Type u_1}
  {Ω : Type u_3} [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} {a : 𝓐}
  {R' : ℕ → Ω → ℝ} {n : ℕ} {ω : Ω} :
  empMean A R' a (n + 1) ω =
    empMean' n (fun i => (A (↑i) ω, R' (↑i) ω)) a
Learning.empMean_add_one_eq_empMean'.{u_1,
    u_3}
  {𝓐 : Type u_1} {Ω : Type u_3}
  [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} {a : 𝓐}
  {R' : ℕ → Ω → ℝ} {n : ℕ} {ω : Ω} :
  empMean A R' a (n + 1) ω =
    empMean' n
      (fun i => (A (↑i) ω, R' (↑i) ω)) a

Code

lemma empMean_add_one_eq_empMean' {R' : ℕ → Ω → ℝ} {n : ℕ} {ω : Ω} :
    empMean A R' a (n + 1) ω = empMean' n (fun i ↦ (A i ω, R' i ω)) a

Type uses (2)

Body uses (6)

Used by (1)

ucb_succ_eq_ucb'

Actions: Source · Open Issue

Proof

by
  unfold empMean empMean'
  rw [sumRewards_add_one_eq_sumRewards', pullCount_add_one_eq_pullCount']

`empMean_eq_empMean'`🔗

LemmaLearning.empMean_eq_empMean'

Details

No docstring.

theorem

Learning.empMean_eq_empMean'.{u_1, u_3} {𝓐 : Type u_1} {Ω : Type u_3}
  [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} {a : 𝓐} {R' : ℕ → Ω → ℝ} {n : ℕ}
  {ω : Ω} (hn : n ≠ 0) :
  empMean A R' a n ω =
    empMean' (n - 1) (fun i => (A (↑i) ω, R' (↑i) ω)) a
Learning.empMean_eq_empMean'.{u_1, u_3}
  {𝓐 : Type u_1} {Ω : Type u_3}
  [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} {a : 𝓐}
  {R' : ℕ → Ω → ℝ} {n : ℕ} {ω : Ω}
  (hn : n ≠ 0) :
  empMean A R' a n ω =
    empMean' (n - 1)
      (fun i => (A (↑i) ω, R' (↑i) ω)) a

Code

lemma empMean_eq_empMean' {R' : ℕ → Ω → ℝ} {n : ℕ} {ω : Ω} (hn : n ≠ 0) :
    empMean A R' a n ω = empMean' (n - 1) (fun i ↦ (A i ω, R' i ω)) a

Type uses (2)

Body uses (6)

Used by (2)

Actions: Source · Open Issue

Proof

by
  unfold empMean empMean'
  rw [sumRewards_eq_sumRewards' hn, pullCount_eq_pullCount' hn]

`sumRewards_sub_pullCount_mul_eq_sum`🔗

LemmaLearning.sumRewards_sub_pullCount_mul_eq_sum

Details

No docstring.

theorem

Learning.sumRewards_sub_pullCount_mul_eq_sum.{u_1, u_3} {𝓐 : Type u_1}
  {Ω : Type u_3} [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} {a : 𝓐} {n : ℕ} {ω : Ω}
  {R' : ℕ → Ω → ℝ} (c : 𝓐 → ℝ) :
  sumRewards A R' a (n + 1) ω - ↑(pullCount A a (n + 1) ω) * c a =
    ∑ i ∈ Finset.range (n + 1), if A i ω = a then R' i ω - c a else 0
Learning.sumRewards_sub_pullCount_mul_eq_sum.{u_1,
    u_3}
  {𝓐 : Type u_1} {Ω : Type u_3}
  [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} {a : 𝓐}
  {n : ℕ} {ω : Ω} {R' : ℕ → Ω → ℝ}
  (c : 𝓐 → ℝ) :
  sumRewards A R' a (n + 1) ω -
      ↑(pullCount A a (n + 1) ω) * c a =
    ∑ i ∈ Finset.range (n + 1),
      if A i ω = a then R' i ω - c a
      else 0

Code

lemma sumRewards_sub_pullCount_mul_eq_sum {R' : ℕ → Ω → ℝ} (c : 𝓐 → ℝ) :
    sumRewards A R' a (n + 1) ω - pullCount A a (n + 1) ω * c a =
      ∑ i ∈ range (n + 1), (if A i ω = a then R' i ω - c a else 0)

Type uses (2)

Body uses (4)

Actions: Source · Open Issue

Proof

by
  induction n with
  | zero =>
    simp_rw [sumRewards_add_one, pullCount_add_one]
    simp only [sumRewards_zero, Pi.zero_apply, zero_add, pullCount_zero, Nat.cast_ite, Nat.cast_one,
      CharP.cast_eq_zero, ite_mul, one_mul, zero_mul, range_one, sum_singleton]
    grind
  | succ n hn =>
    simp_rw [sumRewards_add_one (t := n + 1), pullCount_add_one (t := n + 1)]
    split_ifs with ha
    · conv_rhs => rw [sum_range_succ]
      simp only [Nat.cast_add, Nat.cast_one, ha, ↓reduceIte, add_mul, one_mul]
      grind
    · simp only [add_zero, hn]
      conv_rhs => rw [sum_range_succ]
      simp [ha]

`measurable_sumRewards`🔗

LemmaLearning.measurable_sumRewards

Details

No docstring.

theorem

Learning.measurable_sumRewards.{u_1, u_3} {𝓐 : Type u_1} {Ω : Type u_3}
  {m𝓐 : MeasurableSpace 𝓐} {mΩ : MeasurableSpace Ω} [DecidableEq 𝓐]
  {A : ℕ → Ω → 𝓐} [MeasurableSingletonClass 𝓐] {R' : ℕ → Ω → ℝ}
  (hA : ∀ (n : ℕ), Measurable (A n))
  (hR' : ∀ (n : ℕ), Measurable (R' n)) (a : 𝓐) (t : ℕ) :
  Measurable (sumRewards A R' a t)
Learning.measurable_sumRewards.{u_1, u_3}
  {𝓐 : Type u_1} {Ω : Type u_3}
  {m𝓐 : MeasurableSpace 𝓐}
  {mΩ : MeasurableSpace Ω} [DecidableEq 𝓐]
  {A : ℕ → Ω → 𝓐}
  [MeasurableSingletonClass 𝓐]
  {R' : ℕ → Ω → ℝ}
  (hA : ∀ (n : ℕ), Measurable (A n))
  (hR' : ∀ (n : ℕ), Measurable (R' n))
  (a : 𝓐) (t : ℕ) :
  Measurable (sumRewards A R' a t)

Code

lemma measurable_sumRewards [MeasurableSingletonClass 𝓐] {R' : ℕ → Ω → ℝ}
    (hA : ∀ n, Measurable (A n)) (hR' : ∀ n, Measurable (R' n)) (a : 𝓐) (t : ℕ) :
    Measurable (sumRewards A R' a t)

Type uses (1)

sumRewards

Used by (6)

Actions: Source · Open Issue

Proof

by
  unfold sumRewards
  have h_meas s : Measurable (fun h : Ω ↦ if A s h = a then R' s h else 0) := by
    refine Measurable.ite ?_ (by fun_prop) (by fun_prop)
    exact (measurableSet_singleton _).preimage (by fun_prop)
  fun_prop

`measurable_uncurry_sumRewards_comp`🔗

LemmaLearning.measurable_uncurry_sumRewards_comp

Details

No docstring.

theorem

Learning.measurable_uncurry_sumRewards_comp.{u_1, u_3} {𝓐 : Type u_1}
  {Ω : Type u_3} {m𝓐 : MeasurableSpace 𝓐} {mΩ : MeasurableSpace Ω}
  [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} [Countable 𝓐]
  [MeasurableSingletonClass 𝓐] {R' : ℕ → Ω → ℝ}
  (hA : ∀ (n : ℕ), Measurable (A n))
  (hR' : ∀ (n : ℕ), Measurable (R' n)) {f : Ω → 𝓐} (hf : Measurable f)
  {g : Ω → ℕ} (hg : Measurable g) :
  Measurable fun ω => sumRewards A R' (f ω) (g ω) ω
Learning.measurable_uncurry_sumRewards_comp.{u_1,
    u_3}
  {𝓐 : Type u_1} {Ω : Type u_3}
  {m𝓐 : MeasurableSpace 𝓐}
  {mΩ : MeasurableSpace Ω} [DecidableEq 𝓐]
  {A : ℕ → Ω → 𝓐} [Countable 𝓐]
  [MeasurableSingletonClass 𝓐]
  {R' : ℕ → Ω → ℝ}
  (hA : ∀ (n : ℕ), Measurable (A n))
  (hR' : ∀ (n : ℕ), Measurable (R' n))
  {f : Ω → 𝓐} (hf : Measurable f)
  {g : Ω → ℕ} (hg : Measurable g) :
  Measurable fun ω =>
    sumRewards A R' (f ω) (g ω) ω

Code

lemma measurable_uncurry_sumRewards_comp [Countable 𝓐] [MeasurableSingletonClass 𝓐]
    {R' : ℕ → Ω → ℝ} (hA : ∀ n, Measurable (A n)) (hR' : ∀ n, Measurable (R' n)) {f : Ω → 𝓐}
    (hf : Measurable f) {g : Ω → ℕ} (hg : Measurable g) :
    Measurable (fun ω ↦ sumRewards A R' (f ω) (g ω) ω)

Type uses (1)

sumRewards

Body uses (1)

measurable_sumRewards

Used by (2)

Actions: Source · Open Issue

Proof

by
  change Measurable ((fun aω ↦ sumRewards A R' aω.1 (g aω.2) aω.2) ∘ fun ω ↦ (f ω, ω))
  apply Measurable.comp _ (by fun_prop)
  refine measurable_from_prod_countable_right fun a ↦ ?_
  change Measurable ((fun tω ↦ sumRewards A R' a tω.1 tω.2) ∘ fun ω ↦ (g ω, ω))
  apply Measurable.comp _ (by fun_prop)
  exact measurable_from_prod_countable_right (fun t ↦ measurable_sumRewards hA hR' a t)

`measurable_empMean`🔗

LemmaLearning.measurable_empMean

Details

No docstring.

theorem

Learning.measurable_empMean.{u_1, u_3} {𝓐 : Type u_1} {Ω : Type u_3}
  {m𝓐 : MeasurableSpace 𝓐} {mΩ : MeasurableSpace Ω} [DecidableEq 𝓐]
  {A : ℕ → Ω → 𝓐} [MeasurableSingletonClass 𝓐] {R' : ℕ → Ω → ℝ}
  (hA : ∀ (n : ℕ), Measurable (A n))
  (hR' : ∀ (n : ℕ), Measurable (R' n)) (a : 𝓐) (n : ℕ) :
  Measurable (empMean A R' a n)
Learning.measurable_empMean.{u_1, u_3}
  {𝓐 : Type u_1} {Ω : Type u_3}
  {m𝓐 : MeasurableSpace 𝓐}
  {mΩ : MeasurableSpace Ω} [DecidableEq 𝓐]
  {A : ℕ → Ω → 𝓐}
  [MeasurableSingletonClass 𝓐]
  {R' : ℕ → Ω → ℝ}
  (hA : ∀ (n : ℕ), Measurable (A n))
  (hR' : ∀ (n : ℕ), Measurable (R' n))
  (a : 𝓐) (n : ℕ) :
  Measurable (empMean A R' a n)

Code

lemma measurable_empMean [MeasurableSingletonClass 𝓐] {R' : ℕ → Ω → ℝ} (hA : ∀ n, Measurable (A n))
    (hR' : ∀ n, Measurable (R' n)) (a : 𝓐) (n : ℕ) :
    Measurable (empMean A R' a n)

Type uses (1)

empMean

Body uses (4)

Used by (3)

Actions: Source · Open Issue

Proof

by
  unfold empMean
  fun_prop

`measurable_uncurry_empMean_comp`🔗

LemmaLearning.measurable_uncurry_empMean_comp

Details

No docstring.

theorem

Learning.measurable_uncurry_empMean_comp.{u_1, u_3} {𝓐 : Type u_1}
  {Ω : Type u_3} {m𝓐 : MeasurableSpace 𝓐} {mΩ : MeasurableSpace Ω}
  [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} [Countable 𝓐]
  [MeasurableSingletonClass 𝓐] {R' : ℕ → Ω → ℝ}
  (hA : ∀ (n : ℕ), Measurable (A n))
  (hR' : ∀ (n : ℕ), Measurable (R' n)) {f : Ω → 𝓐} (hf : Measurable f)
  {g : Ω → ℕ} (hg : Measurable g) :
  Measurable fun ω => empMean A R' (f ω) (g ω) ω
Learning.measurable_uncurry_empMean_comp.{u_1,
    u_3}
  {𝓐 : Type u_1} {Ω : Type u_3}
  {m𝓐 : MeasurableSpace 𝓐}
  {mΩ : MeasurableSpace Ω} [DecidableEq 𝓐]
  {A : ℕ → Ω → 𝓐} [Countable 𝓐]
  [MeasurableSingletonClass 𝓐]
  {R' : ℕ → Ω → ℝ}
  (hA : ∀ (n : ℕ), Measurable (A n))
  (hR' : ∀ (n : ℕ), Measurable (R' n))
  {f : Ω → 𝓐} (hf : Measurable f)
  {g : Ω → ℕ} (hg : Measurable g) :
  Measurable fun ω =>
    empMean A R' (f ω) (g ω) ω

Code

lemma measurable_uncurry_empMean_comp [Countable 𝓐] [MeasurableSingletonClass 𝓐] {R' : ℕ → Ω → ℝ}
    (hA : ∀ n, Measurable (A n)) (hR' : ∀ n, Measurable (R' n)) {f : Ω → 𝓐} (hf : Measurable f)
    {g : Ω → ℕ} (hg : Measurable g) :
    Measurable (fun ω ↦ empMean A R' (f ω) (g ω) ω)

Type uses (1)

empMean

Body uses (4)

Used by (1)

integral_sum_range_actionMean_bestAction_sub_ucb_bestAction_le

Actions: Source · Open Issue

Proof

by
  unfold empMean
  fun_prop

`measurable_sumRewards'`🔗

LemmaLearning.measurable_sumRewards'

Details

No docstring.

theorem

Learning.measurable_sumRewards'.{u_1} {𝓐 : Type u_1}
  {m𝓐 : MeasurableSpace 𝓐} [DecidableEq 𝓐] [MeasurableSingletonClass 𝓐]
  (n : ℕ) (a : 𝓐) : Measurable fun h => sumRewards' n h a
Learning.measurable_sumRewards'.{u_1}
  {𝓐 : Type u_1} {m𝓐 : MeasurableSpace 𝓐}
  [DecidableEq 𝓐]
  [MeasurableSingletonClass 𝓐] (n : ℕ)
  (a : 𝓐) :
  Measurable fun h => sumRewards' n h a

Code

lemma measurable_sumRewards' [MeasurableSingletonClass 𝓐] (n : ℕ) (a : 𝓐) :
    Measurable (fun h ↦ sumRewards' n h a)

Type uses (1)

sumRewards'

Used by (1)

measurable_empMean'

Actions: Source · Open Issue

Proof

by
  simp_rw [sumRewards']
  have h_meas s : Measurable (fun (h : Iic n → 𝓐 × ℝ) ↦ if (h s).1 = a then (h s).2 else 0) := by
    refine Measurable.ite ?_ (by fun_prop) (by fun_prop)
    exact (measurableSet_singleton _).preimage (by fun_prop)
  fun_prop

`measurable_uncurry_sumRewards'`🔗

LemmaLearning.measurable_uncurry_sumRewards'

Details

No docstring.

theorem

Learning.measurable_uncurry_sumRewards'.{u_1} {𝓐 : Type u_1}
  {m𝓐 : MeasurableSpace 𝓐} [DecidableEq 𝓐] [MeasurableEq 𝓐] (n : ℕ) :
  Measurable fun p => sumRewards' n (Prod.fst p) (Prod.snd p)
Learning.measurable_uncurry_sumRewards'.{u_1}
  {𝓐 : Type u_1} {m𝓐 : MeasurableSpace 𝓐}
  [DecidableEq 𝓐] [MeasurableEq 𝓐]
  (n : ℕ) :
  Measurable fun p =>
    sumRewards' n (Prod.fst p)
      (Prod.snd p)

Code

lemma measurable_uncurry_sumRewards' [MeasurableEq 𝓐] (n : ℕ) :
    Measurable (fun p : (Iic n → 𝓐 × ℝ) × 𝓐 ↦ sumRewards' n p.1 p.2)

Type uses (1)

sumRewards'

Used by (1)

measurable_uncurry_empMean'

Actions: Source · Open Issue

Proof

by
  simp_rw [sumRewards']
  have h_meas s : Measurable (fun p : (Iic n → 𝓐 × ℝ) × 𝓐 ↦
      if (p.1 s).1 = p.2 then (p.1 s).2 else 0) := by
    refine Measurable.ite ?_ (by fun_prop) (by fun_prop)
    exact measurableSet_eq_fun (by fun_prop) (by fun_prop)
  fun_prop

`measurable_empMean'`🔗

LemmaLearning.measurable_empMean'

Details

No docstring.

theorem

Learning.measurable_empMean'.{u_1} {𝓐 : Type u_1}
  {m𝓐 : MeasurableSpace 𝓐} [DecidableEq 𝓐] [MeasurableSingletonClass 𝓐]
  (n : ℕ) (a : 𝓐) : Measurable fun h => empMean' n h a
Learning.measurable_empMean'.{u_1}
  {𝓐 : Type u_1} {m𝓐 : MeasurableSpace 𝓐}
  [DecidableEq 𝓐]
  [MeasurableSingletonClass 𝓐] (n : ℕ)
  (a : 𝓐) :
  Measurable fun h => empMean' n h a

Code

lemma measurable_empMean' [MeasurableSingletonClass 𝓐] (n : ℕ) (a : 𝓐) :
    Measurable (fun h ↦ empMean' n h a)

Type uses (1)

empMean'

Body uses (4)

Used by (2)

Actions: Source · Open Issue

Proof

by
  unfold empMean'
  fun_prop

`measurable_uncurry_empMean'`🔗

LemmaLearning.measurable_uncurry_empMean'

Details

No docstring.

theorem

Learning.measurable_uncurry_empMean'.{u_1} {𝓐 : Type u_1}
  {m𝓐 : MeasurableSpace 𝓐} [DecidableEq 𝓐] [MeasurableEq 𝓐] (n : ℕ) :
  Measurable fun p => empMean' n (Prod.fst p) (Prod.snd p)
Learning.measurable_uncurry_empMean'.{u_1}
  {𝓐 : Type u_1} {m𝓐 : MeasurableSpace 𝓐}
  [DecidableEq 𝓐] [MeasurableEq 𝓐]
  (n : ℕ) :
  Measurable fun p =>
    empMean' n (Prod.fst p) (Prod.snd p)

Code

lemma measurable_uncurry_empMean' [MeasurableEq 𝓐] (n : ℕ) :
    Measurable (fun p : (Iic n → 𝓐 × ℝ) × 𝓐 ↦ empMean' n p.1 p.2)

Type uses (1)

empMean'

Body uses (4)

Used by (1)

measurable_uncurry_ucb'

Actions: Source · Open Issue

Proof

by
  unfold empMean'
  fun_prop

`isPredictable_sumRewards`🔗

LemmaLearning.IsAlgEnvSeq.isPredictable_sumRewards

Details

No docstring.

theorem

Learning.IsAlgEnvSeq.isPredictable_sumRewards.{u_1, u_3} {𝓐 : Type u_1}
  {Ω : Type u_3} {m𝓐 : MeasurableSpace 𝓐} {mΩ : MeasurableSpace Ω}
  [DecidableEq 𝓐] {P : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure P] {A : ℕ → Ω → 𝓐}
  [StandardBorelSpace 𝓐] {R' : ℕ → Ω → ℝ} {alg : Algorithm 𝓐 ℝ}
  {env : Environment 𝓐 ℝ} (h : IsAlgEnvSeq A R' alg env P) (a : 𝓐) :
  MeasureTheory.IsStronglyPredictable (filtration ⋯ ⋯)
    (sumRewards A R' a)
Learning.IsAlgEnvSeq.isPredictable_sumRewards.{u_1,
    u_3}
  {𝓐 : Type u_1} {Ω : Type u_3}
  {m𝓐 : MeasurableSpace 𝓐}
  {mΩ : MeasurableSpace Ω} [DecidableEq 𝓐]
  {P : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure P]
  {A : ℕ → Ω → 𝓐} [StandardBorelSpace 𝓐]
  {R' : ℕ → Ω → ℝ} {alg : Algorithm 𝓐 ℝ}
  {env : Environment 𝓐 ℝ}
  (h : IsAlgEnvSeq A R' alg env P)
  (a : 𝓐) :
  MeasureTheory.IsStronglyPredictable
    (filtration ⋯ ⋯) (sumRewards A R' a)

Code

lemma IsAlgEnvSeq.isPredictable_sumRewards [StandardBorelSpace 𝓐] {R' : ℕ → Ω → ℝ}
    {alg : Algorithm 𝓐 ℝ} {env : Environment 𝓐 ℝ}
    (h : IsAlgEnvSeq A R' alg env P) (a : 𝓐) :
    IsStronglyPredictable (IsAlgEnvSeq.filtration h.measurable_action h.measurable_feedback)
      (sumRewards A R' a)

Type uses (5)

Body uses (3)

Used by (2)

Actions: Source · Open Issue

Proof

by
  rw [IsStronglyPredictable.iff_measurable_add_one]
  constructor
  · simp only [sumRewards_zero]
    fun_prop
  refine fun n ↦ Measurable.stronglyMeasurable ?_
  refine measurable_fun_sum _ fun i hi ↦ Measurable.ite ?_ ?_ (by fun_prop)
  · refine (measurableSet_singleton a).preimage ?_
    have h_meas_i := IsAlgEnvSeq.adapted_action h.measurable_action h.measurable_feedback i
    simp only [mem_range] at hi
    exact h_meas_i.mono ((IsAlgEnvSeq.filtration h.measurable_action h.measurable_feedback).mono
      (by lia)) le_rfl
  · have h_meas_i := IsAlgEnvSeq.adapted_feedback h.measurable_action h.measurable_feedback i
    simp only [mem_range] at hi
    exact h_meas_i.mono ((IsAlgEnvSeq.filtration h.measurable_action h.measurable_feedback).mono
      (by lia)) le_rfl

`stronglyAdapted_sumRewards_add_one`🔗

LemmaLearning.IsAlgEnvSeq.stronglyAdapted_sumRewards_add_one

Details

No docstring.

theorem

Learning.IsAlgEnvSeq.stronglyAdapted_sumRewards_add_one.{u_1, u_3}
  {𝓐 : Type u_1} {Ω : Type u_3} {m𝓐 : MeasurableSpace 𝓐}
  {mΩ : MeasurableSpace Ω} [DecidableEq 𝓐] {P : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure P] {A : ℕ → Ω → 𝓐}
  [StandardBorelSpace 𝓐] {R' : ℕ → Ω → ℝ} {alg : Algorithm 𝓐 ℝ}
  {env : Environment 𝓐 ℝ} (h : IsAlgEnvSeq A R' alg env P) (a : 𝓐) :
  MeasureTheory.StronglyAdapted (filtration ⋯ ⋯) fun n =>
    sumRewards A R' a (n + 1)
Learning.IsAlgEnvSeq.stronglyAdapted_sumRewards_add_one.{u_1,
    u_3}
  {𝓐 : Type u_1} {Ω : Type u_3}
  {m𝓐 : MeasurableSpace 𝓐}
  {mΩ : MeasurableSpace Ω} [DecidableEq 𝓐]
  {P : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure P]
  {A : ℕ → Ω → 𝓐} [StandardBorelSpace 𝓐]
  {R' : ℕ → Ω → ℝ} {alg : Algorithm 𝓐 ℝ}
  {env : Environment 𝓐 ℝ}
  (h : IsAlgEnvSeq A R' alg env P)
  (a : 𝓐) :
  MeasureTheory.StronglyAdapted
    (filtration ⋯ ⋯) fun n =>
    sumRewards A R' a (n + 1)

Code

lemma IsAlgEnvSeq.stronglyAdapted_sumRewards_add_one [StandardBorelSpace 𝓐]
    {R' : ℕ → Ω → ℝ} {alg : Algorithm 𝓐 ℝ} {env : Environment 𝓐 ℝ}
    (h : IsAlgEnvSeq A R' alg env P) (a : 𝓐) :
    StronglyAdapted (IsAlgEnvSeq.filtration h.measurable_action h.measurable_feedback)
      (fun n ↦ sumRewards A R' a (n + 1))

Type uses (5)

Body uses (1)

isPredictable_sumRewards

Used by (1)

adapted_sumRewards_add_one

Actions: Source · Open Issue

Proof

by
  have h_predictable := h.isPredictable_sumRewards a
  rw [IsStronglyPredictable.iff_measurable_add_one] at h_predictable
  exact h_predictable.2

`adapted_sumRewards_add_one`🔗

LemmaLearning.IsAlgEnvSeq.adapted_sumRewards_add_one

Details

No docstring.

theorem

Learning.IsAlgEnvSeq.adapted_sumRewards_add_one.{u_1, u_3}
  {𝓐 : Type u_1} {Ω : Type u_3} {m𝓐 : MeasurableSpace 𝓐}
  {mΩ : MeasurableSpace Ω} [DecidableEq 𝓐] {P : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure P] {A : ℕ → Ω → 𝓐}
  [StandardBorelSpace 𝓐] {R' : ℕ → Ω → ℝ} {alg : Algorithm 𝓐 ℝ}
  {env : Environment 𝓐 ℝ} (h : IsAlgEnvSeq A R' alg env P) (a : 𝓐) :
  MeasureTheory.Adapted (filtration ⋯ ⋯) fun n =>
    sumRewards A R' a (n + 1)
Learning.IsAlgEnvSeq.adapted_sumRewards_add_one.{u_1,
    u_3}
  {𝓐 : Type u_1} {Ω : Type u_3}
  {m𝓐 : MeasurableSpace 𝓐}
  {mΩ : MeasurableSpace Ω} [DecidableEq 𝓐]
  {P : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure P]
  {A : ℕ → Ω → 𝓐} [StandardBorelSpace 𝓐]
  {R' : ℕ → Ω → ℝ} {alg : Algorithm 𝓐 ℝ}
  {env : Environment 𝓐 ℝ}
  (h : IsAlgEnvSeq A R' alg env P)
  (a : 𝓐) :
  MeasureTheory.Adapted (filtration ⋯ ⋯)
    fun n => sumRewards A R' a (n + 1)

Code

lemma IsAlgEnvSeq.adapted_sumRewards_add_one [StandardBorelSpace 𝓐] {R' : ℕ → Ω → ℝ}
    {alg : Algorithm 𝓐 ℝ} {env : Environment 𝓐 ℝ}
    (h : IsAlgEnvSeq A R' alg env P) (a : 𝓐) :
    Adapted (IsAlgEnvSeq.filtration h.measurable_action h.measurable_feedback)
      (fun n ↦ sumRewards A R' a (n + 1))

Type uses (5)

Body uses (1)

stronglyAdapted_sumRewards_add_one

Actions: Source · Open Issue

Proof

(h.stronglyAdapted_sumRewards_add_one a).adapted

`div₀'`🔗

LemmaMeasureTheory.StronglyMeasurable.div₀'

Details

No docstring.

theorem

MeasureTheory.StronglyMeasurable.div₀'.{u_4, u_5} {𝓐 : Type u_4}
  {β : Type u_5} {m𝓐 : MeasurableSpace 𝓐} [TopologicalSpace β]
  [GroupWithZero β] [ContinuousMul β] [ContinuousInv₀ β]
  [TopologicalSpace.PseudoMetrizableSpace β] [MeasurableSpace β]
  [BorelSpace β] [MeasurableSingletonClass β] {f g : 𝓐 → β}
  (hf : StronglyMeasurable f) (hg : StronglyMeasurable g) :
  StronglyMeasurable (f / g)
MeasureTheory.StronglyMeasurable.div₀'.{u_4,
    u_5}
  {𝓐 : Type u_4} {β : Type u_5}
  {m𝓐 : MeasurableSpace 𝓐}
  [TopologicalSpace β] [GroupWithZero β]
  [ContinuousMul β] [ContinuousInv₀ β]
  [TopologicalSpace.PseudoMetrizableSpace
      β]
  [MeasurableSpace β] [BorelSpace β]
  [MeasurableSingletonClass β]
  {f g : 𝓐 → β}
  (hf : StronglyMeasurable f)
  (hg : StronglyMeasurable g) :
  StronglyMeasurable (f / g)

Code

lemma _root_.MeasureTheory.StronglyMeasurable.div₀' {𝓐 β : Type*}
    {m𝓐 : MeasurableSpace 𝓐} [TopologicalSpace β]
    [GroupWithZero β] [ContinuousMul β] [ContinuousInv₀ β]
    [TopologicalSpace.PseudoMetrizableSpace β]
    [MeasurableSpace β] [BorelSpace β] [MeasurableSingletonClass β]
    {f g : 𝓐 → β} (hf : StronglyMeasurable f) (hg : StronglyMeasurable g) :
    StronglyMeasurable (f / g)

Used by (1)

isPredictable_empMean

Actions: Source · Open Issue

Proof

by
  refine ⟨fun n => hf.approx n / (hg.approx n).restrict {x | g x ≠ 0}, fun x => ?_⟩
  have : MeasurableSet {x | g x ≠ 0} := ((MeasurableSet.singleton 0).preimage hg.measurable).compl
  by_cases h : g x = 0
  · simp_all only [ne_eq, SimpleFunc.coe_div, SimpleFunc.coe_restrict, Pi.div_apply, mem_setOf_eq,
      not_true_eq_false, not_false_eq_true, indicator_of_notMem, _root_.div_zero]
    exact tendsto_const_nhds
  · simp_all only [ne_eq, SimpleFunc.coe_div, SimpleFunc.coe_restrict,
      Pi.div_apply, mem_setOf_eq, not_false_eq_true, indicator_of_mem]
    exact (hf.tendsto_approx x).div (hg.tendsto_approx x) h

`isPredictable_empMean`🔗

LemmaLearning.IsAlgEnvSeq.isPredictable_empMean

Details

No docstring.

theorem

Learning.IsAlgEnvSeq.isPredictable_empMean.{u_1, u_3} {𝓐 : Type u_1}
  {Ω : Type u_3} {m𝓐 : MeasurableSpace 𝓐} {mΩ : MeasurableSpace Ω}
  [DecidableEq 𝓐] {P : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure P] {A : ℕ → Ω → 𝓐}
  [StandardBorelSpace 𝓐] {R' : ℕ → Ω → ℝ} {alg : Algorithm 𝓐 ℝ}
  {env : Environment 𝓐 ℝ} (h : IsAlgEnvSeq A R' alg env P) (a : 𝓐) :
  MeasureTheory.IsStronglyPredictable (filtration ⋯ ⋯) (empMean A R' a)
Learning.IsAlgEnvSeq.isPredictable_empMean.{u_1,
    u_3}
  {𝓐 : Type u_1} {Ω : Type u_3}
  {m𝓐 : MeasurableSpace 𝓐}
  {mΩ : MeasurableSpace Ω} [DecidableEq 𝓐]
  {P : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure P]
  {A : ℕ → Ω → 𝓐} [StandardBorelSpace 𝓐]
  {R' : ℕ → Ω → ℝ} {alg : Algorithm 𝓐 ℝ}
  {env : Environment 𝓐 ℝ}
  (h : IsAlgEnvSeq A R' alg env P)
  (a : 𝓐) :
  MeasureTheory.IsStronglyPredictable
    (filtration ⋯ ⋯) (empMean A R' a)

Code

lemma IsAlgEnvSeq.isPredictable_empMean [StandardBorelSpace 𝓐] {R' : ℕ → Ω → ℝ}
    {alg : Algorithm 𝓐 ℝ} {env : Environment 𝓐 ℝ}
    (h : IsAlgEnvSeq A R' alg env P) (a : 𝓐) :
    IsStronglyPredictable (IsAlgEnvSeq.filtration h.measurable_action h.measurable_feedback)
      (empMean A R' a)

Type uses (5)

Body uses (5)

Used by (1)

stronglyAdapted_empMean_add_one

Actions: Source · Open Issue

Proof

by
  unfold empMean
  refine StronglyMeasurable.div₀' ?_ ?_
  · exact h.isPredictable_sumRewards a
  · have h_meas := (isPredictable_pullCount h.measurable_action h.measurable_feedback a).measurable
    fun_prop

`stronglyAdapted_empMean_add_one`🔗

LemmaLearning.IsAlgEnvSeq.stronglyAdapted_empMean_add_one

Details

No docstring.

theorem

Learning.IsAlgEnvSeq.stronglyAdapted_empMean_add_one.{u_1, u_3}
  {𝓐 : Type u_1} {Ω : Type u_3} {m𝓐 : MeasurableSpace 𝓐}
  {mΩ : MeasurableSpace Ω} [DecidableEq 𝓐] {P : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure P] {A : ℕ → Ω → 𝓐}
  [StandardBorelSpace 𝓐] {R' : ℕ → Ω → ℝ} {alg : Algorithm 𝓐 ℝ}
  {env : Environment 𝓐 ℝ} (h : IsAlgEnvSeq A R' alg env P) (a : 𝓐) :
  MeasureTheory.StronglyAdapted (filtration ⋯ ⋯) fun n =>
    empMean A R' a (n + 1)
Learning.IsAlgEnvSeq.stronglyAdapted_empMean_add_one.{u_1,
    u_3}
  {𝓐 : Type u_1} {Ω : Type u_3}
  {m𝓐 : MeasurableSpace 𝓐}
  {mΩ : MeasurableSpace Ω} [DecidableEq 𝓐]
  {P : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure P]
  {A : ℕ → Ω → 𝓐} [StandardBorelSpace 𝓐]
  {R' : ℕ → Ω → ℝ} {alg : Algorithm 𝓐 ℝ}
  {env : Environment 𝓐 ℝ}
  (h : IsAlgEnvSeq A R' alg env P)
  (a : 𝓐) :
  MeasureTheory.StronglyAdapted
    (filtration ⋯ ⋯) fun n =>
    empMean A R' a (n + 1)

Code

lemma IsAlgEnvSeq.stronglyAdapted_empMean_add_one [StandardBorelSpace 𝓐]
    {R' : ℕ → Ω → ℝ} {alg : Algorithm 𝓐 ℝ} {env : Environment 𝓐 ℝ}
    (h : IsAlgEnvSeq A R' alg env P) (a : 𝓐) :
    StronglyAdapted (IsAlgEnvSeq.filtration h.measurable_action h.measurable_feedback)
      (fun n ↦ empMean A R' a (n + 1))

Type uses (5)

Body uses (1)

isPredictable_empMean

Used by (1)

adapted_empMean_add_one

Actions: Source · Open Issue

Proof

by
  have h_predictable := h.isPredictable_empMean a
  rw [IsStronglyPredictable.iff_measurable_add_one] at h_predictable
  exact h_predictable.2

`adapted_empMean_add_one`🔗

LemmaLearning.IsAlgEnvSeq.adapted_empMean_add_one

Details

No docstring.

theorem

Learning.IsAlgEnvSeq.adapted_empMean_add_one.{u_1, u_3} {𝓐 : Type u_1}
  {Ω : Type u_3} {m𝓐 : MeasurableSpace 𝓐} {mΩ : MeasurableSpace Ω}
  [DecidableEq 𝓐] {P : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure P] {A : ℕ → Ω → 𝓐}
  [StandardBorelSpace 𝓐] {R' : ℕ → Ω → ℝ} {alg : Algorithm 𝓐 ℝ}
  {env : Environment 𝓐 ℝ} (h : IsAlgEnvSeq A R' alg env P) (a : 𝓐) :
  MeasureTheory.Adapted (filtration ⋯ ⋯) fun n => empMean A R' a (n + 1)
Learning.IsAlgEnvSeq.adapted_empMean_add_one.{u_1,
    u_3}
  {𝓐 : Type u_1} {Ω : Type u_3}
  {m𝓐 : MeasurableSpace 𝓐}
  {mΩ : MeasurableSpace Ω} [DecidableEq 𝓐]
  {P : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure P]
  {A : ℕ → Ω → 𝓐} [StandardBorelSpace 𝓐]
  {R' : ℕ → Ω → ℝ} {alg : Algorithm 𝓐 ℝ}
  {env : Environment 𝓐 ℝ}
  (h : IsAlgEnvSeq A R' alg env P)
  (a : 𝓐) :
  MeasureTheory.Adapted (filtration ⋯ ⋯)
    fun n => empMean A R' a (n + 1)

Code

lemma IsAlgEnvSeq.adapted_empMean_add_one [StandardBorelSpace 𝓐] {R' : ℕ → Ω → ℝ}
    {alg : Algorithm 𝓐 ℝ} {env : Environment 𝓐 ℝ}
    (h : IsAlgEnvSeq A R' alg env P) (a : 𝓐) :
    Adapted (IsAlgEnvSeq.filtration h.measurable_action h.measurable_feedback)
      (fun n ↦ empMean A R' a (n + 1))

Type uses (5)

Body uses (1)

stronglyAdapted_empMean_add_one

Actions: Source · Open Issue

Proof

(h.stronglyAdapted_empMean_add_one a).adapted

3.1. SequentialLearning.FiniteActions🔗

pullCount🔗

pullCount'🔗

pullCount_zero🔗

pullCount_zero_apply🔗

pullCount_one🔗

monotone_pullCount🔗

pullCount_mono🔗

pullCount_action_eq_pullCount_add_one🔗

pullCount_eq_pullCount_of_action_ne🔗

pullCount_add_one🔗

pullCount_eq_sum🔗

pullCount'_eq_sum🔗

pullCount_add_one_eq_pullCount'🔗

pullCount_eq_pullCount'🔗

pullCount'_mono🔗

pullCount_le🔗

pullCount_congr🔗

pullCount_lt_of_forall_ne🔗

exists_pullCount_eq_of_le🔗

pullCount_le_add🔗

measurable_pullCount🔗

measurable_uncurry_pullCount🔗

measurable_uncurry_pullCount_comp🔗

measurable_pullCount'🔗

measurable_uncurry_pullCount'🔗

adapted_pullCount_add_one🔗

stronglyAdapted_pullCount_add_one🔗

isPredictable_pullCount🔗

integrable_pullCount🔗

stepsUntil🔗

stepsUntil_eq_top_iff🔗

stepsUntil_ne_top🔗

exists_pullCount_eq🔗

stepsUntil_zero_of_ne🔗

stepsUntil_zero_of_eq🔗

stepsUntil_eq_dite🔗

stepsUntil_eq_leastGE🔗

stepsUntil_mono🔗

stepsUntil_pullCount_le🔗

stepsUntil_pullCount_eq🔗

stepsUntil_one_of_eq🔗

stepsUntil_eq_zero_iff🔗

action_stepsUntil🔗

action_eq_of_stepsUntil_eq_coe🔗

pullCount_stepsUntil_add_one🔗

pullCount_stepsUntil🔗

pullCount_lt_of_le_stepsUntil🔗

pullCount_eq_of_stepsUntil_eq_coe🔗

pullCount_add_one_eq_of_stepsUntil_eq_coe🔗

stepsUntil_eq_iff🔗

stepsUntil_eq_iff'🔗

stepsUntil_eq_congr🔗

isStoppingTime_stepsUntil🔗

measurable_stepsUntil🔗

measurable_stepsUntil'🔗

measurable_comap_indicator_stepsUntil_eq🔗

measurable_indicator_stepsUntil_eq🔗

measurableSet_stepsUntil_eq_zero🔗

measurable_comap_indicator_stepsUntil_eq_zero🔗

measurableSet_stepsUntil_eq🔗

isStoppingTime_stepsUntil_filtrationAction🔗

rewardByCount🔗

rewardByCount_eq_ite🔗

rewardByCount_eq_add🔗

rewardByCount_of_stepsUntil_eq_top🔗

rewardByCount_of_stepsUntil_ne_top🔗

rewardByCount_eq_stoppedValue🔗

rewardByCount_of_stepsUntil_eq_coe🔗

rewardByCount_zero🔗

rewardByCount_pullCount_add_one_eq_reward🔗

measurable_rewardByCount🔗

sum_pullCount_mul🔗

sum_pullCount🔗

sum_comp_pullCount🔗

sumRewards🔗

sumRewards'🔗

empMean🔗

empMean'🔗

sumRewards_zero🔗

`pullCount`🔗

`pullCount'`🔗

`pullCount_zero`🔗

`pullCount_zero_apply`🔗

`pullCount_one`🔗

`monotone_pullCount`🔗

`pullCount_mono`🔗

`pullCount_action_eq_pullCount_add_one`🔗

`pullCount_eq_pullCount_of_action_ne`🔗

`pullCount_add_one`🔗

`pullCount_eq_sum`🔗

`pullCount'_eq_sum`🔗

`pullCount_add_one_eq_pullCount'`🔗

`pullCount_eq_pullCount'`🔗

`pullCount'_mono`🔗

`pullCount_le`🔗

`pullCount_congr`🔗

`pullCount_lt_of_forall_ne`🔗

`exists_pullCount_eq_of_le`🔗

`pullCount_le_add`🔗

`measurable_pullCount`🔗

`measurable_uncurry_pullCount`🔗

`measurable_uncurry_pullCount_comp`🔗

`measurable_pullCount'`🔗

`measurable_uncurry_pullCount'`🔗

`adapted_pullCount_add_one`🔗

`stronglyAdapted_pullCount_add_one`🔗

`isPredictable_pullCount`🔗

`integrable_pullCount`🔗

`stepsUntil`🔗

`stepsUntil_eq_top_iff`🔗

`stepsUntil_ne_top`🔗

`exists_pullCount_eq`🔗

`stepsUntil_zero_of_ne`🔗

`stepsUntil_zero_of_eq`🔗

`stepsUntil_eq_dite`🔗

`stepsUntil_eq_leastGE`🔗

`stepsUntil_mono`🔗

`stepsUntil_pullCount_le`🔗

`stepsUntil_pullCount_eq`🔗

`stepsUntil_one_of_eq`🔗

`stepsUntil_eq_zero_iff`🔗

`action_stepsUntil`🔗

`action_eq_of_stepsUntil_eq_coe`🔗

`pullCount_stepsUntil_add_one`🔗

`pullCount_stepsUntil`🔗

`pullCount_lt_of_le_stepsUntil`🔗

`pullCount_eq_of_stepsUntil_eq_coe`🔗

`pullCount_add_one_eq_of_stepsUntil_eq_coe`🔗

`stepsUntil_eq_iff`🔗

`stepsUntil_eq_iff'`🔗

`stepsUntil_eq_congr`🔗

`isStoppingTime_stepsUntil`🔗

`measurable_stepsUntil`🔗

`measurable_stepsUntil'`🔗

`measurable_comap_indicator_stepsUntil_eq`🔗

`measurable_indicator_stepsUntil_eq`🔗

`measurableSet_stepsUntil_eq_zero`🔗

`measurable_comap_indicator_stepsUntil_eq_zero`🔗

`measurableSet_stepsUntil_eq`🔗

`isStoppingTime_stepsUntil_filtrationAction`🔗

`rewardByCount`🔗

`rewardByCount_eq_ite`🔗

`rewardByCount_eq_add`🔗

`rewardByCount_of_stepsUntil_eq_top`🔗

`rewardByCount_of_stepsUntil_ne_top`🔗

`rewardByCount_eq_stoppedValue`🔗

`rewardByCount_of_stepsUntil_eq_coe`🔗

`rewardByCount_zero`🔗

`rewardByCount_pullCount_add_one_eq_reward`🔗

`measurable_rewardByCount`🔗

`sum_pullCount_mul`🔗

`sum_pullCount`🔗

`sum_comp_pullCount`🔗

`sumRewards`🔗

`sumRewards'`🔗

`empMean`🔗

`empMean'`🔗

`sumRewards_zero`🔗

`sumRewards_add_one`🔗