Lean module · Probability layer
BanditRLProof.MeasurablePullCount
# Measurability of local pull counts This module proves that the recursive pull-count process is measurable when the action trace is timewise measurable. It stays before expectation and before scalar-cast pull-count identities.
Module map
Imports
BanditRLProof.MeasureFoundation, BanditRLProof.LeafLemmas
Imported by
BanditRLProof, BanditRLProof.Algorithms.UCB, BanditRLProof.MeasurablePullCountCast
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.measurable_pullCount
Compiled
The local recursive pull count is measurable at each finite horizon. This is the `MEAS-PULLCOUNT` bridge. It prepares expected pull-count leaves without introducing measures, integration, filtration, or concentration.
theorem measurable_pullCount {Omega : Type u} {Action : Type v} [MeasurableSpace Omega] [MeasurableSpace Action] [MeasurableSingletonClass Action] [MeasurableSpace Nat] [MeasurableAdd₂ Nat] [DecidableEq Action] (action : Omega -> ActionTrace Action) (haction : forall t : Nat, Measurable (fun omega : Omega => action omega t)) (a : Action) (n : Nat) : Measurable (fun omega : Omega => pullCount (action omega) a n)