Lean module · Foundations
BanditRLProof.ExpectationPseudoRegretOfRealBounds
# Lower-integral bounds for `ENNReal.ofReal` pseudo-regret 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.
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))