Lean module · Foundations
BanditRLProof.ExpectationRegretPullCount
# Bochner expected-regret pull-count decomposition This module lifts the deterministic `REGRET-PULLCOUNT` equality to a Real-valued Bochner expectation statement. It stays at the bookkeeping layer: the only probabilistic regularity assumption is integrability of each finite horizon pull-count random variable after casting to `Real`.
Module map
Imports
BanditRLProof.ExpectationBochnerSums, BanditRLProof.MeasurablePullCountCast, BanditRLProof.RegretDecomposition
Imported by
BanditRLProof, BanditRLProof.Algorithms.UCBConditionalRewardLawCenteredKernelReal
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.real_pseudoRegret_eq_univ_sum_gap_mul_natCast_pullCount
Compiled Internal helper
No declaration docstring is present; use the chapter context and exact statement below.
private theorem real_pseudoRegret_eq_univ_sum_gap_mul_natCast_pullCount {K : Nat} (model : FiniteBanditModel K) (action : ActionTrace (Fin K)) (n : Nat) : ((pseudoRegret model action n : Rat) : Real) = (Finset.univ : Finset (Fin K)).sum (fun a : Fin K => ((model.gap a : Rat) : Real) * ((pullCount action a n : Nat) : Real))
theorem
BanditRLProof.integrable_real_pullCount_of_measurable_action
Compiled
The Real cast of a finite-horizon pull count is integrable under any finite measure when the action trace is measurable one time coordinate at a time. This is the generic regularity adapter behind Real expected-regret wrappers: measurability comes from `measurable_natCast_pullCount`, while `pullCount_le_time` supplies the deterministic integrable bound.
theorem integrable_real_pullCount_of_measurable_action {Omega : Type u} {Action : Type*} [MeasurableSpace Omega] [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (mu : Measure Omega) [MeasureTheory.IsFiniteMeasure mu] (action : Omega -> ActionTrace Action) (haction : forall t : Nat, Measurable (fun omega : Omega => action omega t)) (arm : Action) (n : Nat) : Integrable (fun omega : Omega => ((pullCount (action omega) arm n : Nat) : Real)) mu
theorem
BanditRLProof.integrable_real_pseudoRegret_of_integrable_pullCount
Compiled
If every finite-horizon pull count is integrable after casting to `Real`, then the corresponding Real-valued pseudo-regret is integrable. This is the regularity adapter used by the Bochner expected-regret decomposition. It does not prove measurability or integrability from a policy model; callers provide the pull-count integrability witnesses.
theorem integrable_real_pseudoRegret_of_integrable_pullCount {Omega : Type u} {K : Nat} [MeasurableSpace Omega] (mu : Measure Omega) (model : FiniteBanditModel K) (action : Omega -> ActionTrace (Fin K)) (n : Nat) (hcount : forall a : Fin K, Integrable (fun omega : Omega => ((pullCount (action omega) a n : Nat) : Real)) mu) : Integrable (fun omega : Omega => ((pseudoRegret model (action omega) n : Rat) : Real)) mu
theorem
BanditRLProof.integral_real_pseudoRegret_eq_sum_gap_mul_integral_pullCount
Compiled
The Real-valued Bochner expectation of pseudo-regret is the finite sum of each arm gap multiplied by the Bochner expectation of that arm's pull count. This is the local `EXP-REGRET-PULLCOUNT` leaf. It consumes the deterministic `REGRET-PULLCOUNT` bridge and the Mathlib-backed `EXP-FINITE-SUM` wrapper.
theorem integral_real_pseudoRegret_eq_sum_gap_mul_integral_pullCount {Omega : Type u} {K : Nat} [MeasurableSpace Omega] (mu : Measure Omega) (model : FiniteBanditModel K) (action : Omega -> ActionTrace (Fin K)) (n : Nat) (hcount : forall a : Fin K, Integrable (fun omega : Omega => ((pullCount (action omega) a n : Nat) : Real)) mu) : MeasureTheory.integral mu (fun omega : Omega => ((pseudoRegret model (action omega) n : Rat) : Real)) = (Finset.univ : Finset (Fin K)).sum (fun a : Fin K => ((model.gap a : Rat) : Real) * MeasureTheory.integral mu (fun omega : Omega => ((pullCount (action omega) a n : Nat) : Real)))