Lean module · Foundations
BanditRLProof.Algorithms.CUCBFiniteConcavity
The source finite-concavity obligation, instantiated with actual under-sampled charge counts, including zero counts and zero horizon.
Module map
Imports
BanditRLProof.Algorithms.CUCBGapCutoff
Imported by
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.CUCB.SourceModel.finite_power_sum_le
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.CUCB.SourceModel.finite_power_sum_leReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem finite_power_sum_le {m : ℕ} (hm : 0<m) (z : Fin m → ℝ) (hz : ∀i, 0≤z i) (H p : ℝ) (hp0 : 0≤p) (hp1 : p≤1) (hH : (∑i:Fin m, z i)≤H) : (∑i:Fin m, (z i)^p)≤(m:ℝ)^(1-p)*H^p
theorem
BanditRLProof.CUCB.SourceModel.underChargeCount_power_sum_le
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
Indexed settings: Combinatorial bandits
Canonical node identity
declaration:BanditRLProof.CUCB.SourceModel.underChargeCount_power_sum_leReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem underChargeCount_power_sum_le (H : ℕ) (actions : ℕ → A) (ω : ℝ) (hω : 0<ω) (hω1 : ω≤1) : (∑i:Fin m, ((S.underChargeTimes H actions i).card:ℝ)^(1-ω/2))≤ (m:ℝ)^(ω/2)*(H:ℝ)^(1-ω/2)