Lean module · Probability layer
BanditRLProof.ConcentrationCappedOccupancy
Generated source map for this Lean module.
Module map
Imports
BanditRLProof.ConcentrationGaussianOccupancy
Imported by
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
def
BanditRLProof.Concentration.cappedOccupancyTail
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book · Reinforcement Learning Book · Online Learning Book
2. Probability, kernels, filtrations, and concentration
Canonical node identity
declaration:BanditRLProof.Concentration.cappedOccupancyTailReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
def cappedOccupancyTail (a ε t : ℝ) : ℝ
theorem
BanditRLProof.Concentration.cappedOccupancyTail_nonneg
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book · Reinforcement Learning Book · Online Learning Book
2. Probability, kernels, filtrations, and concentration
Canonical node identity
declaration:BanditRLProof.Concentration.cappedOccupancyTail_nonnegReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem cappedOccupancyTail_nonneg (a ε t : ℝ) : 0 ≤ cappedOccupancyTail a ε t
theorem
BanditRLProof.Concentration.cappedOccupancyTail_antitone
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book · Reinforcement Learning Book · Online Learning Book
2. Probability, kernels, filtrations, and concentration
Canonical node identity
declaration:BanditRLProof.Concentration.cappedOccupancyTail_antitoneReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem cappedOccupancyTail_antitone (a ε : ℝ) (ha : 0 < a) (hε : 0 < ε) : Antitone (cappedOccupancyTail a ε)
theorem
BanditRLProof.Concentration.integral_cappedOccupancyTail
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book · Reinforcement Learning Book · Online Learning Book
2. Probability, kernels, filtrations, and concentration
Canonical node identity
declaration:BanditRLProof.Concentration.integral_cappedOccupancyTailReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem integral_cappedOccupancyTail (a ε : ℝ) (ha : 0 < a) (hε : 0 < ε) : IntegrableOn (cappedOccupancyTail a ε) (Ioi 0) ∧ (∫ t in Ioi 0, cappedOccupancyTail a ε t) = (2/ε^2)*(a+sqrt (Real.pi*a)+1)
theorem
BanditRLProof.Concentration.sum_le_occupancy_bound_sharp
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book · Reinforcement Learning Book · Online Learning Book
2. Probability, kernels, filtrations, and concentration
Canonical node identity
declaration:BanditRLProof.Concentration.sum_le_occupancy_bound_sharpReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem sum_le_occupancy_bound_sharp (p : ℕ → ℝ) (a ε : ℝ) (ha : 0 < a) (hε : 0 < ε) (h1 : ∀ s, p s ≤ 1) (htail : ∀ s : ℕ, 2*a/ε^2 < (s : ℝ) → p s ≤ occupancyTail a ε s) (n : ℕ) : (∑ i ∈ Finset.range n, p (i+1)) ≤ (2/ε^2)*(a+sqrt (Real.pi*a)+1)