BanditRLProof.HeavyTailClipping

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

noncomputable def clip (B x : ℝ) : ℝ

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

theorem abs_clip_sub_clip_le (B x y : ℝ) : |clip B x - clip B y| ≤ |x - y|

Unlike hard truncation, clipping is stable even when corruption crosses B.

theorem clip_corruption_le (B x c : ℝ) : |clip B (x + c) - clip B x| ≤ |c|

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

noncomputable def prefixMean (X : ℕ → ℝ) (n : ℕ) : ℝ

The finite-prefix corruption producer allows index-dependent clipping.

theorem clipped_prefix_corruption_le (X c B : ℕ → ℝ) (n : ℕ) (C : ℝ) (hC : (∑ s ∈ Finset.range n, |c s|) ≤ C) : |prefixMean (fun s => clip (B s) (X s + c s)) n - prefixMean (fun s => clip (B s) (X s)) n| ≤ C / n

Actual adaptively consumed clipped observations retain the same prefix. The corruption stream can be arbitrary; this is a pathwise statement.

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

Combine the new corruption producer with the common error assembly. Bias and fluctuation are still supplied; no concentration is asserted here.

theorem corrupted_clipped_estimator_error_le (X c B : ℕ → ℝ) (n : ℕ) (C center mean bias fluctuation : ℝ) (hC : (∑ s ∈ Finset.range n, |c s|) ≤ C) (hb : |center - mean| ≤ bias) (hf : |prefixMean (fun s => clip (B s) (X s)) n - center| ≤ fluctuation) : |prefixMean (fun s => clip (B s) (X s + c s)) n - mean| ≤ bias + fluctuation + C / n

Full pathwise transfer to the actually observed estimator. Both reward streams are compared along the SAME action trace; this does not compare two policies whose actions changed in response to the corruption.

theorem actual_clipped_corruption_le {Ω : Type*} {K : ℕ} (action : Ω → ActionTrace (Fin K)) (stream corruption : Ω → UCB.ArmRewardStream K) (B : ℕ → Fin K → ℝ) (ω : Ω) (arm : Fin K) (t : ℕ) (C : ℝ) (hC : (∑ j ∈ Finset.range (pullCount (action ω) arm t), |corruption ω j arm|) ≤ C) : |sumRewards (action ω) (fun s => clip (B (pullCount (action ω) (action ω s) s) (action ω s)) (UCB.rewardFromArmStream action (fun ω j a => stream ω j a + corruption ω j a) ω s)) arm t / pullCount (action ω) arm t - sumRewards (action ω) (fun s => clip (B (pullCount (action ω) (action ω s) s) (action ω s)) (UCB.rewardFromArmStream action stream ω s)) arm t / pullCount (action ω) arm t| ≤ C / pullCount (action ω) arm t

A concrete discontinuity diagnostic: hard truncation cannot use the same unit-Lipschitz corruption producer.

theorem truncate_not_unit_lipschitz : ¬ (∀ x y : ℝ, |truncate 1 x - truncate 1 y| ≤ |x - y|)