Lean module · Foundations
BanditRLProof.Algorithms.HeavyTailSourceAdaptive
Strict good-event index comparison and actual selected-large-count events.
Module map
Imports
BanditRLProof.HeavyTailSourceGap
Imported by
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.HeavyTail.SourcePolicy.selected_gap_lt
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.HeavyTail.SourcePolicy.selected_gap_ltReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem selected_gap_lt (hK : 0 < K) (ε u : ℝ) (stream : UCB.ArmRewardStream K) (mean : Fin K → ℝ) (best : Fin K) (n : ℕ) (hn : K ≤ n+1) (hbest : mean best - robustMean hK ε u stream best (n+1) < sourceConfidenceRadius ε u (n+1) (pullCount (robustAction hK ε u stream) best (n+1))) (hchosen : robustMean hK ε u stream (robustAction hK ε u stream (n+1)) (n+1) - mean (robustAction hK ε u stream (n+1)) < sourceConfidenceRadius ε u (n+1) (pullCount (robustAction hK ε u stream) (robustAction hK ε u stream (n+1)) (n+1))) : mean best - mean (robustAction hK ε u stream (n+1)) < 2*sourceConfidenceRadius ε u (n+1) (pullCount (robustAction hK ε u stream) (robustAction hK ε u stream (n+1)) (n+1))
theorem
BanditRLProof.HeavyTail.SourcePolicy.robust_selected_small_radius_tail
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.HeavyTail.SourcePolicy.robust_selected_small_radius_tailReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem robust_selected_small_radius_tail (hK : 0 < K) (ν : Kernel (Fin K) ℝ) [IsMarkovKernel ν] (best arm : Fin K) (ε u : ℝ) (t : ℕ) (ht : K ≤ t) (hε0 : 0 ≤ ε) (hε : ε ≤ 1) (hu0 : 0 < u) (hX : ∀ a, Integrable (fun x : ℝ => x) (ν a)) (hm : ∀ a, Integrable (fun x : ℝ => |x|^(1+ε)) (ν a)) (hu : ∀ a, (∫ x, |x|^(1+ε) ∂ν a) ≤ u) : (UCB.armStreamMeasure ν).real {stream | robustAction hK ε u stream t = arm ∧ 2*sourceConfidenceRadius ε u t (pullCount (robustAction hK ε u stream) arm t) ≤ (∫ x, x ∂ν best) - ∫ x, x ∂ν arm} ≤ 2*t*Real.exp (-(5/4 : ℝ)*sourceConfidenceLog t)
theorem
BanditRLProof.HeavyTail.SourcePolicy.robust_initial_count_zero
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.HeavyTail.SourcePolicy.robust_initial_count_zeroReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem robust_initial_count_zero (hK : 0 < K) (ε u : ℝ) (stream : UCB.ArmRewardStream K) (t : ℕ) (ht : t < K) : pullCount (robustAction hK ε u stream) (robustAction hK ε u stream t) t = 0
theorem
BanditRLProof.HeavyTail.SourcePolicy.robust_large_count_tail
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.HeavyTail.SourcePolicy.robust_large_count_tailReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem robust_large_count_tail (hK : 0 < K) (ν : Kernel (Fin K) ℝ) [IsMarkovKernel ν] (best arm : Fin K) (ε u : ℝ) (T t : ℕ) (hT : 2 ≤ T) (ht : t < T) (hε0 : 0 < ε) (hε : ε ≤ 1) (hu0 : 0 < u) (hgap : 0 < (∫ x, x ∂ν best) - ∫ x, x ∂ν arm) (hX : ∀ a, Integrable (fun x : ℝ => x) (ν a)) (hm : ∀ a, Integrable (fun x : ℝ => |x|^(1+ε)) (ν a)) (hu : ∀ a, (∫ x, |x|^(1+ε) ∂ν a) ≤ u) : (UCB.armStreamMeasure ν).real {stream | robustAction hK ε u stream t = arm ∧ gapThreshold ε u ((∫ x, x ∂ν best) - ∫ x, x ∂ν arm) T ≤ pullCount (robustAction hK ε u stream) arm t} ≤ 2*t*Real.exp (-(5/4 : ℝ)*sourceConfidenceLog t)