Lean module · Foundations
BanditRLProof.Algorithms.HOORate
Repaired source Theorem 6: actual HOO expected pseudo-regret at all positive horizons, with a horizon-independent constant.
Module map
Imports
BanditRLProof.Algorithms.HOODepthOptimization
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.expected_pseudoRegret_rate
Compiled
Every real exponent strictly above the actual near-optimality dimension admits the source rate for the constructed causal HOO process. The logarithm repair is log(max(N,2)); the confidence and algorithm use the same repair.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.HOO.RegularCovering.expected_pseudoRegret_rateReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem RegularCovering.expected_pseudoRegret_rate {X : Type*} [MeasurableSpace X] (C : RegularCovering X) (law : Kernel X ℝ) [IsMarkovKernel law] (f : X → ℝ) (best d : ℝ) (hmean : ∀x, (∫ y, y ∂law x)=f x) (hf : ∀x, f x≤best) (hfrange : ∀x, f x ∈ Set.Icc (0:ℝ) 1) (hbest : regionSup f Set.univ=best) (hw : WeaklyLipschitz f C.ell best) (hbound : ∀x, ∀ᵐ y ∂law x, y ∈ Set.Icc (0:ℝ) 1) (hd : C.nearOptimalityDimension f best (4*C.nu1/C.nu2) < (d:EReal)) : ∃ γ : ℝ, 0<γ ∧ ∀ N : ℕ, 1≤N → (∫ Y, (∑ n ∈ Finset.range N, (best-f (C.toCovering.arm C.nu1 C.rho Y n))) ∂trajectory C.nu1 C.rho (C.toCovering.nodeLaw law)) ≤ γ*(N:ℝ)^((d+1)/(d+2))*(Real.log (max (N:ℝ) 2))^(1/(d+2))