Lean module · Probability layer
BanditRLProof.ConcentrationDyadicExponential
A convex-exponential comparison gives a dyadic sum estimate strong enough to imply the constant 15 used in source Lemma 9.3.
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.mul_exp_neg_le_exp_difference
Compiled
A telescoping majorant obtained from `x/3 ≤ sinh(x/3)`.
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.mul_exp_neg_le_exp_differenceReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem mul_exp_neg_le_exp_difference (x : ℝ) (hx : 0 ≤ x) : x * exp (-x) ≤ (3 / 2 : ℝ) * (exp (-(2 * x / 3)) - exp (-(4 * x / 3)))
theorem
BanditRLProof.Concentration.sum_dyadic_mul_exp_neg_le
Compiled
Finite dyadic exponential sum, with the remaining terminal mass retained.
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_dyadic_mul_exp_neg_leReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem sum_dyadic_mul_exp_neg_le (a : ℝ) (ha : 0 < a) (N : ℕ) : ∑ j ∈ range N, (2 : ℝ) ^ j * exp (-(a * 2 ^ j)) ≤ 3 / (2 * a) * (exp (-(2 * a / 3)) - exp (-(2 * (a * 2 ^ N) / 3)))
theorem
BanditRLProof.Concentration.sum_dyadic_mul_exp_neg_le_three_div_two
Compiled
Uniform finite-prefix bound; no logarithm or integral comparison loss.
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_dyadic_mul_exp_neg_le_three_div_twoReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem sum_dyadic_mul_exp_neg_le_three_div_two (a : ℝ) (ha : 0 < a) (N : ℕ) : ∑ j ∈ range N, (2 : ℝ) ^ j * exp (-(a * 2 ^ j)) ≤ 3 / (2 * a)
theorem
BanditRLProof.Concentration.tsum_dyadic_mul_exp_neg_le
Compiled
Countable dyadic sum in the probability-friendly extended nonnegative reals.
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.tsum_dyadic_mul_exp_neg_leReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem tsum_dyadic_mul_exp_neg_le (a : ℝ) (ha : 0 < a) : (∑' j : ℕ, ENNReal.ofReal ((2 : ℝ) ^ j * exp (-(a * 2 ^ j)))) ≤ ENNReal.ofReal (3 / (2 * a))
theorem
BanditRLProof.Concentration.sum_moss_peeling_exponential_le_twelve
Compiled
The geometric series in source Lemma 9.3 is at most 12 delta/gap^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.sum_moss_peeling_exponential_le_twelveReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem sum_moss_peeling_exponential_le_twelve (δ gap : ℝ) (hδ : 0 ≤ δ) (hgap : 0 < gap) (N : ℕ) : ∑ j ∈ range N, δ * (2 : ℝ) ^ (j+1) * exp (-(gap ^ 2 / 4 * 2 ^ j)) ≤ 12 * δ / gap ^ 2
theorem
BanditRLProof.Concentration.tsum_moss_peeling_exponential_le_fifteen
Compiled
Source-constant countable series bound, with no weakened constant.
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.tsum_moss_peeling_exponential_le_fifteenReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem tsum_moss_peeling_exponential_le_fifteen (δ gap : ℝ) (hδ : 0 ≤ δ) (hgap : 0 < gap) : (∑' j : ℕ, ENNReal.ofReal (δ * (2 : ℝ) ^ (j+1) * exp (-(gap ^ 2 / 4 * 2 ^ j)))) ≤ ENNReal.ofReal (15 * δ / gap ^ 2)