BanditRLProof.HeavyTailTruncation

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

noncomputable def truncate (B x : ℝ) : ℝ

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

theorem abs_truncate_le (B x : ℝ) (hB : 0 ≤ B) : |truncate B x| ≤ B

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

theorem measurable_truncate (B : ℝ) : Measurable (truncate B)

The discarded tail is controlled by a raw (1+epsilon)-moment.

theorem abs_sub_truncate_le (B x ε : ℝ) (hB : 0 < B) (hε : 0 ≤ ε) : |x - truncate B x| ≤ |x| ^ (1 + ε) / B ^ ε

Truncation supplies the variance-scale envelope needed by Bernstein.

theorem sq_truncate_le (B x ε : ℝ) (hB : 0 < B) (hε : ε ≤ 1) : (truncate B x) ^ 2 ≤ |x| ^ (1 + ε) * B ^ (1 - ε)

Integrating the pointwise tail inequality produces an actual bias bound.

theorem integral_truncate_bias_le {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) (X : Ω → ℝ) (B ε u : ℝ) (hB : 0 < B) (hε : 0 ≤ ε) (hXm : Measurable X) (hX : Integrable X μ) (hm : Integrable (fun ω => |X ω| ^ (1 + ε)) μ) (hu : (∫ ω, |X ω| ^ (1 + ε) ∂μ) ≤ u) : |(∫ ω, X ω ∂μ) - ∫ ω, truncate B (X ω) ∂μ| ≤ u / B ^ ε

The second moment envelope is integrable and bounded by the raw moment.

theorem integral_sq_truncate_le {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) (X : Ω → ℝ) (B ε u : ℝ) (hB : 0 < B) (hε : ε ≤ 1) (hXm : Measurable X) (hm : Integrable (fun ω => |X ω| ^ (1 + ε)) μ) (hu : (∫ ω, |X ω| ^ (1 + ε) ∂μ) ≤ u) : (∫ ω, (truncate B (X ω)) ^ 2 ∂μ) ≤ u * B ^ (1 - ε)

A sample-index transform of actual observations is the same transform of the consumed latent prefix. No IID claim is made about adaptively selected data.

theorem transformed_observed_prefix {Ω : Type*} {K : ℕ} (action : Ω → ActionTrace (Fin K)) (stream : Ω → UCB.ArmRewardStream K) (transform : ℕ → Fin K → ℝ → ℝ) (ω : Ω) (arm : Fin K) (n : ℕ) : sumRewards (action ω) (fun t => transform (pullCount (action ω) (action ω t) t) (action ω t) (UCB.rewardFromArmStream action stream ω t)) arm n = (Finset.range (pullCount (action ω) arm n)).sum (fun s => transform s arm (stream ω s arm))

Common estimator assembly: deterministic bias and stochastic fluctuation remain separate obligations, rather than assuming the desired confidence event.

theorem estimator_error_le (estimate center mean bias fluctuation : ℝ) (hb : |center - mean| ≤ bias) (hf : |estimate - center| ≤ fluctuation) : |estimate - mean| ≤ bias + fluctuation