Lean module · Probability layer
BanditRLProof.MeasureFoundation
This module starts the probability-facing layer with measurable events only. It deliberately avoids measure, integration, probability, filtration, and concentration imports.
Module map
Imports
Imported by
BanditRLProof, BanditRLProof.ExpectationFoundation, BanditRLProof.HistoryFiltration, BanditRLProof.MeasurablePullCount, BanditRLProof.MeasurableSums
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.measurableSet_actionTrace_eval_eq
Compiled
If every time-indexed action random variable is measurable, then the event that the action at a fixed time equals a fixed arm is measurable. This is the `MEAS-FIN-ACTION` canary. The statement is more general than finite actions: it only needs singleton measurability of the action space.
Used in these reading views: Bandit Book · Reinforcement Learning Book · Online Learning Book
2. Probability, kernels, filtrations, and concentration
Canonical node identity
declaration:BanditRLProof.measurableSet_actionTrace_eval_eqReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem measurableSet_actionTrace_eval_eq {Omega : Type u} {Action : Type v} [MeasurableSpace Omega] [MeasurableSpace Action] [MeasurableSingletonClass Action] (action : Omega -> ActionTrace Action) (hmeas : forall t : Nat, Measurable (fun omega : Omega => action omega t)) (a : Action) (t : Nat) : MeasurableSet {omega : Omega | action omega t = a}
theorem
BanditRLProof.measurable_actionTrace_eval_eq_indicator_const
Compiled
The indicator of a measurable action-equality event with a constant value is measurable. This is the `MEAS-PULL-INDICATOR` bridge. It remains scalar-agnostic so later expectation work can choose the codomain deliberately.
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_actionTrace_eval_eq_indicator_constReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem measurable_actionTrace_eval_eq_indicator_const {Omega : Type u} {Action : Type v} {Beta : Type w} [MeasurableSpace Omega] [MeasurableSpace Action] [MeasurableSingletonClass Action] [MeasurableSpace Beta] [Zero Beta] (action : Omega -> ActionTrace Action) (hmeas : forall t : Nat, Measurable (fun omega : Omega => action omega t)) (a : Action) (t : Nat) (c : Beta) : Measurable (({omega : Omega | action omega t = a} : Set Omega).indicator (fun _ : Omega => c))
theorem
BanditRLProof.measurable_actionTrace_eval_eq_indicator_reward
Compiled
The selected-reward contribution for a fixed action event is measurable when the action and reward traces are timewise measurable. This is the `MEAS-REWARD` bridge. It deliberately stays at the measurability layer and does not choose an expectation or scalar algebra route.
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_actionTrace_eval_eq_indicator_rewardReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem measurable_actionTrace_eval_eq_indicator_reward {Omega : Type u} {Action : Type v} {Reward : Type w} [MeasurableSpace Omega] [MeasurableSpace Action] [MeasurableSingletonClass Action] [MeasurableSpace Reward] [Zero 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) (t : Nat) : Measurable (({omega : Omega | action omega t = a} : Set Omega).indicator (fun omega : Omega => reward omega t))