Lean module · Probability layer
BanditRLProof.ConcentrationGaussianOccupancy
Generated source map for this Lean module.
Module map
Imports
No project-local imports.
Imported by
BanditRLProof, BanditRLProof.ConcentrationCappedOccupancy, BanditRLProof.ConcentrationIndexOccupancy
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.Concentration.integral_mul_exp_neg_mul_sq_Ioi
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_mul_exp_neg_mul_sq_IoiReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem integral_mul_exp_neg_mul_sq_Ioi (b : ℝ) (hb : 0 < b) : ∫ x : ℝ in Ioi 0, x*exp (-b*x^2) = (2*b)⁻¹
theorem
BanditRLProof.Concentration.integral_transformed_occupancy_tail
Compiled
Exact transformed tail integral in source Lemma 8.2.
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_transformed_occupancy_tailReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem integral_transformed_occupancy_tail (a ε : ℝ) (ha : 0 < a) (hε : 0 < ε) : ∫ z : ℝ in Ioi 0, (2/ε^2)*(z+sqrt (2*a))*exp (-(1/2 : ℝ)*z^2) = (2/ε^2)*(1+sqrt (Real.pi*a))
def
BanditRLProof.Concentration.occupancyTail
Compiled
The shifted Gaussian kernel after the algebraic square-root rewrite.
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.occupancyTailReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
def occupancyTail (a ε t : ℝ) : ℝ
theorem
BanditRLProof.Concentration.occupancyTail_antitoneOn
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.occupancyTail_antitoneOnReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem occupancyTail_antitoneOn (a ε : ℝ) (ha : 0 < a) (hε : 0 < ε) : AntitoneOn (occupancyTail a ε) (Ici (2*a/ε^2))
def
BanditRLProof.Concentration.occupancySubstitution
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.occupancySubstitutionReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
def occupancySubstitution (a ε z : ℝ) : ℝ
theorem
BanditRLProof.Concentration.occupancySubstitution_image
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.occupancySubstitution_imageReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem occupancySubstitution_image (a ε : ℝ) (ha : 0 < a) (hε : 0 < ε) : occupancySubstitution a ε '' Ioi 0 = Ioi (2*a/ε^2)
theorem
BanditRLProof.Concentration.occupancySubstitution_injOn
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.occupancySubstitution_injOnReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem occupancySubstitution_injOn (a ε : ℝ) (ha : 0 < a) (hε : 0 < ε) : InjOn (occupancySubstitution a ε) (Ioi 0)
theorem
BanditRLProof.Concentration.hasDerivAt_occupancySubstitution
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.hasDerivAt_occupancySubstitutionReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem hasDerivAt_occupancySubstitution (a ε z : ℝ) : HasDerivAt (occupancySubstitution a ε) ((2/ε^2)*(z+sqrt (2*a))) z
theorem
BanditRLProof.Concentration.integral_occupancyTail
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_occupancyTailReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem integral_occupancyTail (a ε : ℝ) (ha : 0 < a) (hε : 0 < ε) : ∫ t in Ioi (2*a/ε^2), occupancyTail a ε t = (2/ε^2)*(1+sqrt (Real.pi*a))
theorem
BanditRLProof.Concentration.integrableOn_occupancyTail
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.integrableOn_occupancyTailReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem integrableOn_occupancyTail (a ε : ℝ) (ha : 0 < a) (hε : 0 < ε) : IntegrableOn (occupancyTail a ε) (Ioi (2*a/ε^2))
theorem
BanditRLProof.Concentration.sum_occupancyTail_shift_le
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_occupancyTail_shift_leReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem sum_occupancyTail_shift_le (a ε r : ℝ) (ha : 0 < a) (hε : 0 < ε) (hr : 2*a/ε^2 ≤ r) (N : ℕ) : (∑ i ∈ Finset.range N, occupancyTail a ε (r+(i+1 : ℕ))) ≤ (2/ε^2)*(1+sqrt (Real.pi*a))
theorem
BanditRLProof.Concentration.sum_le_occupancy_bound
Compiled
Integer cutoff aggregation with the exact source Lemma 8.2 constants.
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_boundReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem sum_le_occupancy_bound (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)) ≤ 1+(2/ε^2)*(a+sqrt (Real.pi*a)+1)