Lean module · Probability layer
BanditRLProof.MeasurablePullCount
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.StochasticGradientBanditTheoremTwoNthPull, 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.
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_pullCountReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
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)