Bookkeeping definitions for finite action space sequential learning problems

If the number of actions is finite, it makes sense to define the number of times each action was chosen, the time at which an action was chosen for the nth time, the value of the reward at that time, the sum of rewards obtained for each action, the empirical mean reward for each action, etc.

For each definition that take as arguments a time t : ℕ, a history h : ℕ → 𝓐 × R, and possibly other parameters, we put the time and history at the end in this order, so that the definition can be seen as a stochastic process indexed by time t on the measurable space ℕ → 𝓐 × R.

noncomputable def Learning.pullCount {𝓐 : Type u_2} {Ω : Type u_4} [DecidableEq 𝓐] (A : ℕ → Ω → 𝓐) (a : 𝓐) (t : ℕ) (ω : Ω) : ℕ

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

Equations

• Learning.pullCount A a t ω = {s ∈ Finset.range t | A s ω = a}.card

noncomputable def Learning.pullCount' {𝓞 : Type u_1} {𝓐 : Type u_2} {R : Type u_3} [DecidableEq 𝓐] (n : ℕ) (h : Hist 𝓞 𝓐 R n) (a : 𝓐) : ℕ

Number of pulls of arm a in the history before time n. This is the number of entries in h in which the arm is a.

Equations

• Learning.pullCount' n h a = {s : Fin n | (h s).action = a}.card

@[simp]

theorem Learning.pullCount_zero {𝓐 : Type u_2} {Ω : Type u_4} [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} (a : 𝓐) : pullCount A a 0 = 0

theorem Learning.pullCount_zero_apply {𝓐 : Type u_2} {Ω : Type u_4} [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} (a : 𝓐) (ω : Ω) : pullCount A a 0 ω = 0

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

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

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

theorem Learning.pullCount_action_eq_pullCount_add_one {𝓐 : Type u_2} {Ω : Type u_4} [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} (t : ℕ) (ω : Ω) : pullCount A (A t ω) (t + 1) ω = pullCount A (A t ω) t ω + 1

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

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

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

theorem Learning.pullCount'_eq_sum {𝓞 : Type u_1} {𝓐 : Type u_2} {R : Type u_3} [DecidableEq 𝓐] (n : ℕ) (h : Hist 𝓞 𝓐 R n) (a : 𝓐) : pullCount' n h a = ∑ s : Fin n, if (h s).action = a then 1 else 0

theorem Learning.pullCount_eq_pullCount' {𝓞 : Type u_1} {𝓐 : Type u_2} {R : Type u_3} {Ω : Type u_4} [DecidableEq 𝓐] {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {R' : ℕ → Ω → R} {a : 𝓐} {n : ℕ} {ω : Ω} : pullCount A a n ω = pullCount' n (history O A R' n ω) a

theorem Learning.pullCount_eq_comp_history {𝓞 : Type u_1} {𝓐 : Type u_2} {R : Type u_3} {Ω : Type u_4} [DecidableEq 𝓐] {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {R' : ℕ → Ω → R} (a : 𝓐) (n : ℕ) : pullCount A a n = (fun (h : Hist 𝓞 𝓐 R n) => pullCount' n h a) ∘ history O A R' n

pullCount A a n is a function of the history before time n.

theorem Learning.pullCount'_mono {𝓞 : Type u_1} {𝓐 : Type u_2} {R : Type u_3} {Ω : Type u_4} [DecidableEq 𝓐] {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {R' : ℕ → Ω → R} {a : 𝓐} {ω : Ω} {n m : ℕ} (hnm : n ≤ m) : pullCount' n (history O A R' n ω) a ≤ pullCount' m (history O A R' m ω) a

theorem Learning.pullCount_le {𝓐 : Type u_2} {Ω : Type u_4} [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} (a : 𝓐) (t : ℕ) (ω : Ω) : pullCount A a t ω ≤ t

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

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

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

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

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

theorem Learning.measurable_uncurry_pullCount {𝓐 : Type u_2} {Ω : Type u_4} {m𝓐 : MeasurableSpace 𝓐} {mΩ : MeasurableSpace Ω} [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} [MeasurableEq 𝓐] (hA : ∀ (n : ℕ), Measurable (A n)) (t : ℕ) : Measurable fun (p : Ω × 𝓐) => pullCount A p.2 t p.1

theorem Learning.measurable_uncurry_pullCount_comp {𝓐 : Type u_2} {Ω : Type u_4} {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 ω) ω

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

theorem Learning.measurable_uncurry_pullCount' {𝓞 : Type u_1} {𝓐 : Type u_2} {R : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {mR : MeasurableSpace R} [DecidableEq 𝓐] [MeasurableEq 𝓐] (n : ℕ) : Measurable fun (p : Hist 𝓞 𝓐 R n × 𝓐) => pullCount' n p.1 p.2

theorem Learning.adapted_pullCount_add_one {𝓞 : Type u_1} {𝓐 : Type u_2} {R : Type u_3} {Ω : Type u_4} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {mR : MeasurableSpace R} {mΩ : MeasurableSpace Ω} [DecidableEq 𝓐] {alg : Algorithm 𝓞 𝓐 R} {env : Environment 𝓞 𝓐 R} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {R' : ℕ → Ω → R} [MeasurableSingletonClass 𝓐] (h : IsAlgEnvSeq O A R' alg env P) (a : 𝓐) : MeasureTheory.Adapted h.filtration fun (n : ℕ) => pullCount A a (n + 1)

theorem Learning.stronglyAdapted_pullCount_add_one {𝓞 : Type u_1} {𝓐 : Type u_2} {R : Type u_3} {Ω : Type u_4} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {mR : MeasurableSpace R} {mΩ : MeasurableSpace Ω} [DecidableEq 𝓐] {alg : Algorithm 𝓞 𝓐 R} {env : Environment 𝓞 𝓐 R} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {R' : ℕ → Ω → R} [MeasurableSingletonClass 𝓐] (h : IsAlgEnvSeq O A R' alg env P) (a : 𝓐) : MeasureTheory.StronglyAdapted h.filtration fun (n : ℕ) => pullCount A a (n + 1)

theorem Learning.isStronglyPredictable_pullCount {𝓞 : Type u_1} {𝓐 : Type u_2} {R : Type u_3} {Ω : Type u_4} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {mR : MeasurableSpace R} {mΩ : MeasurableSpace Ω} [DecidableEq 𝓐] {alg : Algorithm 𝓞 𝓐 R} {env : Environment 𝓞 𝓐 R} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {R' : ℕ → Ω → R} [MeasurableSingletonClass 𝓐] (h : IsAlgEnvSeq O A R' alg env P) (a : 𝓐) : MeasureTheory.IsStronglyPredictable h.filtration (pullCount A a)

theorem Learning.measurableSet_action_eq_and_pullCount_eq {𝓐 : Type u_2} {Ω : Type u_4} {m𝓐 : MeasurableSpace 𝓐} {mΩ : MeasurableSpace Ω} [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} [MeasurableSingletonClass 𝓐] (hA : ∀ (n : ℕ), Measurable (A n)) (t : ℕ) (b : 𝓐) (k : ℕ) : MeasurableSet {x : Ω | A t x = b ∧ pullCount A b t x = k}

theorem Learning.measurableSet_snd_eq_and_pullCount'_eq {𝓞 : Type u_1} {𝓐 : Type u_2} {R : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {mR : MeasurableSpace R} [DecidableEq 𝓐] [MeasurableSingletonClass 𝓐] (n : ℕ) (b : 𝓐) (k : ℕ) : MeasurableSet {u : (Hist 𝓞 𝓐 R n × 𝓞) × 𝓐 | u.2 = b ∧ pullCount' n u.1.1 b = k}

theorem Learning.setOf_action_eq_and_pullCount_eq_eq_preimage {𝓞 : Type u_1} {𝓐 : Type u_2} {R : Type u_3} {Ω : Type u_4} [DecidableEq 𝓐] {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {R' : ℕ → Ω → R} (n : ℕ) (b : 𝓐) (k : ℕ) : {x : Ω | A n x = b ∧ pullCount A b n x = k} = (fun (x : Ω) => ((history O A R' n x, O n x), A n x)) ⁻¹' {u : (Hist 𝓞 𝓐 R n × 𝓞) × 𝓐 | u.2 = b ∧ pullCount' n u.1.1 b = k}

The event that the action at time n is b and that b was pulled k times before is a preimage by ((history O A R' n, O n), A n).

theorem Learning.integrable_pullCount {𝓐 : Type u_2} {Ω : Type u_4} {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

noncomputable def Learning.stepsUntil {𝓐 : Type u_2} {Ω : Type u_4} [DecidableEq 𝓐] (A : ℕ → Ω → 𝓐) (a : 𝓐) (m : ℕ) (ω : Ω) : ℕ∞

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

Equations

• Learning.stepsUntil A a m ω = sInf (Nat.cast '' {s : ℕ | Learning.pullCount A a (s + 1) ω = m})

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

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

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

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

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

theorem Learning.stepsUntil_eq_dite {𝓐 : Type u_2} {Ω : Type u_4} [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 ⊤

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

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

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

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

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

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

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

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

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

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

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

theorem Learning.pullCount_lt_of_le_stepsUntil {𝓐 : Type u_2} {Ω : Type u_4} [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

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

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

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

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

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

theorem Learning.isStoppingTime_stepsUntil {𝓞 : Type u_1} {𝓐 : Type u_2} {R : Type u_3} {Ω : Type u_4} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {mR : MeasurableSpace R} {mΩ : MeasurableSpace Ω} [DecidableEq 𝓐] {alg : Algorithm 𝓞 𝓐 R} {env : Environment 𝓞 𝓐 R} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {R' : ℕ → Ω → R} {m : ℕ} [MeasurableSingletonClass 𝓐] (h : IsAlgEnvSeq O A R' alg env P) (a : 𝓐) (hm : m ≠ 0) : MeasureTheory.IsStoppingTime h.filtration (stepsUntil A a m)

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

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

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

theorem Learning.measurable_indicator_stepsUntil_eq {𝓞 : Type u_1} {𝓐 : Type u_2} {R : Type u_3} {Ω : Type u_4} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {mR : MeasurableSpace R} {mΩ : MeasurableSpace Ω} [DecidableEq 𝓐] {alg : Algorithm 𝓞 𝓐 R} {env : Environment 𝓞 𝓐 R} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {R' : ℕ → Ω → R} [MeasurableSingletonClass 𝓐] (h : IsAlgEnvSeq O A R' alg env P) (a : 𝓐) (m n : ℕ) : Measurable ({ω : Ω | stepsUntil A a m ω = ↑n}.indicator fun (x : Ω) => 1)

theorem Learning.measurableSet_stepsUntil_eq {𝓞 : Type u_1} {𝓐 : Type u_2} {R : Type u_3} {Ω : Type u_4} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {mR : MeasurableSpace R} [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} [MeasurableSingletonClass 𝓐] (O : ℕ → Ω → 𝓞) (R' : ℕ → Ω → R) (a : 𝓐) (m n : ℕ) : MeasurableSet {ω : Ω | stepsUntil A a m ω = ↑n}

theorem Learning.isStoppingTime_stepsUntil_filtrationAction {𝓞 : Type u_1} {𝓐 : Type u_2} {R : Type u_3} {Ω : Type u_4} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {mR : MeasurableSpace R} {mΩ : MeasurableSpace Ω} [DecidableEq 𝓐] {alg : Algorithm 𝓞 𝓐 R} {env : Environment 𝓞 𝓐 R} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {R' : ℕ → Ω → R} [MeasurableSingletonClass 𝓐] (h : IsAlgEnvSeq O A R' alg env P) (a : 𝓐) (m : ℕ) : MeasureTheory.IsStoppingTime h.filtrationAction (stepsUntil A a m)

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

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

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.

Equations

• Learning.rewardByCount A R' a m ω = match Learning.stepsUntil A a m ω.1 with | none => ω.2 m a | some n => R' n ω.1

theorem Learning.rewardByCount_eq_ite {𝓐 : Type u_2} {R : Type u_3} {Ω : Type u_4} [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} {R' : ℕ → Ω → R} (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

theorem Learning.rewardByCount_eq_add {𝓐 : Type u_2} {R : Type u_3} {Ω : Type u_4} [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} {R' : ℕ → Ω → R} [AddMonoid R] (a : 𝓐) (m : ℕ) : rewardByCount A R' a m = ({ω : Ω × (ℕ → 𝓐 → R) | stepsUntil A a m ω.1 ≠ ⊤}.indicator fun (ω : Ω × (ℕ → 𝓐 → R)) => R' (stepsUntil A a m ω.1).toNat ω.1) + {ω : Ω × (ℕ → 𝓐 → R) | stepsUntil A a m ω.1 = ⊤}.indicator fun (ω : Ω × (ℕ → 𝓐 → R)) => ω.2 m a

theorem Learning.rewardByCount_of_stepsUntil_eq_top {𝓐 : Type u_2} {R : Type u_3} {Ω : Type u_4} [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} {R' : ℕ → Ω → R} {a : 𝓐} {m : ℕ} {ω : Ω × (ℕ → 𝓐 → R)} (h : stepsUntil A a m ω.1 = ⊤) : rewardByCount A R' a m ω = ω.2 m a

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

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

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

@[simp]

theorem Learning.rewardByCount_zero {𝓐 : Type u_2} {R : Type u_3} {Ω : Type u_4} [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} {R' : ℕ → Ω → R} (a : 𝓐) (ω : Ω × (ℕ → 𝓐 → R)) : rewardByCount A R' a 0 ω = if A 0 ω.1 = a then ω.2 0 a else R' 0 ω.1

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

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

theorem Learning.measurable_rewardByCount {𝓐 : Type u_2} {R : Type u_3} {Ω : Type u_4} {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 (ω : Ω × (ℕ → 𝓐 → R)) => rewardByCount A R' a m ω

noncomputable def Learning.rewardByCountUntil {𝓐 : Type u_2} {R : Type u_3} {Ω : Type u_4} [DecidableEq 𝓐] (A : ℕ → Ω → 𝓐) (R' : ℕ → Ω → R) : ℕ → Ω × (ℕ → 𝓐 → R) → 𝓐 × ℕ → R

Array of rewards by count, truncated at time t: the entry (a, m) is the reward received at the (m + 1)-th pull of action a if that pull happened before time t, and the entry (m + 1, a) of the auxiliary array ω.2 otherwise.

This is an auxiliary definition used to prove results about the distribution of rewardByCount.

It is defined recursively: at time t, the entry (A t, pullCount A (A t) t) is replaced by the reward R' t. See rewardByCountUntil_apply_of_lt_pullCount and rewardByCountUntil_apply_of_pullCount_le.

Equations

• Learning.rewardByCountUntil A R' 0 x✝ = fun (p : 𝓐 × ℕ) => x✝.2 (p.2 + 1) p.1
• Learning.rewardByCountUntil A R' t.succ x✝ = Function.update (Learning.rewardByCountUntil A R' t x✝) (A t x✝.1, Learning.pullCount A (A t x✝.1) t x✝.1) (R' t x✝.1)

@[simp]

theorem Learning.rewardByCountUntil_zero {𝓐 : Type u_2} {R : Type u_3} {Ω : Type u_4} [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} {R' : ℕ → Ω → R} (ω : Ω × (ℕ → 𝓐 → R)) : rewardByCountUntil A R' 0 ω = fun (p : 𝓐 × ℕ) => ω.2 (p.2 + 1) p.1

theorem Learning.rewardByCountUntil_add_one {𝓐 : Type u_2} {R : Type u_3} {Ω : Type u_4} [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} {R' : ℕ → Ω → R} (t : ℕ) (ω : Ω × (ℕ → 𝓐 → R)) : rewardByCountUntil A R' (t + 1) ω = Function.update (rewardByCountUntil A R' t ω) (A t ω.1, pullCount A (A t ω.1) t ω.1) (R' t ω.1)

theorem Learning.rewardByCountUntil_apply_of_pullCount_le {𝓐 : Type u_2} {R : Type u_3} {Ω : Type u_4} [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} {R' : ℕ → Ω → R} {a : 𝓐} {m t : ℕ} {ω : Ω × (ℕ → 𝓐 → R)} (h : pullCount A a t ω.1 ≤ m) : rewardByCountUntil A R' t ω (a, m) = ω.2 (m + 1) a

If action a was pulled at most m times before time t, then the entry (a, m) of rewardByCountUntil A R' t ω is the entry (m + 1, a) of the auxiliary array.

theorem Learning.rewardByCountUntil_apply_of_lt_pullCount {𝓐 : Type u_2} {R : Type u_3} {Ω : Type u_4} [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} {R' : ℕ → Ω → R} {a : 𝓐} {m t : ℕ} {ω : Ω × (ℕ → 𝓐 → R)} (h : m < pullCount A a t ω.1) : rewardByCountUntil A R' t ω (a, m) = rewardByCount A R' a (m + 1) ω

If action a was pulled more than m times before time t, then the entry (a, m) of rewardByCountUntil A R' t ω is the reward received at the (m + 1)-th pull of a.

theorem Learning.rewardByCountUntil_congr {𝓐 : Type u_2} {R : Type u_3} {Ω : Type u_4} [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} {R' : ℕ → Ω → R} {x : Ω} {z z' : ℕ → 𝓐 → R} (t : ℕ) (p : 𝓐 × ℕ) (hz : z (p.2 + 1) p.1 = z' (p.2 + 1) p.1) : rewardByCountUntil A R' t (x, z) p = rewardByCountUntil A R' t (x, z') p

rewardByCountUntil A R' t (x, z) p depends on z only through z (p.2 + 1) p.1.

theorem Learning.eventually_rewardByCountUntil_eq {𝓐 : Type u_2} {R : Type u_3} {Ω : Type u_4} [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} {R' : ℕ → Ω → R} (ω : Ω × (ℕ → 𝓐 → R)) (p : 𝓐 × ℕ) : ∀ᶠ (t : ℕ) in Filter.atTop, rewardByCountUntil A R' t ω p = rewardByCount A R' p.1 (p.2 + 1) ω

For each entry, rewardByCountUntil A R' t ω coincides with rewardByCount for t large enough.

theorem Learning.measurable_rewardByCountUntil_of {𝓐 : Type u_2} {R : Type u_3} {Ω : Type u_4} {m𝓐 : MeasurableSpace 𝓐} {mR : MeasurableSpace R} [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} {R' : ℕ → Ω → R} {m : MeasurableSpace (Ω × (ℕ → 𝓐 → R))} [MeasurableEq 𝓐] (t : ℕ) (hA : ∀ i < t, Measurable fun (ω : Ω × (ℕ → 𝓐 → R)) => A i ω.1) (hR : ∀ i < t, Measurable fun (ω : Ω × (ℕ → 𝓐 → R)) => R' i ω.1) (hZ : Measurable Prod.snd) : Measurable (rewardByCountUntil A R' t)

Measurability of rewardByCountUntil A R' t with respect to a σ-algebra m for which the actions and rewards before time t and the auxiliary array are measurable.

theorem Learning.measurable_rewardByCountUntil {𝓐 : Type u_2} {R : Type u_3} {Ω : Type u_4} {m𝓐 : MeasurableSpace 𝓐} {mR : MeasurableSpace R} {mΩ : MeasurableSpace Ω} [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} {R' : ℕ → Ω → R} [MeasurableEq 𝓐] (hA : ∀ (n : ℕ), Measurable (A n)) (hR' : ∀ (n : ℕ), Measurable (R' n)) (t : ℕ) : Measurable (rewardByCountUntil A R' t)

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

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

theorem Learning.sum_comp_pullCount {𝓐 : Type u_2} {R : Type u_3} {Ω : Type u_4} [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

theorem Learning.sum_pullCount' {𝓞 : Type u_1} {𝓐 : Type u_2} [DecidableEq 𝓐] [Fintype 𝓐] (n : ℕ) (h : Hist 𝓞 𝓐 ℝ n) : ∑ a : 𝓐, pullCount' n h a = n