Lean module · Foundations
BanditRLProof.HOOGeometry
Source A2 and Lemma 3 for general dissimilarities. No metric triangle inequality, maximizer, or attainment of a regional supremum is assumed.
Module map
Imports
BanditRLProof.Algorithms.HOOTree
Imported by
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
def
BanditRLProof.HOO.WeaklyLipschitz
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.WeaklyLipschitzReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
def WeaklyLipschitz {X : Type*} (f : X → ℝ) (ell : X → X → ℝ) (best : ℝ) : Prop
def
BanditRLProof.HOO.regionSup
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.regionSupReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def regionSup {X : Type*} (f : X → ℝ) (A : Set X) : ℝ
theorem
BanditRLProof.HOO.region_gap_le
Compiled
First part of source Lemma 3, retaining the region's exact suboptimality.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.HOO.region_gap_leReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem region_gap_le {X : Type*} (f : X → ℝ) (ell : X → X → ℝ) (best D : ℝ) (A : Set X) (hA : A.Nonempty) (hw : WeaklyLipschitz f ell best) (hdiam : ∀ x ∈ A, ∀ y ∈ A, ell x y ≤ D) (y : X) (hy : y ∈ A) : best - f y ≤ (best - regionSup f A) + max (best - regionSup f A) D
theorem
BanditRLProof.HOO.near_optimal_region
Compiled
Source Lemma 3, including c=0 and the max(2c,c+1) constant.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.HOO.near_optimal_regionReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem near_optimal_region {X : Type*} (f : X → ℝ) (ell : X → X → ℝ) (best D c : ℝ) (A : Set X) (hA : A.Nonempty) (hD : 0 ≤ D) (hw : WeaklyLipschitz f ell best) (hdiam : ∀ x ∈ A, ∀ y ∈ A, ell x y ≤ D) (hgap : best - regionSup f A ≤ c*D) (y : X) (hy : y ∈ A) : best - f y ≤ max (2*c) (c+1)*D