Lean module · Foundations
BanditRLProof.Algorithms.MOSSHistory
An inclusive history at t contains t+1 observations; the successor selector therefore calls the source action at t+1. No reward law or concentration certificate is required to construct this deterministic Markov policy.
Module map
Imports
BanditRLProof.Algorithms.MOSS, BanditRLProof.Algorithms.UCBRealHistoryIndex, BanditRLProof.Algorithms.ThompsonAlgorithmDensityProcess
Imported by
BanditRLProof, BanditRLProof.Algorithms.MOSSStreamMeasurable
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
def
BanditRLProof.MOSS.historyAction
Compiled
Source MOSS action after an inclusive finite action/reward history.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.MOSS.historyActionReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def historyAction {k : ℕ} (hk : 0 < k) (n t : ℕ) (history : History.FinitePairHistory (Fin k) ℝ t) : Fin k
theorem
BanditRLProof.MOSS.measurable_historyAction
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.measurable_historyActionReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem measurable_historyAction {k : ℕ} (hk : 0 < k) (n t : ℕ) : Measurable (historyAction hk n t)
def
BanditRLProof.MOSS.historyAlgorithm
Compiled
Concrete MOSS policy on the history interface shared by Chapter 13's minimax regret functional. Initial action is arm zero.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret · Chapter 13: Lower Bounds: Basic Ideas
Canonical node identity
declaration:BanditRLProof.MOSS.historyAlgorithmReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def historyAlgorithm {k : ℕ} (hk : 0 < k) (n : ℕ) : Thompson.HistoryAlgorithm (Fin k) ℝ where
theorem
BanditRLProof.MOSS.historyAlgorithm_policy_apply
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.historyAlgorithm_policy_applyReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
@[simp] theorem historyAlgorithm_policy_apply {k : ℕ} (hk : 0 < k) (n t : ℕ) (history : History.FinitePairHistory (Fin k) ℝ t) : (historyAlgorithm hk n).policy t history = Measure.dirac (historyAction hk n t history)
theorem
BanditRLProof.MOSS.historyAction_initialization
Compiled
Subsequent initialization rounds select the corresponding arm.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.MOSS.historyAction_initializationReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem historyAction_initialization {k : ℕ} (hk : 0 < k) (n t : ℕ) (history : History.FinitePairHistory (Fin k) ℝ t) (ht : t + 1 < k) : historyAction hk n t history = ⟨t + 1, ht⟩
theorem
BanditRLProof.MOSS.historyAction_index_max
Compiled
Exact post-initialization source index maximality on visible history.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.MOSS.historyAction_index_maxReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem historyAction_index_max {k : ℕ} (hk : 0 < k) (n t : ℕ) (history : History.FinitePairHistory (Fin k) ℝ t) (ht : k ≤ t + 1) (a : Fin k) : index n (ETC.realHistoryEmpMean t history) (ETC.realHistoryPullCount t history) a ≤ index n (ETC.realHistoryEmpMean t history) (ETC.realHistoryPullCount t history) (historyAction hk n t history)