BanditRLProof.Algorithms.HeavyTailAdaptive

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

noncomputable def robustMean (hK : 0 < K) (ε u : ℝ) (stream : UCB.ArmRewardStream K) (arm : Fin K) (t : ℕ) : ℝ

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

theorem robustMean_latent (hK : 0 < K) (ε u : ℝ) (stream : UCB.ArmRewardStream K) (arm : Fin K) (t : ℕ) : robustMean hK ε u stream arm t = (∑ s ∈ Finset.range (pullCount (robustAction hK ε u stream) arm t), truncate (sampleThreshold ε u t s) (stream s arm)) / pullCount (robustAction hK ε u stream) arm t

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

theorem robust_pullCount_pos (hK : 0 < K) (ε u : ℝ) (stream : UCB.ArmRewardStream K) (arm : Fin K) (t : ℕ) (ht : K ≤ t) : 0 < pullCount (robustAction hK ε u stream) arm t

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

theorem robustMean_history (hK : 0 < K) (ε u : ℝ) (stream : UCB.ArmRewardStream K) (arm : Fin K) (n : ℕ) : historyTruncatedMean (UCB.initializationArm hK 0) (sampleThreshold ε u (n+1)) n (ArmStreamPolicy.history (UCB.initializationArm hK 0) (nextArm hK ε u) stream n) arm = robustMean hK ε u stream arm (n+1)

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

theorem robustIndex_history (hK : 0 < K) (ε u : ℝ) (stream : UCB.ArmRewardStream K) (arm : Fin K) (n : ℕ) : historyIndex (UCB.initializationArm hK 0) ε u n (ArmStreamPolicy.history (UCB.initializationArm hK 0) (nextArm hK ε u) stream n) arm = robustMean hK ε u stream arm (n+1) + confidenceRadius ε u (n+1) (pullCount (robustAction hK ε u stream) arm (n+1))

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

theorem robustMean_tail (hK : 0 < K) (ν : Kernel (Fin K) ℝ) [IsMarkovKernel ν] (arm : Fin K) (ε u : ℝ) (t : ℕ) (ht : K ≤ t) (hε0 : 0 ≤ ε) (hε : ε ≤ 1) (hu0 : 0 < u) (hX : Integrable (fun x : ℝ => x) (ν arm)) (hm : Integrable (fun x : ℝ => |x|^(1+ε)) (ν arm)) (hu : (∫ x, |x|^(1+ε) ∂ν arm) ≤ u) : (UCB.armStreamMeasure ν).real {stream | confidenceRadius ε u t (pullCount (robustAction hK ε u stream) arm t) ≤ |robustMean hK ε u stream arm t - ∫ x, x ∂ν arm|} ≤ t * (2 * Real.exp (-confidenceLog t))

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

theorem robust_selected_gap_le (hK : 0 < K) (ε u : ℝ) (stream : UCB.ArmRewardStream K) (mean : Fin K → ℝ) (best : Fin K) (n : ℕ) (hn : K ≤ n+1) (hbest : |robustMean hK ε u stream best (n+1) - mean best| ≤ confidenceRadius ε u (n+1) (pullCount (robustAction hK ε u stream) best (n+1))) (hchosen : |robustMean hK ε u stream (robustAction hK ε u stream (n+1)) (n+1) - mean (robustAction hK ε u stream (n+1))| ≤ confidenceRadius ε u (n+1) (pullCount (robustAction hK ε u stream) (robustAction hK ε u stream (n+1)) (n+1))) : mean best - mean (robustAction hK ε u stream (n+1)) ≤ 2 * confidenceRadius ε u (n+1) (pullCount (robustAction hK ε u stream) (robustAction hK ε u stream (n+1)) (n+1))

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

theorem robust_selected_small_radius_tail (hK : 0 < K) (ν : Kernel (Fin K) ℝ) [IsMarkovKernel ν] (best arm : Fin K) (ε u : ℝ) (t : ℕ) (ht : K ≤ t) (hε0 : 0 ≤ ε) (hε : ε ≤ 1) (hu0 : 0 < u) (hX : ∀ a, Integrable (fun x : ℝ => x) (ν a)) (hm : ∀ a, Integrable (fun x : ℝ => |x|^(1+ε)) (ν a)) (hu : ∀ a, (∫ x, |x|^(1+ε) ∂ν a) ≤ u) : (UCB.armStreamMeasure ν).real {stream | robustAction hK ε u stream t = arm ∧ 2 * confidenceRadius ε u t (pullCount (robustAction hK ε u stream) arm t) < (∫ x, x ∂ν best) - ∫ x, x ∂ν arm} ≤ 4*t*Real.exp (-confidenceLog t)

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

theorem robust_initial_count_zero (hK : 0 < K) (ε u : ℝ) (stream : UCB.ArmRewardStream K) (t : ℕ) (ht : t < K) : pullCount (robustAction hK ε u stream) (robustAction hK ε u stream t) t = 0

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

theorem robust_large_count_tail (hK : 0 < K) (ν : Kernel (Fin K) ℝ) [IsMarkovKernel ν] (best arm : Fin K) (ε u : ℝ) (T t : ℕ) (ht : t ≤ T) (hε0 : 0 < ε) (hε : ε ≤ 1) (hu0 : 0 < u) (hgap : 0 < (∫ x, x ∂ν best) - ∫ x, x ∂ν arm) (hX : ∀ a, Integrable (fun x : ℝ => x) (ν a)) (hm : ∀ a, Integrable (fun x : ℝ => |x|^(1+ε)) (ν a)) (hu : ∀ a, (∫ x, |x|^(1+ε) ∂ν a) ≤ u) : (UCB.armStreamMeasure ν).real {stream | robustAction hK ε u stream t = arm ∧ gapThreshold ε u ((∫ x, x ∂ν best) - ∫ x, x ∂ν arm) T ≤ pullCount (robustAction hK ε u stream) arm t} ≤ 4*t*Real.exp (-confidenceLog t)