Lean module · Probability layer

BanditRLProof.MeasurablePullCountCast

# Measurability of scalar-casted pull counts This module proves scalar-valued measurability of local pull counts. It stays before expectation, while matching the scalar form used by regret decompositions.

Module map

Source: BanditRLProof/MeasurablePullCountCast.lean
Teaching chapter: 2. Probability, kernels, filtrations, and concentration
Declarations: 1
Placeholders: 0

Imports

BanditRLProof.MeasurablePullCount

Imported by

BanditRLProof, BanditRLProof.Algorithms.ETCExpectedPullCount, BanditRLProof.Algorithms.UCBArmStreamExpectedPullCount, BanditRLProof.Algorithms.UCBRealHistoryIndex, BanditRLProof.ExpectationRegretPullCount, BanditRLProof.ExpectationWeightedPullCount

Declarations

Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.

theorem BanditRLProof.measurable_natCast_pullCount Compiled

The local recursive pull count, cast into an additive scalar, is measurable at each finite horizon. This is the `MEAS-PULLCOUNT-CAST` bridge. Later expectation leaves can instantiate `Beta := Rat` without changing the proof.

theorem measurable_natCast_pullCount {Omega : Type u} {Action : Type v} {Beta : Type w} [MeasurableSpace Omega] [MeasurableSpace Action] [MeasurableSingletonClass Action] [MeasurableSpace Beta] [AddCommMonoidWithOne Beta] [MeasurableAdd₂ Beta] [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 : Nat) : Beta))

Source line 23 Chapter context: Probability layer