Lean module · Probability layer
BanditRLProof.MeasurableRegret
This module keeps regret measurability before expectation. It only proves that the local deterministic pseudo-regret quantity becomes a measurable random variable when the action trace is timewise measurable.
Module map
Imports
Imported by
BanditRLProof, BanditRLProof.Algorithms.ETCFiniteArmRewardLaw
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.measurable_pseudoRegret
Compiled
The local pseudo-regret process is measurable as a random variable at each finite horizon. This is the narrow `MEAS-REGRET` bridge. It does not introduce probability measures, expectations, filtrations, or concentration assumptions.
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_pseudoRegretReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem measurable_pseudoRegret {Omega : Type u} [MeasurableSpace Omega] [MeasurableSpace (Fin K)] [MeasurableSingletonClass (Fin K)] [MeasurableSpace Rat] [MeasurableAdd₂ Rat] (model : FiniteBanditModel K) (action : Omega -> ActionTrace (Fin K)) (haction : forall t : Nat, Measurable (fun omega : Omega => action omega t)) (n : Nat) : Measurable (fun omega : Omega => pseudoRegret model (action omega) n)