Lean module · Probability layer
BanditRLProof.MeasurableRegret
# Measurability of local pseudo-regret 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.
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)