Lean module · Foundations
BanditRLProof.HeavyTailArmLaw
Stationary raw-moment reward laws supply every fixed-coordinate hypothesis.
Module map
Imports
BanditRLProof.HeavyTailScheduledConfidence, BanditRLProof.Algorithms.UCBArmStreamTail
Imported by
BanditRLProof.Algorithms.HeavyTailAdaptive, BanditRLProof.Algorithms.HeavyTailSourcePolicy, BanditRLProof.HeavyTailClippedTransfer
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.HeavyTail.arm_coordinate_integral
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.arm_coordinate_integralReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem arm_coordinate_integral (ν : Kernel (Fin K) ℝ) [IsMarkovKernel ν] (arm : Fin K) (i : ℕ) (g : ℝ → ℝ) (hg : Measurable g) : (∫ stream, g (stream i arm) ∂UCB.armStreamMeasure ν) = ∫ x, g x ∂ν arm
theorem
BanditRLProof.HeavyTail.arm_coordinate_integrable
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.arm_coordinate_integrableReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem arm_coordinate_integrable (ν : Kernel (Fin K) ℝ) [IsMarkovKernel ν] (arm : Fin K) (i : ℕ) (g : ℝ → ℝ) (hg : Integrable g (ν arm)) : Integrable (fun stream => g (stream i arm)) (UCB.armStreamMeasure ν)
theorem
BanditRLProof.HeavyTail.arm_adaptive_mean_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.arm_adaptive_mean_tailReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem arm_adaptive_mean_tail (ν : Kernel (Fin K) ℝ) [IsMarkovKernel ν] (arm : Fin K) (count : UCB.ArmRewardStream K → ℕ) (ε u : ℝ) (t : ℕ) (hε0 : 0 ≤ ε) (hε : ε ≤ 1) (hu0 : 0 < u) (hX : Integrable (fun x : ℝ => x) (ν arm)) (hm : Integrable (fun x : ℝ => |x|^(1+ε)) (ν arm)) (hu : (∫ x, |x|^(1+ε) ∂ν arm) ≤ u) : (UCB.armStreamMeasure ν).real {stream | 0 < count stream ∧ count stream ≤ t ∧ confidenceRadius ε u t (count stream) ≤ |(∑ s ∈ Finset.range (count stream), truncate (sampleThreshold ε u t s) (stream s arm)) / count stream - ∫ x, x ∂ν arm|} ≤ t * (2 * Real.exp (-confidenceLog t))