Lean module · Probability layer
BanditRLProof.ConcentrationTailIntegration
Generated source map for this Lean module.
Module map
Imports
No project-local imports.
Imported by
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.Concentration.integral_positive_tail_le_two_sqrt
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_positive_tail_le_two_sqrtReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem integral_positive_tail_le_two_sqrt (f : ℝ → ℝ) (hf : Measurable f) (hn : ∀ t, 0 ≤ f t) (h1 : ∀ t, f t ≤ 1) (c : ℝ) (hc : 0 < c) (ht : ∀ t, 0 < t → f t ≤ c/t^2) : ∫ t in Ioi 0, f t ≤ 2*sqrt c