BanditRLProof.Algorithms.HeavyTailSourcePolicy

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

noncomputable def sampleThreshold (ε u : ℝ) (t s : ℕ) : ℝ

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

noncomputable def historyIndex (initial : Fin K) (ε u : ℝ) (n : ℕ) (h : History.FinitePairHistory (Fin K) ℝ n) (arm : Fin K) : ℝ

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

noncomputable def nextArm (hK : 0 < K) (ε u : ℝ) (n : ℕ) (h : History.FinitePairHistory (Fin K) ℝ n) : Fin K

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

theorem measurable_historyIndex (initial : Fin K) (ε u : ℝ) (n : ℕ) (arm : Fin K) : Measurable (fun h => historyIndex initial ε u n h arm)

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

theorem measurable_nextArm (hK : 0 < K) (ε u : ℝ) (n : ℕ) : Measurable (nextArm hK ε u n)

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

noncomputable def robustAction (hK : 0 < K) (ε u : ℝ)

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

noncomputable def robustReward (hK : 0 < K) (ε u : ℝ)

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

theorem measurable_robustAction (hK : 0 < K) (ε u : ℝ) (t : ℕ) : Measurable (fun stream => robustAction hK ε u stream t)

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

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

The selected index is maximal on the actual observed history.

theorem robustAction_maximizes (hK : 0 < K) (ε u : ℝ) (stream : UCB.ArmRewardStream K) (n : ℕ) (hn : K ≤ n+1) (arm : Fin K) : let h := ArmStreamPolicy.history (UCB.initializationArm hK 0) (nextArm hK ε u) stream n historyIndex (UCB.initializationArm hK 0) ε u n h arm ≤ historyIndex (UCB.initializationArm hK 0) ε u n h (robustAction hK ε u stream (n+1))

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) + sourceConfidenceRadius ε 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 arm_adaptive_upper_tail (ν : Kernel (Fin K) ℝ) [IsMarkovKernel ν] (arm : Fin K) (count : UCB.ArmRewardStream K → ℕ) (ε u : ℝ) (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 | 0 < count stream ∧ count stream ≤ t ∧ sourceConfidenceRadius ε u t (count stream) ≤ (∑ s ∈ Finset.range (count stream), truncate (sampleThreshold ε u t s) (stream s arm)) / count stream - ∫ x, x ∂ν arm} ≤ t*Real.exp (-(5/4 : ℝ)*sourceConfidenceLog t)

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

theorem robustMean_upper_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 | sourceConfidenceRadius ε u t (pullCount (robustAction hK ε u stream) arm t) ≤ robustMean hK ε u stream arm t - ∫ x, x ∂ν arm} ≤ t*Real.exp (-(5/4 : ℝ)*sourceConfidenceLog t)

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

theorem arm_adaptive_lower_tail (ν : Kernel (Fin K) ℝ) [IsMarkovKernel ν] (arm : Fin K) (count : UCB.ArmRewardStream K → ℕ) (ε u : ℝ) (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 | 0 < count stream ∧ count stream ≤ t ∧ sourceConfidenceRadius ε u t (count stream) ≤ (∫ x, x ∂ν arm) - (∑ s ∈ Finset.range (count stream), truncate (sampleThreshold ε u t s) (stream s arm)) / count stream} ≤ t*Real.exp (-(5/4 : ℝ)*sourceConfidenceLog t)

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

theorem robustMean_lower_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 | sourceConfidenceRadius ε u t (pullCount (robustAction hK ε u stream) arm t) ≤ (∫ x, x ∂ν arm) - robustMean hK ε u stream arm t} ≤ t*Real.exp (-(5/4 : ℝ)*sourceConfidenceLog t)

Finite time budget for one signed event of the actual source-parameter policy.

theorem robustMean_upper_tail_sum (hK : 0 < K) (ν : Kernel (Fin K) ℝ) [IsMarkovKernel ν] (arm : Fin K) (ε u : ℝ) (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) : (∑ t ∈ Finset.range T, (UCB.armStreamMeasure ν).real {stream | K ≤ t ∧ sourceConfidenceRadius ε u t (pullCount (robustAction hK ε u stream) arm t) ≤ robustMean hK ε u stream arm t - ∫ x, x ∂ν arm}) ≤ 2

Finite time budget for one signed event of the actual source-parameter policy.

theorem robustMean_lower_tail_sum (hK : 0 < K) (ν : Kernel (Fin K) ℝ) [IsMarkovKernel ν] (arm : Fin K) (ε u : ℝ) (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) : (∑ t ∈ Finset.range T, (UCB.armStreamMeasure ν).real {stream | K ≤ t ∧ sourceConfidenceRadius ε u t (pullCount (robustAction hK ε u stream) arm t) ≤ (∫ x, x ∂ν arm) - robustMean hK ε u stream arm t}) ≤ 2