BanditRLProof.HeavyTailClippedTransfer

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

theorem integrable_of_raw_moment {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ] (X : Ω → ℝ) (ε : ℝ) (hXm : Measurable X) (hε : 0 ≤ ε) (hm : Integrable (fun ω => |X ω|^(1+ε)) μ) : Integrable X μ

No clean-confidence or fluctuation premise: these are produced from the independent raw-moment stream. Only the actually consumed prefix is budgeted.

theorem adaptive_corrupted_clipped_mean_tail {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ] (X c : ℕ → Ω → ℝ) (count : Ω → ℕ) (ε u mean C : ℝ) (t : ℕ) (hXm : ∀ i, Measurable (X i)) (hi : iIndepFun X μ) (hε0 : 0 ≤ ε) (hε : ε ≤ 1) (hu0 : 0 < u) (hmean : ∀ i, (∫ ω, X i ω ∂μ) = mean) (hm : ∀ i, Integrable (fun ω => |X i ω|^(1+ε)) μ) (hu : ∀ i, (∫ ω, |X i ω|^(1+ε) ∂μ) ≤ u) (hC : ∀ ω, (∑ s ∈ Finset.range (count ω), |c s ω|) ≤ C) : μ.real {ω | 0 < count ω ∧ count ω ≤ t ∧ confidenceRadius ε u t (count ω) + C / count ω ≤ |prefixMean (fun s => clip (sampleThreshold ε u t s) (X s ω + c s ω)) (count ω) - mean|} ≤ t * (2 * Real.exp (-confidenceLog t))

Confidence for the actual clipped observations along an arbitrary action trace, including a policy driven by corrupted observations. This compares clean and corrupted rewards along that same trace, not two different policies.

theorem observed_corrupted_clipped_mean_tail {Ω : Type*} [MeasurableSpace Ω] {K : ℕ} (μ : Measure Ω) [IsProbabilityMeasure μ] (action : Ω → ActionTrace (Fin K)) (stream corruption : Ω → UCB.ArmRewardStream K) (arm : Fin K) (ε u mean C : ℝ) (t : ℕ) (hXm : ∀ i, Measurable (fun ω => stream ω i arm)) (hi : iIndepFun (fun i ω => stream ω i arm) μ) (hε0 : 0 ≤ ε) (hε : ε ≤ 1) (hu0 : 0 < u) (hmean : ∀ i, (∫ ω, stream ω i arm ∂μ) = mean) (hm : ∀ i, Integrable (fun ω => |stream ω i arm|^(1+ε)) μ) (hu : ∀ i, (∫ ω, |stream ω i arm|^(1+ε) ∂μ) ≤ u) (hC : ∀ ω, (∑ s ∈ Finset.range (pullCount (action ω) arm t), |corruption ω s arm|) ≤ C) : μ.real {ω | 0 < pullCount (action ω) arm t ∧ pullCount (action ω) arm t ≤ t ∧ confidenceRadius ε u t (pullCount (action ω) arm t) + C / pullCount (action ω) arm t ≤ |sumRewards (action ω) (fun s => clip (sampleThreshold ε u t (pullCount (action ω) (action ω s) s)) (UCB.rewardFromArmStream action (fun ω j a => stream ω j a + corruption ω j a) ω s)) arm t / pullCount (action ω) arm t - mean|} ≤ t * (2 * Real.exp (-confidenceLog t))

Stationary arm laws supply the coordinate independence and moments for the reserved transfer endpoint. No confidence bound is supplied by the caller.

theorem arm_corrupted_clipped_mean_tail {K : ℕ} (ν : Kernel (Fin K) ℝ) [IsMarkovKernel ν] (arm : Fin K) (count : UCB.ArmRewardStream K → ℕ) (c : ℕ → UCB.ArmRewardStream K → ℝ) (ε u C : ℝ) (t : ℕ) (hε0 : 0 ≤ ε) (hε : ε ≤ 1) (hu0 : 0 < u) (hm : Integrable (fun x : ℝ => |x|^(1+ε)) (ν arm)) (hu : (∫ x, |x|^(1+ε) ∂ν arm) ≤ u) (hC : ∀ stream, (∑ s ∈ Finset.range (count stream), |c s stream|) ≤ C) : (UCB.armStreamMeasure ν).real {stream | 0 < count stream ∧ count stream ≤ t ∧ confidenceRadius ε u t (count stream) + C / count stream ≤ |prefixMean (fun s => clip (sampleThreshold ε u t s) (stream s arm + c s stream)) (count stream) - ∫ x, x ∂ν arm|} ≤ t * (2 * Real.exp (-confidenceLog t))