Equalities between definitions of random variables used in bandit algorithms

theorem Bandits.pullCount_add_one_eq_pullCount' {K : ℕ} {a : Fin K} {n : ℕ} {h : ℕ → Fin K × ℝ} : pullCount a (n + 1) h = pullCount' n (fun (i : { x : ℕ // x ∈ Finset.Iic n }) => h ↑i) a

theorem Bandits.pullCount_eq_pullCount' {K : ℕ} {a : Fin K} {n : ℕ} {h : ℕ → Fin K × ℝ} (hn : n ≠ 0) : pullCount a n h = pullCount' (n - 1) (fun (i : { x : ℕ // x ∈ Finset.Iic (n - 1) }) => h ↑i) a

theorem Bandits.sumRewards_add_one_eq_sumRewards' {K : ℕ} {a : Fin K} {n : ℕ} {h : ℕ → Fin K × ℝ} : sumRewards a (n + 1) h = sumRewards' n (fun (i : { x : ℕ // x ∈ Finset.Iic n }) => h ↑i) a

theorem Bandits.sumRewards_eq_sumRewards' {K : ℕ} {a : Fin K} {n : ℕ} {h : ℕ → Fin K × ℝ} (hn : n ≠ 0) : sumRewards a n h = sumRewards' (n - 1) (fun (i : { x : ℕ // x ∈ Finset.Iic (n - 1) }) => h ↑i) a

theorem Bandits.empMean_add_one_eq_empMean' {K : ℕ} {a : Fin K} {n : ℕ} {h : ℕ → Fin K × ℝ} : empMean a (n + 1) h = empMean' n (fun (i : { x : ℕ // x ∈ Finset.Iic n }) => h ↑i) a

theorem Bandits.empMean_eq_empMean' {K : ℕ} {a : Fin K} {n : ℕ} {h : ℕ → Fin K × ℝ} (hn : n ≠ 0) : empMean a n h = empMean' (n - 1) (fun (i : { x : ℕ // x ∈ Finset.Iic (n - 1) }) => h ↑i) a