Lean module · Foundations
BanditRLProof.HeavyTailSourceGap
Explicit corrected gap cutoff for the unchanged source-parameter policy.
Module map
Imports
BanditRLProof.Algorithms.HeavyTailSourcePolicy
Imported by
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
def
BanditRLProof.HeavyTail.SourcePolicy.horizonLog
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.horizonLogReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def horizonLog (T : ℕ) : ℝ
def
BanditRLProof.HeavyTail.SourcePolicy.gapBudget
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.gapBudgetReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def gapBudget (ε u gap : ℝ) (T : ℕ) : ℝ
def
BanditRLProof.HeavyTail.SourcePolicy.gapThreshold
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.gapThresholdReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def gapThreshold (ε u gap : ℝ) (T : ℕ) : ℕ
theorem
BanditRLProof.HeavyTail.SourcePolicy.horizonLog_nonneg
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.horizonLog_nonnegReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem horizonLog_nonneg (T : ℕ) : 0 ≤ horizonLog T
theorem
BanditRLProof.HeavyTail.SourcePolicy.horizonLog_pos
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.horizonLog_posReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem horizonLog_pos (T : ℕ) (hT : 2 ≤ T) : 0 < horizonLog T
theorem
BanditRLProof.HeavyTail.SourcePolicy.gapBudget_nonneg
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.gapBudget_nonnegReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem gapBudget_nonneg (ε u gap : ℝ) (T : ℕ) (hu : 0 < u) (hg : 0 < gap) : 0 ≤ gapBudget ε u gap T
theorem
BanditRLProof.HeavyTail.SourcePolicy.gapThreshold_pos
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.gapThreshold_posReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem gapThreshold_pos (ε u gap : ℝ) (T : ℕ) (hT : 2 ≤ T) (hu : 0 < u) (hg : 0 < gap) : 0 < gapThreshold ε u gap T
theorem
BanditRLProof.HeavyTail.SourcePolicy.sourceLog_le_horizon
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.sourceLog_le_horizonReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem sourceLog_le_horizon {t T : ℕ} (ht : t < T) : sourceConfidenceLog t ≤ horizonLog T
theorem
BanditRLProof.HeavyTail.SourcePolicy.twice_radius_le_gap
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.twice_radius_le_gapReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem twice_radius_le_gap (ε u gap : ℝ) (hε : 0 < ε) (hu : 0 < u) (hg : 0 < gap) (t T n : ℕ) (hT : 2 ≤ T) (ht : t < T) (hn : gapThreshold ε u gap T ≤ n) : 2*sourceConfidenceRadius ε u t n ≤ gap