Lean module · Foundations
BanditRLProof.Algorithms.HOOConfidence
Finite visit-count peeling for HOO. The time parameter is the number of already observed chronological rewards; the bound applies to the next decision.
Module map
Imports
BanditRLProof.Algorithms.HOOConcentration, BanditRLProof.ProbabilityUnionBound
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.regionDeviation
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.regionDeviationReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def regionDeviation (ν ρ : ℝ) (law : Kernel Node ℝ) (v : Node) (n : ℕ) (lower : Bool) (Y : ℕ → ℝ) : ℝ
theorem
BanditRLProof.HOO.visits_history_le
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.visits_history_leReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem visits_history_le (ν ρ : ℝ) (v : Node) (n : ℕ) (Y : ℕ → ℝ) : visits (history ν ρ Y n) v ≤ n
theorem
BanditRLProof.HOO.region_deviation_slice
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.region_deviation_sliceReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem region_deviation_slice (ν ρ : ℝ) (law : Kernel Node ℝ) [IsMarkovKernel law] (hbound : ∀ a, ∀ᵐ y ∂law a, y ∈ Set.Icc (0 : ℝ) 1) (v : Node) (n k : ℕ) (lower : Bool) (L : ℝ) (hL : 0 ≤ L) (hk : 0 < k) : (trajectory ν ρ law) {Y | Real.sqrt (2 * (k : ℝ) * L) ≤ regionDeviation ν ρ law v n lower Y ∧ (visits (history ν ρ Y n) v : ℝ) ≤ k} ≤ ENNReal.ofReal (Real.exp (-4*L))
theorem
BanditRLProof.HOO.region_deviation_confidence
Compiled
One-sided confidence for the empirical regional noise, with its actual random visit count. The Boolean selects the upper or lower deviation.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.HOO.region_deviation_confidenceReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem region_deviation_confidence (ν ρ : ℝ) (law : Kernel Node ℝ) [IsMarkovKernel law] (hbound : ∀ a, ∀ᵐ y ∂law a, y ∈ Set.Icc (0 : ℝ) 1) (v : Node) (n : ℕ) (lower : Bool) (L : ℝ) (hL : 0 ≤ L) : (trajectory ν ρ law) {Y | 0 < visits (history ν ρ Y n) v ∧ Real.sqrt (2 * (visits (history ν ρ Y n) v : ℝ) * L) ≤ regionDeviation ν ρ law v n lower Y} ≤ (n : ENNReal) * ENNReal.ofReal (Real.exp (-4*L))