Lean module · Foundations
BanditRLProof.Algorithms.ArmStreamPolicy
A measurable history selector driven by the existing latent reward streams. This generalizes the UCB recursion without changing its reward/count semantics.
Module map
Imports
BanditRLProof.Algorithms.UCBArmStreamProcess
Imported by
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
def
BanditRLProof.ArmStreamPolicy.history
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.ArmStreamPolicy.historyReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def history (initial : Fin K) (select : (n : ℕ) → History.FinitePairHistory (Fin K) ℝ n → Fin K) (stream : UCB.ArmRewardStream K) : (n : ℕ) → History.FinitePairHistory (Fin K) ℝ n | 0 => fun _ => (initial, stream 0 initial) | n + 1 => let h := history initial select stream n let a := select n h History.extendPairHistorySucc h (a, stream (ETC.realHistoryPullCount n h a) a) noncomputable def action (initial : Fin K) (select : (n : ℕ) → History.FinitePairHistory (Fin K) ℝ n → Fin K) (stream : UCB.ArmRewardStream K) : ActionTrace (Fin K)
def
BanditRLProof.ArmStreamPolicy.action
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.ArmStreamPolicy.actionReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def action (initial : Fin K) (select : (n : ℕ) → History.FinitePairHistory (Fin K) ℝ n → Fin K) (stream : UCB.ArmRewardStream K) : ActionTrace (Fin K)
def
BanditRLProof.ArmStreamPolicy.reward
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.ArmStreamPolicy.rewardReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def reward (initial : Fin K) (select : (n : ℕ) → History.FinitePairHistory (Fin K) ℝ n → Fin K)
theorem
BanditRLProof.ArmStreamPolicy.action_zero
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.ArmStreamPolicy.action_zeroReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
@[simp] theorem action_zero (initial : Fin K) (select) (stream) : action initial select stream 0 = initial
theorem
BanditRLProof.ArmStreamPolicy.action_succ
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.ArmStreamPolicy.action_succReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
@[simp] theorem action_succ (initial : Fin K) (select) (stream) (n : ℕ) : action initial select stream (n+1) = select n (history initial select stream n)
theorem
BanditRLProof.ArmStreamPolicy.history_eq_trace
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.ArmStreamPolicy.history_eq_traceReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem history_eq_trace (initial : Fin K) (select) (stream) (n : ℕ) : history initial select stream n = History.finitePairHistoryOfTrace (action initial select stream) (reward initial select stream) n
theorem
BanditRLProof.ArmStreamPolicy.measurable_history
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.ArmStreamPolicy.measurable_historyReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem measurable_history (initial : Fin K) (select) (hm : ∀ n, Measurable (select n)) (n : ℕ) : Measurable (fun stream => history initial select stream n)
theorem
BanditRLProof.ArmStreamPolicy.measurable_action
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.ArmStreamPolicy.measurable_actionReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem measurable_action (initial : Fin K) (select) (hm : ∀ n, Measurable (select n)) (t : ℕ) : Measurable (fun stream => action initial select stream t)
theorem
BanditRLProof.ArmStreamPolicy.history_ucb
Compiled
Compatibility is equality of the actual recursively generated histories.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.ArmStreamPolicy.history_ucbReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem history_ucb (hK : 0 < K) (c : ℝ) (stream) (n : ℕ) : history (UCB.initializationArm hK 0) (UCB.realHistoryNextArm hK c) stream n = UCB.armStreamHistory hK c stream n