Lean module · Foundations
BanditRLProof.Algorithms.HOOExpectedRegret
Integrability and the unoptimized expected HOO regret bound, on the actual trajectory. Mean boundedness is a native source-model hypothesis.
Module map
Imports
BanditRLProof.Algorithms.HOORegretPartition
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.integrable_actual_gap
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.integrable_actual_gapReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem RegularCovering.integrable_actual_gap {X : Type*} [MeasurableSpace X] (C : RegularCovering X) (f : X → ℝ) (best : ℝ) (hfrange : ∀x, f x ∈ Set.Icc (0:ℝ) 1) (μ : Measure (ℕ → ℝ)) [IsProbabilityMeasure μ] (n : ℕ) : Integrable (fun Y => best-f (C.toCovering.arm C.nu1 C.rho Y n)) μ
theorem
BanditRLProof.HOO.RegularCovering.expected_regret_partition_bound
Compiled
Expected regret with an arbitrary integer cutoff H, retaining the exact three terms. All random count bounds come from the actual HOO law.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.HOO.RegularCovering.expected_regret_partition_boundReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem RegularCovering.expected_regret_partition_bound {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) (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) (H 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)) ≤ 4*(C.nu1*C.rho^H)*N + (∑ h ∈ Finset.range H, 4*(C.nu1*C.rho^h)*(C.nearOptimalNodes f best h).card) + ∑ h ∈ Finset.range H, 4*(C.nu1*C.rho^h)*(C.boundaryNodes f best h).card * (8*Real.log (max (N:ℝ) 2)/(C.nu1*C.rho^(h+1))^2+4)
theorem
BanditRLProof.HOO.RegularCovering.expected_regret_dimension_sums
Compiled
Definition-5 dimension supplies one constant for every cutoff and horizon; the remaining finite geometric sums are explicit, not hidden in an O premise.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.HOO.RegularCovering.expected_regret_dimension_sumsReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem RegularCovering.expected_regret_dimension_sums {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)) : ∃ K : ℝ, 0<K ∧ ∀ H 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)) ≤ 4*(C.nu1*C.rho^H)*N + (∑ h ∈ Finset.range H, 4*(C.nu1*C.rho^h)*(K*(C.nu2*C.rho^h)^(-d))) + ∑ h ∈ Finset.range H, 8*(C.nu1*C.rho^h)*(K*(C.nu2*C.rho^h)^(-d)) * (8*Real.log (max (N:ℝ) 2)/(C.nu1*C.rho^(h+1))^2+4)