Lean module · Foundations
BanditRLProof.Algorithms.MOSSOccupancy
Generated source map for this Lean module.
Module map
Imports
BanditRLProof.Algorithms.MOSSOptimism, BanditRLProof.PullCountReindex
Imported by
BanditRLProof, BanditRLProof.Algorithms.MOSSExpectedOccupancy
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
def
BanditRLProof.MOSS.fixedLogRadius
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.MOSS.fixedLogRadiusReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
def fixedLogRadius (δ gap : ℝ) (s : ℕ) : ℝ
theorem
BanditRLProof.MOSS.sampleRadius_le_fixedLogRadius
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.MOSS.sampleRadius_le_fixedLogRadiusReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem sampleRadius_le_fixedLogRadius (δ gap : ℝ) (s : ℕ) (hδ : 0 < δ) (hg : 0 < gap) (hs : 0 < s) (hlarge : 1 ≤ (s : ℝ)*gap^2) : sqrt (4/(s : ℝ)*logPlus (1/((s : ℝ)*δ))) ≤ fixedLogRadius δ gap s
def
BanditRLProof.MOSS.indexExceedanceCount
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.MOSS.indexExceedanceCountReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
def indexExceedanceCount (mean : ℕ → ℝ) (δ gap : ℝ) (n : ℕ) : ℝ
theorem
BanditRLProof.MOSS.pullCount_le_one_add_indexExceedanceCount
Compiled
Deterministic count transport; the MOSS policy event is a separate obligation.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.MOSS.pullCount_le_one_add_indexExceedanceCountReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem pullCount_le_one_add_indexExceedanceCount {Action : Type*} [DecidableEq Action] (action : ActionTrace Action) (a : Action) (mean : ℕ → ℝ) (δ gap : ℝ) (n : ℕ) (hselected : ∀ t < n, action t = a → 0 < pullCount action a t → gap/2 ≤ mean (pullCount action a t) + sqrt (4/(pullCount action a t : ℝ)*logPlus (1/((pullCount action a t : ℝ)*δ)))) : (pullCount action a n : ℝ) ≤ 1 + indexExceedanceCount mean δ gap n
def
BanditRLProof.MOSS.fixedLogExceedanceCount
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.MOSS.fixedLogExceedanceCountReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
def fixedLogExceedanceCount (mean : ℕ → ℝ) (δ gap : ℝ) (n : ℕ) : ℝ
def
BanditRLProof.MOSS.smallSampleCount
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.MOSS.smallSampleCountReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
def smallSampleCount (gap : ℝ) (n : ℕ) : ℝ
theorem
BanditRLProof.MOSS.indexExceedanceCount_le_small_add_fixed
Compiled
Source correction step before applying Lemma 8.2, with no stochastic premise.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.MOSS.indexExceedanceCount_le_small_add_fixedReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem indexExceedanceCount_le_small_add_fixed (mean : ℕ → ℝ) (δ gap : ℝ) (hδ : 0 < δ) (hg : 0 < gap) (n : ℕ) : indexExceedanceCount mean δ gap n ≤ smallSampleCount gap n + fixedLogExceedanceCount mean δ gap n
theorem
BanditRLProof.MOSS.smallSampleCount_le_horizon
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.MOSS.smallSampleCount_le_horizonReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem smallSampleCount_le_horizon (gap : ℝ) (n : ℕ) : smallSampleCount gap n ≤ (n : ℝ)
theorem
BanditRLProof.MOSS.smallSampleCount_le_inv_sq
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.MOSS.smallSampleCount_le_inv_sqReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem smallSampleCount_le_inv_sq (gap : ℝ) (hg : 0 < gap) (n : ℕ) : smallSampleCount gap n ≤ 1/gap^2
theorem
BanditRLProof.MOSS.indexExceedanceCount_le_inv_sq_add_fixed
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.MOSS.indexExceedanceCount_le_inv_sq_add_fixedReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem indexExceedanceCount_le_inv_sq_add_fixed (mean : ℕ → ℝ) (δ gap : ℝ) (hδ : 0 < δ) (hg : 0 < gap) (n : ℕ) : indexExceedanceCount mean δ gap n ≤ 1/gap^2 + fixedLogExceedanceCount mean δ gap n