Lean module · Foundations
BanditRLProof.Algorithms.MOSSRewardBranch
Generated source map for this Lean module.
Module map
Imports
BanditRLProof.Algorithms.MOSSUnusedCoordinate
Imported by
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
def
BanditRLProof.MOSS.conditionCoordinate
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.conditionCoordinateReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
def conditionCoordinate {k : ℕ} (t : ℕ) (c : History.FinitePairHistory (Fin k) ℝ t × Fin k) : ℕ × Fin k
def
BanditRLProof.MOSS.conditionBranch
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.conditionBranchReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
def conditionBranch {k : ℕ} (t : ℕ) (target : ℕ × Fin k)
theorem
BanditRLProof.MOSS.measurable_conditionCoordinate
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_conditionCoordinateReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem measurable_conditionCoordinate {k : ℕ} (t : ℕ) : Measurable (conditionCoordinate (k := k) t)
theorem
BanditRLProof.MOSS.measurableSet_conditionBranch
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.measurableSet_conditionBranchReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem measurableSet_conditionBranch {k : ℕ} (t : ℕ) (target : ℕ × Fin k) : MeasurableSet (conditionBranch t target)
theorem
BanditRLProof.MOSS.measurable_canonicalNextCoordinate
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_canonicalNextCoordinateReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem measurable_canonicalNextCoordinate {k : ℕ} (hk : 0 < k) (n : ℕ) (mean : Fin k → ℝ) (t : ℕ) : Measurable (canonicalNextCoordinate hk n mean t)
theorem
BanditRLProof.MOSS.canonicalReward_succ_eq_coordinate
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.canonicalReward_succ_eq_coordinateReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem canonicalReward_succ_eq_coordinate {k : ℕ} (hk : 0 < k) (n : ℕ) (mean : Fin k → ℝ) (t : ℕ) (table : UCB.ArmRewardStream k) : canonicalReward hk n mean table (t+1) = UCB.armStreamCoordinate (canonicalNextCoordinate hk n mean t table) table
theorem
BanditRLProof.MOSS.rebuilt_mem_conditionBranch_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 identity
declaration:BanditRLProof.MOSS.rebuilt_mem_conditionBranch_iffReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem rebuilt_mem_conditionBranch_iff {k : ℕ} (hk : 0 < k) (n : ℕ) (mean : Fin k → ℝ) (t : ℕ) (target : ℕ × Fin k) (v : ℝ) (table : UCB.ArmRewardStream k) : canonicalConditionWithout hk n mean t target v (UCB.armStreamWithoutCoordinate target table) ∈ conditionBranch t target ↔ canonicalNextCoordinate hk n mean t table = target
theorem
BanditRLProof.MOSS.map_rebuilt_restrict_conditionBranch
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.map_rebuilt_restrict_conditionBranchReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem map_rebuilt_restrict_conditionBranch {k : ℕ} (hk : 0 < k) (n : ℕ) (mean : Fin k → ℝ) (t : ℕ) (target : ℕ × Fin k) (v : ℝ) (μ : Measure (UCB.ArmRewardStream k)) : (Measure.map (fun table => canonicalConditionWithout hk n mean t target v (UCB.armStreamWithoutCoordinate target table)) μ).restrict (conditionBranch t target) = (Measure.map (canonicalCondition hk n mean t) μ).restrict (conditionBranch t target)
theorem
BanditRLProof.MOSS.map_condition_reward_restrict_branch
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.map_condition_reward_restrict_branchReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem map_condition_reward_restrict_branch {k : ℕ} (hk : 0 < k) (n : ℕ) (mean : Fin k → ℝ) (t : ℕ) (ν : Kernel (Fin k) ℝ) [IsMarkovKernel ν] (target : ℕ × Fin k) (v : ℝ) : Measure.map (fun table => (canonicalCondition hk n mean t table, canonicalReward hk n mean table (t+1))) ((UCB.armStreamMeasure ν).restrict {table | canonicalNextCoordinate hk n mean t table = target}) = ((Measure.map (canonicalCondition hk n mean t) (UCB.armStreamMeasure ν)).restrict (conditionBranch t target)).prod (ν target.2)