Lean module · Foundations
BanditRLProof.HOOCantorRate
A conservative finite dimension certificate and full-rate instantiation for the infinite-arm noisy Cantor model. The certificate is an upper bound, not a claim that its exact near-optimality dimension equals two.
Module map
Imports
BanditRLProof.HOOCantorModel, BanditRLProof.Algorithms.HOOActualRegret
Imported by
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.HOO.CantorModel.packing_le_two_div
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.HOO.CantorModel.packing_le_two_divReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem packing_le_two_div (A : Set Arm) {ε : ℝ} (hε : 0<ε) (hε1 : ε≤1) : (covering.packingNumber A ε : ℝ) ≤ 2/ε
theorem
BanditRLProof.HOO.CantorModel.dimension_le_two
Compiled
Conservative upper certificate, sufficient for a nonvacuous full-rate canary. It follows from ambient packing, not a postulated dimension value.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.HOO.CantorModel.dimension_le_twoReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem dimension_le_two (c : ℝ) : covering.nearOptimalityDimension mean (1/2) c ≤ (2:EReal)
theorem
BanditRLProof.HOO.CantorModel.expected_actual_rate
Compiled
A concrete full-rate consequence with d'=3>dimension. The general theorem retains every d' strictly above the actual dimension; this model certificate is deliberately conservative and does not claim the sharp model exponent.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Indexed settings: Lipschitz bandits
Canonical node identity
declaration:BanditRLProof.HOO.CantorModel.expected_actual_rateReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem expected_actual_rate : ∃ γ : ℝ, 0<γ ∧ ∀ N : ℕ, 1≤N → (∫ Y, (∑ n ∈ Finset.range N, ((1/2:ℝ)-Y n)) ∂trajectory 1 (1/2) (covering.toCovering.nodeLaw law)) ≤ γ*(N:ℝ)^(4/5:ℝ)*(Real.log (max (N:ℝ) 2))^(1/5:ℝ)