Lean module · Foundations
BanditRLProof.ScalarPseudoRegret
# Scalar pseudo-regret `ENNReal.ofReal` bridges This module is still pointwise scalar algebra. It connects the deterministic pull-count regret decomposition to the scalar `ENNReal.ofReal` finite-sum faithfulness lemma under an explicit nonnegativity contract on model gaps.
Module map
Imports
BanditRLProof.ScalarENNReal, BanditRLProof.RegretDecomposition
Imported by
BanditRLProof, BanditRLProof.Algorithms.UCBConditionalRewardLawRegret, BanditRLProof.ExpectationPseudoRegretOfRealBounds
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_model_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_model_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.ENNReal.ofReal_pseudoRegret_eq_univ_sum_model_gap_ofReal_mul_natCast_pullCount_of_nonneg
Compiled
Pointwise pseudo-regret is faithfully represented by the `ENNReal.ofReal` weighted pull-count expression when all model gaps are explicitly nonnegative after casting from `Rat` to `Real`. This is the `OFREAL-PSEUDOREGRET-PULLCOUNT-FAITHFULNESS` scalar/model bridge. It is not an expectation theorem and does not introduce measures, filtrations, kernels, or concentration assumptions.
theorem ofReal_pseudoRegret_eq_univ_sum_model_gap_ofReal_mul_natCast_pullCount_of_nonneg {K : Nat} (model : FiniteBanditModel K) (action : ActionTrace (Fin K)) (hgap : forall a : Fin K, 0 <= (((model.gap a : Rat) : Real))) (n : Nat) : ENNReal.ofReal (((pseudoRegret model action n : Rat) : Real)) = (Finset.univ : Finset (Fin K)).sum (fun a : Fin K => ENNReal.ofReal (((model.gap a : Rat) : Real)) * ((pullCount action a n : Nat) : ENNReal))