Lean module · Probability layer
BanditRLProof.MeasureFoundation
# Minimal measurable action-event foundations 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.
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.
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.
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))