Lean module · Probability layer
BanditRLProof.MeasurableLocalQuantities
# Measurability of local bandit quantities This module connects generic measurable finite-sum bridges back to the local recursive quantities used by the bandit vocabulary.
Module map
Imports
BanditRLProof.MeasurableSums, BanditRLProof.MathlibWrappers
Imported by
BanditRLProof, BanditRLProof.Algorithms.ETCEmpiricalMeanMeasurability, BanditRLProof.Algorithms.ETCRealEmpiricalMean, BanditRLProof.Algorithms.UCBRealHistoryIndex, BanditRLProof.FiniteRealArgmax
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.sumRewards_eq_finset_range_indicator_reward
Compiled Internal helper
No declaration docstring is present; use the chapter context and exact statement below.
private theorem sumRewards_eq_finset_range_indicator_reward {Omega : Type u} {Action : Type v} {Reward : Type v} [DecidableEq Action] [AddCommMonoid Reward] (action : Omega -> ActionTrace Action) (reward : Omega -> RewardTrace Reward) (a : Action) (n : Nat) (omega : Omega) : sumRewards (action omega) (reward omega) a n = (Finset.range n).sum (fun t : Nat => (({omega' : Omega | action omega' t = a} : Set Omega).indicator (fun omega' : Omega => reward omega' t)) omega)
theorem
BanditRLProof.measurable_sumRewards
Compiled
The local recursive selected-reward accumulator is measurable when action and reward traces are timewise measurable. This is the `MEAS-SUMREWARDS` bridge. It is still only a measurability result: no expectation, probability measure, filtration, or concentration structure is introduced here.
theorem measurable_sumRewards {Omega : Type u} {Action : Type v} {Reward : Type v} [MeasurableSpace Omega] [MeasurableSpace Action] [MeasurableSingletonClass Action] [MeasurableSpace Reward] [AddCommMonoid Reward] [MeasurableAdd₂ Reward] [DecidableEq Action] (action : Omega -> ActionTrace Action) (reward : Omega -> RewardTrace Reward) (haction : forall t : Nat, Measurable (fun omega : Omega => action omega t)) (hreward : forall t : Nat, Measurable (fun omega : Omega => reward omega t)) (a : Action) (n : Nat) : Measurable (fun omega : Omega => sumRewards (action omega) (reward omega) a n)