Lean module · Foundations
BanditRLProof.ExpectationPseudoRegretOfRealBounds
This module lifts the pointwise scalar/model pseudo-regret faithfulness bridge to the existing ENNReal lower-integral model-gap budget bound. It remains an ENNReal.ofReal lower-integral theorem, not a Rat-valued or Bochner expected regret statement.
Module map
Imports
BanditRLProof.ExpectationFiniteBanditModelBounds, BanditRLProof.ScalarPseudoRegret
Imported by
BanditRLProof, BanditRLProof.ExpectationPseudoRegretRatBounds
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.lintegral_ofReal_pseudoRegret_le_sum_model_gap_ofReal_mul_time_of_nonneg
Compiled
Under explicit nonnegativity of model gaps, the lower integral of `ENNReal.ofReal` pseudo-regret is bounded by the finite-arm model-gap horizon budget. This is the `EXP-OFREAL-PSEUDOREGRET-BOUND` leaf. It consumes the pointwise scalar/model pseudo-regret bridge and the existing finite-bandit model-gap lower-integral bound; it does not prove gap nonnegativity, Bochner expectation, filtration, or concentration results.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.lintegral_ofReal_pseudoRegret_le_sum_model_gap_ofReal_mul_time_of_nonnegReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem lintegral_ofReal_pseudoRegret_le_sum_model_gap_ofReal_mul_time_of_nonneg {Omega : Type u} {K : Nat} [MeasurableSpace Omega] [MeasurableSpace (Fin K)] [MeasurableSingletonClass (Fin K)] (mu : Measure Omega) [MeasureTheory.IsProbabilityMeasure mu] (model : FiniteBanditModel K) (action : Omega -> ActionTrace (Fin K)) (haction : forall t : Nat, Measurable (fun omega : Omega => action omega t)) (hgap : forall a : Fin K, 0 <= (((model.gap a : Rat) : Real))) (n : Nat) : MeasureTheory.lintegral mu (fun omega : Omega => ENNReal.ofReal (((pseudoRegret model (action omega) n : Rat) : Real))) <= (Finset.univ : Finset (Fin K)).sum (fun a : Fin K => ENNReal.ofReal (((model.gap a : Rat) : Real)) * (n : ENNReal))