BanditRLProof.Algorithms.MOSSUnusedCoordinate

No declaration docstring is present; use the chapter context and exact statement below.

def canonicalCondition {k : ℕ} (hk : 0 < k) (n : ℕ) (mean : Fin k → ℝ) (t : ℕ) (table : UCB.ArmRewardStream k)

No declaration docstring is present; use the chapter context and exact statement below.

def canonicalNextCoordinate {k : ℕ} (hk : 0 < k) (n : ℕ) (mean : Fin k → ℝ) (t : ℕ) (table : UCB.ArmRewardStream k) : ℕ × Fin k

No declaration docstring is present; use the chapter context and exact statement below.

theorem canonicalNextCoordinate_count {k : ℕ} (hk : 0 < k) (n : ℕ) (mean : Fin k → ℝ) (t : ℕ) (table : UCB.ArmRewardStream k) : (canonicalNextCoordinate hk n mean t table).1 = pullCount (canonicalAction hk n mean table) (canonicalNextCoordinate hk n mean t table).2 (t+1)+1

No declaration docstring is present; use the chapter context and exact statement below.

theorem canonicalHistory_eq_of_complement_eq {k : ℕ} (hk : 0 < k) (n : ℕ) (mean : Fin k → ℝ) (t : ℕ) (target : ℕ × Fin k) (table table' : UCB.ArmRewardStream k) (hc : UCB.armStreamWithoutCoordinate target table = UCB.armStreamWithoutCoordinate target table') (hf : pullCount (canonicalAction hk n mean table) target.2 (t+1) < target.1) : canonicalHistory hk n mean table t = canonicalHistory hk n mean table' t

No declaration docstring is present; use the chapter context and exact statement below.

theorem canonicalNextCoordinate_eq_iff_insert {k : ℕ} (hk : 0 < k) (n : ℕ) (mean : Fin k → ℝ) (t : ℕ) (target : ℕ × Fin k) (v : ℝ) (table : UCB.ArmRewardStream k) : canonicalNextCoordinate hk n mean t table = target ↔ canonicalNextCoordinate hk n mean t (UCB.armStreamInsertCoordinate target v (UCB.armStreamWithoutCoordinate target table)) = target

No declaration docstring is present; use the chapter context and exact statement below.

def canonicalConditionWithout {k : ℕ} (hk : 0 < k) (n : ℕ) (mean : Fin k → ℝ) (t : ℕ) (target : ℕ × Fin k) (v : ℝ)

No declaration docstring is present; use the chapter context and exact statement below.

theorem canonicalCondition_eq_without {k : ℕ} (hk : 0 < k) (n : ℕ) (mean : Fin k → ℝ) (t : ℕ) (target : ℕ × Fin k) (v : ℝ) (table : UCB.ArmRewardStream k) (hnext : canonicalNextCoordinate hk n mean t table = target) : canonicalCondition hk n mean t table = canonicalConditionWithout hk n mean t target v (UCB.armStreamWithoutCoordinate target table)

No declaration docstring is present; use the chapter context and exact statement below.

theorem measurable_canonicalCondition {k : ℕ} (hk : 0 < k) (n : ℕ) (mean : Fin k → ℝ) (t : ℕ) : Measurable (canonicalCondition hk n mean t)

No declaration docstring is present; use the chapter context and exact statement below.

theorem measurable_canonicalConditionWithout {k : ℕ} (hk : 0 < k) (n : ℕ) (mean : Fin k → ℝ) (t : ℕ) (target : ℕ × Fin k) (v : ℝ) : Measurable (canonicalConditionWithout hk n mean t target v)

A target reward is independent of the condition reconstructed without it.

theorem indepFun_coordinate_canonicalConditionWithout {k : ℕ} (hk : 0 < k) (n : ℕ) (mean : Fin k → ℝ) (t : ℕ) (ν : Kernel (Fin k) ℝ) [IsMarkovKernel ν] (target : ℕ × Fin k) (v : ℝ) : IndepFun (UCB.armStreamCoordinate target) (fun table => canonicalConditionWithout hk n mean t target v (UCB.armStreamWithoutCoordinate target table)) (UCB.armStreamMeasure ν)

No declaration docstring is present; use the chapter context and exact statement below.

theorem map_canonicalConditionWithout_coordinate {k : ℕ} (hk : 0 < k) (n : ℕ) (mean : Fin k → ℝ) (t : ℕ) (ν : Kernel (Fin k) ℝ) [IsMarkovKernel ν] (target : ℕ × Fin k) (v : ℝ) : Measure.map (fun table => (canonicalConditionWithout hk n mean t target v (UCB.armStreamWithoutCoordinate target table), UCB.armStreamCoordinate target table)) (UCB.armStreamMeasure ν) = (Measure.map (fun table => canonicalConditionWithout hk n mean t target v (UCB.armStreamWithoutCoordinate target table)) (UCB.armStreamMeasure ν)).prod (ν target.2)