Lean module · Probability layer
BanditRLProof.MeasurableSums
This module keeps the probability-facing layer before integration. It only proves measurability of finite sums built from the selected-reward indicator bridge in MeasureFoundation.
Module map
Imports
BanditRLProof.MeasureFoundation
Imported by
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.measurable_finset_sum_indicator_reward
Compiled
Finite sums of selected-reward indicator contributions are measurable. This is the `MEAS-SELECTED-REWARD-FINITE-SUM` bridge. The statement is over an arbitrary finite set of times so later range, window, or stopped-prefix corollaries can instantiate the same local API.
Used in these reading views: Bandit Book · Reinforcement Learning Book · Online Learning Book
2. Probability, kernels, filtrations, and concentration
Canonical node identity
declaration:BanditRLProof.measurable_finset_sum_indicator_rewardReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem measurable_finset_sum_indicator_reward {Omega : Type u} {Action : Type v} {Reward : Type w} [MeasurableSpace Omega] [MeasurableSpace Action] [MeasurableSingletonClass Action] [MeasurableSpace Reward] [AddCommMonoid Reward] [MeasurableAdd₂ Reward] (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) (s : Finset Nat) : Measurable (fun omega : Omega => s.sum (fun t : Nat => (({omega' : Omega | action omega' t = a} : Set Omega).indicator (fun omega' : Omega => reward omega' t)) omega))