Lean module · ETC
BanditRLProof.Algorithms.ETCWrongCommitRegretAssembly
# ETC wrong-commit regret assembly This module gives a pointwise bridge from the deterministic fixed-commit ETC regret scaffolds to a wrong-commit-shaped suffix penalty. It deliberately stays below integration, probability bounds, concentration, filtrations, and a final ETC expected-regret theorem.
Module map
Imports
BanditRLProof.Algorithms.ETCRegretLemmas
Imported by
BanditRLProof, BanditRLProof.Algorithms.ETCExpectedRegretAssembly
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.ETC.pseudoRegret_actionWithCommit_choice_le_sum_gap_mul_explorationPulls_add_suffix_badGap
Compiled
For an `Omega`-indexed commit selector, fixed-commit ETC regret after a suffix is bounded by the exploration budget plus a suffix penalty that vanishes when the selected commit arm is the model's `bestArm`. The explicit `badGapBound` is the local bridge to a later probability layer: the suffix cost is charged only on the wrong-commit branch.
theorem pseudoRegret_actionWithCommit_choice_le_sum_gap_mul_explorationPulls_add_suffix_badGap {Omega : Type u} {K : Nat} (spec : ETC.Spec K) (model : FiniteBanditModel K) (commit : Omega -> Fin K) (r : Nat) (badGapBound : Rat) (hbadGap : forall a : Fin K, (a = model.bestArm -> False) -> model.gap a <= badGapBound) (omega : Omega) : pseudoRegret model (ETC.actionWithCommit spec (commit omega)) (spec.explorationPulls * K + r) <= ((Finset.univ : Finset (Fin K)).sum (fun a : Fin K => model.gap a)) * (((spec.explorationPulls : Nat) : Rat)) + (((r : Nat) : Rat) * (if commit omega = model.bestArm then 0 else badGapBound))