Lean module · Foundations
BanditRLProof.HOOLevels
Finite complete levels of the infinite HOO covering tree.
Module map
Imports
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.nodesAtDepth
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.nodesAtDepthReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
def nodesAtDepth (n : ℕ) : Finset Node
theorem
BanditRLProof.HOO.mem_nodesAtDepth
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.mem_nodesAtDepthReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
@[simp] theorem mem_nodesAtDepth (v : Node) (n : ℕ) : v ∈ nodesAtDepth n ↔ v.length=n
theorem
BanditRLProof.HOO.card_nodesAtDepth
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.card_nodesAtDepthReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
@[simp] theorem card_nodesAtDepth (n : ℕ) : (nodesAtDepth n).card = 2^n
theorem
BanditRLProof.HOO.Covering.exists_region_at_depth
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.Covering.exists_region_at_depthReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem Covering.exists_region_at_depth {X : Type*} (C : Covering X) (n : ℕ) (x : X) : ∃ v ∈ nodesAtDepth n, x ∈ C.region v
theorem
BanditRLProof.HOO.RegularCovering.disjoint_ball_family_card_le
Compiled
Coarse-scale finite packing bound from A1 alone, valid for asymmetric dissimilarities without a triangle inequality.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.HOO.RegularCovering.disjoint_ball_family_card_leReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem RegularCovering.disjoint_ball_family_card_le {X I : Type*} [MeasurableSpace X] [Fintype I] (C : RegularCovering X) (centers : I → X) (ε : ℝ) (h : ℕ) (hε : C.nu1*C.rho^h < ε) (hd : Pairwise (fun i j => Disjoint {y | C.ell (centers i) y < ε} {y | C.ell (centers j) y < ε})) : Fintype.card I ≤ 2^h
theorem
BanditRLProof.HOO.RegularCovering.exists_finite_packing_bound
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.exists_finite_packing_boundReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem RegularCovering.exists_finite_packing_bound {X : Type*} [MeasurableSpace X] (C : RegularCovering X) (ε : ℝ) (hε : 0 < ε) : ∃ M : ℕ, ∀ (I : Type) [Fintype I] (centers : I → X), Pairwise (fun i j => Disjoint {y | C.ell (centers i) y < ε} {y | C.ell (centers j) y < ε}) → Fintype.card I ≤ M