BanditRLlib
Lean gate passed before this site build; local proof declarations are shown as compiled.Lean-verified build · exact declarations linked.

Lean module · Foundations

BanditRLProof.Algorithms.HOOExpectedVisits

Expected HOO regional visits through the shared threshold-count argument. The binary trace below records visits to one fixed region; it does not replace the infinite HOO action space or its reward trajectory by a finite-arm model.

Module map

Declarations
10
Placeholders
0

Imports

BanditRLProof.Algorithms.HOOSelectionTail, BanditRLProof.HOOTailSum, BanditRLProof.Algorithms.HeavyTailExpectedCount

Imported by

BanditRLProof, BanditRLProof.Algorithms.HOORegretPartition, BanditRLProof.HOOCantorModel

Declarations

Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.

def BanditRLProof.HOO.visitTrace 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 identitydeclaration:BanditRLProof.HOO.visitTrace

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

noncomputable def visitTrace (ν ρ : ℝ) (v : Node) (Y : ℕ → ℝ) : ActionTrace (Fin 2)
Source line 11 Chapter context: Foundations
theorem BanditRLProof.HOO.measurable_visitTrace 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 identitydeclaration:BanditRLProof.HOO.measurable_visitTrace

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem measurable_visitTrace (ν ρ : ℝ) (v : Node) (i : ℕ) : Measurable (fun Y => visitTrace ν ρ v Y i)
Source line 14 Chapter context: Foundations
theorem BanditRLProof.HOO.visitTrace_zero_iff 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 identitydeclaration:BanditRLProof.HOO.visitTrace_zero_iff

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

@[simp] theorem visitTrace_zero_iff (ν ρ : ℝ) (v : Node) (Y : ℕ → ℝ) (i : ℕ) : visitTrace ν ρ v Y i = 0 ↔ v <+: action ν ρ Y i
Source line 19 Chapter context: Foundations
theorem BanditRLProof.HOO.visitTrace_pullCount 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 identitydeclaration:BanditRLProof.HOO.visitTrace_pullCount

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem visitTrace_pullCount (ν ρ : ℝ) (v : Node) (Y : ℕ → ℝ) (n : ℕ) : pullCount (visitTrace ν ρ v Y) 0 n = visits (history ν ρ Y n) v
Source line 24 Chapter context: Foundations
theorem BanditRLProof.HOO.lintegral_visits_threshold 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 identitydeclaration:BanditRLProof.HOO.lintegral_visits_threshold

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem lintegral_visits_threshold (ν ρ : ℝ) (v : Node) (μ : Measure (ℕ → ℝ)) [IsProbabilityMeasure μ] (N B : ℕ) : (∫⁻ Y, (visits (history ν ρ Y N) v : ENNReal) ∂μ) ≤ B + ∑ n ∈ Finset.range N, μ {Y | v <+: action ν ρ Y n ∧ B ≤ visits (history ν ρ Y n) v}
Source line 32 Chapter context: Foundations
def BanditRLProof.HOO.visitThreshold 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 identitydeclaration:BanditRLProof.HOO.visitThreshold

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

noncomputable def visitThreshold (gap : ℝ) (N : ℕ) : ℕ
Source line 39 Chapter context: Foundations
theorem BanditRLProof.HOO.visitThreshold_controls 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 identitydeclaration:BanditRLProof.HOO.visitThreshold_controls

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem visitThreshold_controls (gap : ℝ) (N n : ℕ) (hn : n ≤ N) : 8*Real.log (max (n:ℝ) 2)/gap^2 ≤ (visitThreshold gap N : ℝ)
Source line 42 Chapter context: Foundations
theorem BanditRLProof.HOO.RegularCovering.poor_region_lintegral_visits 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 identitydeclaration:BanditRLProof.HOO.RegularCovering.poor_region_lintegral_visits

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem RegularCovering.poor_region_lintegral_visits {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 : ℕ) : (∫⁻ Y, (visits (history C.nu1 C.rho Y N) v : ENNReal) ∂trajectory C.nu1 C.rho (C.toCovering.nodeLaw law)) ≤ visitThreshold (best-regionSup f (C.region v)-C.nu1*C.rho^v.length) N + 3
Source line 50 Chapter context: Foundations
theorem BanditRLProof.HOO.integrable_visits 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 identitydeclaration:BanditRLProof.HOO.integrable_visits

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem integrable_visits (ν ρ : ℝ) (v : Node) (μ : Measure (ℕ → ℝ)) [IsProbabilityMeasure μ] (N : ℕ) : Integrable (fun Y => (visits (history ν ρ Y N) v : ℝ)) μ
Source line 84 Chapter context: Foundations
theorem BanditRLProof.HOO.RegularCovering.poor_region_expected_visits Compiled

Expected poor-region visits, with the source additive-four shape and an explicit logarithm repair at horizons zero and one. All probability and search premises are produced from the actual HOO algorithm and A1/A2 model.

Used in these reading views: Bandit Book

1. Finite bandits, traces, and regret

Canonical node identitydeclaration:BanditRLProof.HOO.RegularCovering.poor_region_expected_visits

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem RegularCovering.poor_region_expected_visits {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 : ℕ) : (∫ Y, (visits (history C.nu1 C.rho Y N) v : ℝ) ∂trajectory C.nu1 C.rho (C.toCovering.nodeLaw law)) ≤ 8*Real.log (max (N:ℝ) 2)/(best-regionSup f (C.region v)-C.nu1*C.rho^v.length)^2 + 4
Source line 99 Chapter context: Foundations