Lean module · Foundations
BanditRLProof.Algorithms.HeavyTailExpectedCount
Expected pull counts for the actual robust policy under raw-moment reward laws.
Module map
Imports
BanditRLProof.Algorithms.HeavyTailAdaptive, BanditRLProof.HeavyTailTailSum
Imported by
BanditRLProof.Algorithms.HOOExpectedVisits, BanditRLProof.Algorithms.HeavyTailRegret, BanditRLProof.Algorithms.HeavyTailSourceExpectedCount
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.HeavyTail.lintegral_pullCount_threshold
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.lintegral_pullCount_thresholdReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem lintegral_pullCount_threshold {Ω : Type} [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ] (a : Ω → ActionTrace (Fin K)) (ha : ∀ t, Measurable (fun ω => a ω t)) (arm : Fin K) (T B : ℕ) : (∫⁻ ω, (pullCount (a ω) arm T : ℝ≥0∞) ∂μ) ≤ B + ∑ t ∈ Finset.range T, μ {ω | a ω t = arm ∧ B ≤ pullCount (a ω) arm t}
theorem
BanditRLProof.HeavyTail.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.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 : ℕ) (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 + 2
theorem
BanditRLProof.HeavyTail.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.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.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.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 : ℕ) (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 + 2