Lean module · Foundations
BanditRLProof.Algorithms.HeavyTailSourceExpectedCount
Corrected expected counts for the unchanged source policy. The shared threshold-count integral producer is reused; confidence is derived from raw moments.
Module map
Imports
BanditRLProof.Algorithms.HeavyTailSourceAdaptive, BanditRLProof.Algorithms.HeavyTailExpectedCount
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.robust_lintegral_count_le
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_lintegral_count_leReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem robust_lintegral_count_le (hK : 0 < K) (ν : Kernel (Fin K) ℝ) [IsMarkovKernel ν] (best arm : Fin K) (ε u : ℝ) (T : ℕ) (hT : 2 ≤ 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) : (∫⁻ stream, (pullCount (robustAction hK ε u stream) arm T : ℝ≥0∞) ∂UCB.armStreamMeasure ν) ≤ gapThreshold ε u ((∫ x, x ∂ν best) - ∫ x, x ∂ν arm) T + 4
theorem
BanditRLProof.HeavyTail.SourcePolicy.robust_integrable_count
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_integrable_countReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem robust_integrable_count (hK : 0 < K) (ν : Kernel (Fin K) ℝ) [IsMarkovKernel ν] (arm : Fin K) (ε u : ℝ) (T : ℕ) : Integrable (fun stream => (pullCount (robustAction hK ε u stream) arm T : ℝ)) (UCB.armStreamMeasure ν)
theorem
BanditRLProof.HeavyTail.SourcePolicy.robust_integral_count_le
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_integral_count_leReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem robust_integral_count_le (hK : 0 < K) (ν : Kernel (Fin K) ℝ) [IsMarkovKernel ν] (best arm : Fin K) (ε u : ℝ) (T : ℕ) (hT : 2 ≤ 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) : (∫ stream, (pullCount (robustAction hK ε u stream) arm T : ℝ) ∂UCB.armStreamMeasure ν) ≤ gapThreshold ε u ((∫ x, x ∂ν best) - ∫ x, x ∂ν arm) T + 4
theorem
BanditRLProof.HeavyTail.SourcePolicy.robust_integral_count_le_budget
Compiled
All horizons, retaining the additive five without a positive-cutoff assumption at T=0/1.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.HeavyTail.SourcePolicy.robust_integral_count_le_budgetReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem robust_integral_count_le_budget (hK : 0 < K) (ν : Kernel (Fin K) ℝ) [IsMarkovKernel ν] (best arm : Fin K) (ε u : ℝ) (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) : (∫ stream, (pullCount (robustAction hK ε u stream) arm T : ℝ) ∂UCB.armStreamMeasure ν) ≤ gapBudget ε u ((∫ x, x ∂ν best) - ∫ x, x ∂ν arm) T + 5