BanditRLProof.Algorithms.HeavyTailHistory

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

def historyAction (initial : Fin K) (n : ℕ) (h : History.FinitePairHistory (Fin K) ℝ n) : ActionTrace (Fin K)

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

def historyReward (n : ℕ) (h : History.FinitePairHistory (Fin K) ℝ n) : RewardTrace ℝ

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

theorem measurable_historyAction (initial : Fin K) (n t : ℕ) : Measurable (fun h => historyAction initial n h t)

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

theorem measurable_historyReward (n t : ℕ) : Measurable (fun h : History.FinitePairHistory (Fin K) ℝ n => historyReward n h t)

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

noncomputable def historyTruncatedMean (initial : Fin K) (B : ℕ → ℝ) (n : ℕ) (h : History.FinitePairHistory (Fin K) ℝ n) (arm : Fin K) : ℝ

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

theorem measurable_historyTruncatedMean (initial : Fin K) (B : ℕ → ℝ) (n : ℕ) (arm : Fin K) : Measurable (fun h => historyTruncatedMean initial B n h arm)

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

theorem history_count_trace (initial : Fin K) (a : ActionTrace (Fin K)) (r : RewardTrace ℝ) (arm : Fin K) (n t : ℕ) (ht : t ≤ n+1) : pullCount (historyAction initial n (History.finitePairHistoryOfTrace a r n)) arm t = pullCount a arm t

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

theorem historyTruncatedMean_trace (initial : Fin K) (B : ℕ → ℝ) (a : ActionTrace (Fin K)) (r : RewardTrace ℝ) (arm : Fin K) (n : ℕ) : historyTruncatedMean initial B n (History.finitePairHistoryOfTrace a r n) arm = sumRewards a (fun t => truncate (B (pullCount a arm t)) (r t)) arm (n+1) / pullCount a arm (n+1)

On selected observations, the fixed arm count is the selected arm count. This is the pathwise connection to the latent fixed-prefix confidence theorem.

theorem truncated_observed_sum {Ω : Type*} (a : Ω → ActionTrace (Fin K)) (stream : Ω → UCB.ArmRewardStream K) (B : ℕ → ℝ) (ω : Ω) (arm : Fin K) (n : ℕ) : sumRewards (a ω) (fun t => truncate (B (pullCount (a ω) arm t)) (UCB.rewardFromArmStream a stream ω t)) arm n = ∑ s ∈ Finset.range (pullCount (a ω) arm n), truncate (B s) (stream ω s arm)

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

theorem historyTruncatedMean_latent (initial : Fin K) (select) (B : ℕ → ℝ) (stream : UCB.ArmRewardStream K) (arm : Fin K) (n : ℕ) : historyTruncatedMean initial B n (ArmStreamPolicy.history initial select stream n) arm = (∑ s ∈ Finset.range (pullCount (ArmStreamPolicy.action initial select stream) arm (n+1)), truncate (B s) (stream s arm)) / pullCount (ArmStreamPolicy.action initial select stream) arm (n+1)