BanditRLProof.HeavyTailSourceConfidence

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

noncomputable def sourceTruncationThreshold (ε u L : ℝ) (s : ℕ) : ℝ

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

theorem sourceThreshold_pos (ε u L : ℝ) (hu : 0 < u) (hL : 0 < L) (s : ℕ) : 0 < sourceTruncationThreshold ε u L s

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

theorem sourceThreshold_le_terminal (ε u L : ℝ) (hε : 0 ≤ ε) (hu : 0 ≤ u) (hL : 0 < L) (n s : ℕ) (hs : s < n) : sourceTruncationThreshold ε u L s ≤ (u*n/L)^(1/(1+ε))

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

theorem sourceThreshold_bias_average (ε u L : ℝ) (hε : 0 ≤ ε) (hu : 0 < u) (hL : 0 < L) (n : ℕ) (hn : 0 < n) : (∑ s ∈ Finset.range n, u / (sourceTruncationThreshold ε u L s)^ε) / n ≤ (1+ε)*u^(1/(1+ε))*(L/n)^(ε/(1+ε))

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

theorem sourceThreshold_variance_sum (ε u L : ℝ) (hε0 : 0 ≤ ε) (hε : ε ≤ 1) (hu : 0 < u) (hL : 0 < L) (n : ℕ) : (∑ s ∈ Finset.range n, u*(sourceTruncationThreshold ε u L s)^(1-ε)) ≤ n*u*((u*n/L)^(1/(1+ε)))^(1-ε)

One-sided centered-sum bound at the full raw-variable tilt 1/B.

theorem source_centered_sum_upper_tail_sharp {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ] (X : ℕ → Ω → ℝ) (ε u L : ℝ) (n : ℕ) (hn : 0 < n) (hXm : ∀ i, Measurable (X i)) (hi : iIndepFun X μ) (hε0 : 0 ≤ ε) (hε : ε ≤ 1) (hu : 0 < u) (hL : 0 < L) (hm : ∀ i, Integrable (fun ω => |X i ω|^(1+ε)) μ) (hraw : ∀ i, (∫ ω, |X i ω|^(1+ε) ∂μ) ≤ u) : μ.real {ω | 2*(u*n/L)^(1/(1+ε))*L ≤ ∑ i ∈ Finset.range n, (truncate (sourceTruncationThreshold ε u L i) (X i ω) - ∫ ω, truncate (sourceTruncationThreshold ε u L i) (X i ω) ∂μ)} ≤ Real.exp (-(5/4 : ℝ)*L)

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

theorem source_centered_sum_upper_tail {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ] (X : ℕ → Ω → ℝ) (ε u L : ℝ) (n : ℕ) (hn : 0 < n) (hXm : ∀ i, Measurable (X i)) (hi : iIndepFun X μ) (hε0 : 0 ≤ ε) (hε : ε ≤ 1) (hu : 0 < u) (hL : 0 < L) (hm : ∀ i, Integrable (fun ω => |X i ω|^(1+ε)) μ) (hraw : ∀ i, (∫ ω, |X i ω|^(1+ε) ∂μ) ≤ u) : μ.real {ω | 2*(u*n/L)^(1/(1+ε))*L ≤ ∑ i ∈ Finset.range n, (truncate (sourceTruncationThreshold ε u L i) (X i ω) - ∫ ω, truncate (sourceTruncationThreshold ε u L i) (X i ω) ∂μ)} ≤ Real.exp (-L)

Constant-four upper deviation for arbitrary positive log confidence.

theorem source_truncated_mean_upper_tail_log_sharp {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ] (X : ℕ → Ω → ℝ) (ε u L mean : ℝ) (n : ℕ) (hn : 0 < n) (hXm : ∀ i, Measurable (X i)) (hi : iIndepFun X μ) (hε0 : 0 ≤ ε) (hε : ε ≤ 1) (hu : 0 < u) (hL : 0 < L) (hX : ∀ i, Integrable (X i) μ) (hmean : ∀ i, (∫ ω, X i ω ∂μ) = mean) (hm : ∀ i, Integrable (fun ω => |X i ω|^(1+ε)) μ) (hraw : ∀ i, (∫ ω, |X i ω|^(1+ε) ∂μ) ≤ u) : μ.real {ω | 4*u^(1/(1+ε))*(L/n)^(ε/(1+ε)) ≤ (∑ i ∈ Finset.range n, truncate (sourceTruncationThreshold ε u L i) (X i ω))/n - mean} ≤ Real.exp (-(5/4 : ℝ)*L)

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

theorem source_truncated_mean_upper_tail_log {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ] (X : ℕ → Ω → ℝ) (ε u L mean : ℝ) (n : ℕ) (hn : 0 < n) (hXm : ∀ i, Measurable (X i)) (hi : iIndepFun X μ) (hε0 : 0 ≤ ε) (hε : ε ≤ 1) (hu : 0 < u) (hL : 0 < L) (hX : ∀ i, Integrable (X i) μ) (hmean : ∀ i, (∫ ω, X i ω ∂μ) = mean) (hm : ∀ i, Integrable (fun ω => |X i ω|^(1+ε)) μ) (hraw : ∀ i, (∫ ω, |X i ω|^(1+ε) ∂μ) ≤ u) : μ.real {ω | 4*u^(1/(1+ε))*(L/n)^(ε/(1+ε)) ≤ (∑ i ∈ Finset.range n, truncate (sourceTruncationThreshold ε u L i) (X i ω))/n - mean} ≤ Real.exp (-L)

BCL 2013 Lemma 1 upper deviation, retaining its radius constant four. The non-strict bad event proved here is stronger than a strict upper-tail event.

theorem source_truncated_mean_upper_tail {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ] (X : ℕ → Ω → ℝ) (ε u δ mean : ℝ) (n : ℕ) (hn : 0 < n) (hXm : ∀ i, Measurable (X i)) (hi : iIndepFun X μ) (hε0 : 0 < ε) (hε : ε ≤ 1) (hu : 0 < u) (hδ : 0 < δ) (hδ1 : δ < 1) (hX : ∀ i, Integrable (X i) μ) (hmean : ∀ i, (∫ ω, X i ω ∂μ) = mean) (hm : ∀ i, Integrable (fun ω => |X i ω|^(1+ε)) μ) (hraw : ∀ i, (∫ ω, |X i ω|^(1+ε) ∂μ) ≤ u) : μ.real {ω | 4*u^(1/(1+ε))*(Real.log (1/δ)/n)^(ε/(1+ε)) ≤ (∑ i ∈ Finset.range n, truncate (sourceTruncationThreshold ε u (Real.log (1/δ)) i) (X i ω))/n - mean} ≤ δ

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

theorem truncate_neg (B x : ℝ) : truncate B (-x) = -truncate B x

Reflection supplies the other one-sided source confidence statement.

theorem source_truncated_mean_lower_tail {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ] (X : ℕ → Ω → ℝ) (ε u δ mean : ℝ) (n : ℕ) (hn : 0 < n) (hXm : ∀ i, Measurable (X i)) (hi : iIndepFun X μ) (hε0 : 0 < ε) (hε : ε ≤ 1) (hu : 0 < u) (hδ : 0 < δ) (hδ1 : δ < 1) (hX : ∀ i, Integrable (X i) μ) (hmean : ∀ i, (∫ ω, X i ω ∂μ) = mean) (hm : ∀ i, Integrable (fun ω => |X i ω|^(1+ε)) μ) (hraw : ∀ i, (∫ ω, |X i ω|^(1+ε) ∂μ) ≤ u) : μ.real {ω | 4*u^(1/(1+ε))*(Real.log (1/δ)/n)^(ε/(1+ε)) ≤ mean - (∑ i ∈ Finset.range n, truncate (sourceTruncationThreshold ε u (Real.log (1/δ)) i) (X i ω))/n} ≤ δ

Sharper lower log-confidence tail, obtained by reflection.

theorem source_truncated_mean_lower_tail_log_sharp {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ] (X : ℕ → Ω → ℝ) (ε u L mean : ℝ) (n : ℕ) (hn : 0 < n) (hXm : ∀ i, Measurable (X i)) (hi : iIndepFun X μ) (hε0 : 0 ≤ ε) (hε : ε ≤ 1) (hu : 0 < u) (hL : 0 < L) (hX : ∀ i, Integrable (X i) μ) (hmean : ∀ i, (∫ ω, X i ω ∂μ) = mean) (hm : ∀ i, Integrable (fun ω => |X i ω|^(1+ε)) μ) (hraw : ∀ i, (∫ ω, |X i ω|^(1+ε) ∂μ) ≤ u) : μ.real {ω | 4*u^(1/(1+ε))*(L/n)^(ε/(1+ε)) ≤ mean - (∑ i ∈ Finset.range n, truncate (sourceTruncationThreshold ε u (L) i) (X i ω))/n} ≤ Real.exp (-(5/4 : ℝ)*L)