The action indicator

actionIndicator A k n ω = 𝟙{A n ω = k} is the {0,1}-valued indicator that action k was chosen at round n. It is the increment weight of every per-action sum attached to an action process: pullCount A k n is its partial sum (sum_range_actionIndicator_eq_pullCount) and sumRewards A Y k n is its reward-weighted partial sum (sum_actionIndicator_mul).

Main definitions

• Learning.actionIndicator

Main results

• Learning.sum_range_actionIndicator_eq_pullCount, Learning.sum_actionIndicator_mul — the two partial-sum identities.
• Learning.adapted_actionIndicator, Learning.integrable_actionIndicator.

noncomputable def Learning.actionIndicator {Ω : Type u_1} {𝓐 : Type u_3} (A : ℕ → Ω → 𝓐) (k : 𝓐) (n : ℕ) (ω : Ω) : ℝ

The {0,1}-valued assignment indicator of action k: actionIndicator A k n ω = 𝟙{A n ω = k}.

Equations

• Learning.actionIndicator A k n ω = {ω : Ω | A n ω = k}.indicator (fun (x : Ω) => 1) ω

theorem Learning.actionIndicator_eq_one_iff {Ω : Type u_1} {𝓐 : Type u_3} {A : ℕ → Ω → 𝓐} {k : 𝓐} {n : ℕ} {ω : Ω} : actionIndicator A k n ω = 1 ↔ A n ω = k

actionIndicator A k n ω = 1 exactly when action k is chosen at time n.

theorem Learning.actionIndicator_nonneg {Ω : Type u_1} {𝓐 : Type u_3} (A : ℕ → Ω → 𝓐) (k : 𝓐) (n : ℕ) (ω : Ω) : 0 ≤ actionIndicator A k n ω

theorem Learning.actionIndicator_le_one {Ω : Type u_1} {𝓐 : Type u_3} (A : ℕ → Ω → 𝓐) (k : 𝓐) (n : ℕ) (ω : Ω) : actionIndicator A k n ω ≤ 1

theorem Learning.sum_actionIndicator {Ω : Type u_1} {𝓐 : Type u_3} [Fintype 𝓐] (A : ℕ → Ω → 𝓐) (j : ℕ) (ω : Ω) : ∑ k : 𝓐, actionIndicator A k j ω = 1

Exactly one arm is pulled at each round, so the indicators sum to 1.

theorem Learning.sum_actionIndicator_eq_pullCount {Ω : Type u_1} {𝓐 : Type u_3} [DecidableEq 𝓐] (A : ℕ → Ω → 𝓐) (k : 𝓐) (n : ℕ) (ω : Ω) : ∑ j ∈ Finset.range n, actionIndicator A k j ω = ↑(pullCount A k n ω)

theorem Learning.sum_actionIndicator_smul {Ω : Type u_1} {𝓐 : Type u_3} {𝓨 : Type u_4} [DecidableEq 𝓐] [AddCommGroup 𝓨] [Module ℝ 𝓨] (A : ℕ → Ω → 𝓐) (Y : ℕ → Ω → 𝓨) (k : 𝓐) (t : ℕ) (ω : Ω) : ∑ j ∈ Finset.range t, actionIndicator A k j ω • Y j ω = sumRewards A Y k t ω

theorem Learning.sum_actionIndicator_mul {Ω : Type u_1} {𝓐 : Type u_3} [DecidableEq 𝓐] (A : ℕ → Ω → 𝓐) (Y : ℕ → Ω → ℝ) (k : 𝓐) (t : ℕ) (ω : Ω) : ∑ j ∈ Finset.range t, actionIndicator A k j ω * Y j ω = sumRewards A Y k t ω

theorem Learning.measurable_actionIndicator {Ω : Type u_1} {𝓐 : Type u_3} {mΩ : MeasurableSpace Ω} {m𝓐 : MeasurableSpace 𝓐} [MeasurableSingletonClass 𝓐] {A : ℕ → Ω → 𝓐} (k : 𝓐) {n : ℕ} (hA : Measurable (A n)) : Measurable (actionIndicator A k n)

theorem Learning.integrable_actionIndicator {Ω : Type u_1} {𝓐 : Type u_3} {mΩ : MeasurableSpace Ω} {m𝓐 : MeasurableSpace 𝓐} [MeasurableSingletonClass 𝓐] {A : ℕ → Ω → 𝓐} (P : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure P] (k : 𝓐) {n : ℕ} (hA : Measurable (A n)) : MeasureTheory.Integrable (actionIndicator A k n) P

theorem Learning.IsAlgEnvSeq.adapted_actionIndicator {Ω : Type u_1} {𝓞 : Type u_2} {𝓐 : Type u_3} {𝓨 : Type u_4} {mΩ : MeasurableSpace Ω} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} [MeasurableSingletonClass 𝓐] {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {P : MeasureTheory.Measure Ω} {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} [MeasureTheory.IsFiniteMeasure P] (h : IsAlgEnvSeq O A Y alg env P) (k : 𝓐) : MeasureTheory.Adapted h.filtration (actionIndicator A k)

The action indicator is adapted to the history filtration: whether action k was chosen at n is known at time n.

theorem Learning.IsAlgEnvSeq.adapted_actionIndicator_filtrationAction {Ω : Type u_1} {𝓞 : Type u_2} {𝓐 : Type u_3} {𝓨 : Type u_4} {mΩ : MeasurableSpace Ω} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} [MeasurableSingletonClass 𝓐] {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {P : MeasureTheory.Measure Ω} {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} [MeasureTheory.IsFiniteMeasure P] (h : IsAlgEnvSeq O A Y alg env P) (k : 𝓐) : MeasureTheory.Adapted h.filtrationAction (actionIndicator A k)

The action indicator is adapted to the history+action filtration: whether action k was chosen at n is known once we know the action at n.