Lean module · Foundations
BanditRLProof.Algorithms.HOOSelectionTail
Selection of a sufficiently visited poor region forces a confidence failure for that region or for a finite prefix of a supremum-optimal branch.
Module map
Imports
BanditRLProof.Algorithms.HOOIndexConfidence, BanditRLProof.Algorithms.HOOPathComparison
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.RegularCovering.poor_region_selection_tail
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.RegularCovering.poor_region_selection_tailReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem RegularCovering.poor_region_selection_tail {X : Type*} [MeasurableSpace X] (C : RegularCovering X) (law : Kernel X ℝ) [IsMarkovKernel law] (f : X → ℝ) (best : ℝ) (hmean : ∀ x, (∫ y, y ∂law x) = f x) (hf : ∀ x, f x ≤ best) (hbest : regionSup f Set.univ = best) (hw : WeaklyLipschitz f C.ell best) (hbound : ∀ x, ∀ᵐ y ∂law x, y ∈ Set.Icc (0 : ℝ) 1) (v : Node) (hv : C.nu1*C.rho^v.length < best-regionSup f (C.region v)) (n : ℕ) : (trajectory C.nu1 C.rho (C.toCovering.nodeLaw law)) {Y | 8*Real.log (max (n:ℝ) 2)/(best-regionSup f (C.region v)-C.nu1*C.rho^v.length)^2 ≤ (visits (history C.nu1 C.rho Y n) v : ℝ) ∧ v <+: action C.nu1 C.rho Y n} ≤ ((n:ENNReal)+2) * ((n:ENNReal) * ENNReal.ofReal (Real.exp (-4*Real.log (max (n:ℝ) 2))))