BanditRLProof.Algorithms.HeavyTailSourceCounterexample

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

noncomputable def dropped (L : ℝ) (n : ℕ) : ℕ

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

theorem truncate_neg_one (L : ℝ) (hL : 0 < L) (s : ℕ) : truncate (sourceTruncationThreshold 1 1 L s) (-1) = if (s : ℝ)+1 < L then 0 else -1

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

theorem dropped_filter (L : ℝ) (n : ℕ) : (Finset.range n).filter (fun s : ℕ => (s : ℝ)+1 < L) = Finset.range (dropped L n)

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

theorem sum_truncate_neg_one (L : ℝ) (hL : 0 < L) (n : ℕ) : (∑ s ∈ Finset.range n, truncate (sourceTruncationThreshold 1 1 L s) (-1)) = -(n : ℝ) + dropped L n

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

theorem dropped_ge (L : ℝ) (hL : 0 < L) (n : ℕ) (hn : L ≤ n) : L-1 ≤ (dropped L n : ℝ)

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

theorem suboptimal_index_gt (H L n d : ℝ) (hH : 30 < H) (hL : 2*H-2 ≤ L) (hn : 0 < n) (hnM : n ≤ 32*H+5) (hd : L-1 ≤ d) : (1/100 : ℝ) < -1+d/n+4*Real.sqrt (L/n)

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

theorem optimal_index_lt (H L m : ℝ) (hH : 0 < H) (hL0 : 0 ≤ L) (hL : L ≤ 2*H) (hm : 320000*H < m) : 4*Real.sqrt (L/m) < (1/100 : ℝ)

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

noncomputable def deterministicStream : UCB.ArmRewardStream 2

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

noncomputable def trace : ActionTrace (Fin 2)

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

theorem mean_zero (t : ℕ) : SourcePolicy.robustMean (by decide) 1 1 deterministicStream 0 t = 0

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

theorem mean_one (t : ℕ) (ht : 2 ≤ t) : SourcePolicy.robustMean (by decide) 1 1 deterministicStream 1 t = -1 + dropped (sourceConfidenceLog t) (pullCount trace 1 t) / pullCount trace 1 t

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

theorem radius_sqrt (t n : ℕ) : sourceConfidenceRadius 1 1 t n = 4 * Real.sqrt (sourceConfidenceLog t/n)

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

theorem source_index_sub_gt (H : ℝ) (t : ℕ) (ht : 2 ≤ t) (hH : 30 < H) (hL : 2*H-2 ≤ sourceConfidenceLog t) (hnM : (pullCount trace 1 t : ℝ) ≤ 32*H+5) : (1/100 : ℝ) < SourcePolicy.robustMean (by decide) 1 1 deterministicStream 1 t + sourceConfidenceRadius 1 1 t (pullCount trace 1 t)

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

theorem source_index_best_lt (H : ℝ) (t : ℕ) (ht : 2 ≤ t) (hH : 0 < H) (hL : sourceConfidenceLog t ≤ 2*H) (hm : 320000*H < (pullCount trace 0 t : ℝ)) : SourcePolicy.robustMean (by decide) 1 1 deterministicStream 0 t + sourceConfidenceRadius 1 1 t (pullCount trace 0 t) < (1/100 : ℝ)

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

theorem forced_suboptimal (H : ℝ) (t : ℕ) (ht : 2 ≤ t) (hH : 30 < H) (hLlo : 2*H-2 ≤ sourceConfidenceLog t) (hLhi : sourceConfidenceLog t ≤ 2*H) (hnM : (pullCount trace 1 t : ℝ) ≤ 32*H+5) (hm : 320000*H < (pullCount trace 0 t : ℝ)) : trace t = 1

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

def horizon : ℕ

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

noncomputable def horizonHeight : ℝ

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

theorem log_two_bounds : (3/5 : ℝ) < Real.log 2 ∧ Real.log 2 < 1

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

theorem height_bounds : (30 : ℝ) < horizonHeight ∧ horizonHeight < 50

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

theorem late_log_bounds (t : ℕ) (htlo : horizon/2 ≤ t) (hthi : t < horizon) : 2*horizonHeight-2 ≤ sourceConfidenceLog t ∧ sourceConfidenceLog t ≤ 2*horizonHeight

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

theorem late_best_count (t : ℕ) (ht : horizon/2 ≤ t) (hthi : t ≤ horizon) (hcount : (pullCount trace 1 horizon : ℝ) ≤ 32*horizonHeight+5) : 320000*horizonHeight < (pullCount trace 0 t : ℝ)

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

theorem finite_count_obstruction : 32*horizonHeight+5 < (pullCount trace 1 horizon : ℝ)

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

noncomputable def kernel : Kernel (Fin 2) ℝ

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

@[simp] theorem kernel_apply (a : Fin 2) : kernel a = Measure.dirac (if a = 0 then (0 : ℝ) else -1)

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

theorem kernel_raw_moment (a : Fin 2) : Integrable (fun x : ℝ => |x|^(1+(1 : ℝ))) (kernel a) ∧ (∫ x : ℝ, |x|^(1+(1 : ℝ)) ∂kernel a) ≤ 1

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

@[simp] theorem kernel_mean (a : Fin 2) : realKernelMean kernel a = if a = 0 then 0 else -1

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

theorem ae_deterministic : ∀ᵐ stream ∂UCB.armStreamMeasure kernel, stream = deterministicStream

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

theorem kernel_best_mean : (⨆ a : Fin 2, realKernelMean kernel a) = 0

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

theorem kernel_gap (a : Fin 2) : realMeanGap (realKernelMean kernel) a = if a = 0 then 0 else 1

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

theorem regret_eq_count (action : ActionTrace (Fin 2)) (T : ℕ) : realMeanRegret (realKernelMean kernel) action T = (pullCount action 1 T : ℝ)

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

theorem expected_regret_eq_count : (∫ stream, realMeanRegret (realKernelMean kernel) (SourcePolicy.robustAction (by decide) 1 1 stream) horizon ∂UCB.armStreamMeasure kernel) = (pullCount trace 1 horizon : ℝ)

The literal printed coefficient fails for the actual source-parameter policy under valid raw-second-moment stationary two-arm laws at a finite horizon.

theorem printed_coefficient_counterexample : 32 * Real.log (horizon : ℝ) + 5 < ∫ stream, realMeanRegret (realKernelMean kernel) (SourcePolicy.robustAction (by decide) 1 1 stream) horizon ∂UCB.armStreamMeasure kernel

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

theorem printed_gap_sum : (∑ a ∈ Finset.univ.filter (fun a : Fin 2 => 0 < realMeanGap (realKernelMean kernel) a), (8 * (4 / realMeanGap (realKernelMean kernel) a) ^ (1 / (1 : ℝ)) * Real.log (horizon : ℝ) + 5 * realMeanGap (realKernelMean kernel) a)) = 32 * Real.log (horizon : ℝ) + 5

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

theorem literal_printed_bound_false : ¬ (∫ stream, realMeanRegret (realKernelMean kernel) (SourcePolicy.robustAction (by decide) 1 1 stream) horizon ∂UCB.armStreamMeasure kernel) ≤ ∑ a ∈ Finset.univ.filter (fun a : Fin 2 => 0 < realMeanGap (realKernelMean kernel) a), (8 * (4 / realMeanGap (realKernelMean kernel) a) ^ (1 / (1 : ℝ)) * Real.log (horizon : ℝ) + 5 * realMeanGap (realKernelMean kernel) a)