BanditRLProof.Algorithms.ETCRegretLemmas

The pseudo-regret of the pure round-robin ETC exploration prefix is bounded by the sum of arm gaps times the configured number of exploration pulls per arm. This is the `ETC-EXPLORATION-REGRET-BOUND` project-local deterministic regret scaffold.

theorem ETC.pseudoRegret_exploreArm_explorationPulls_mul_K_le_sum_gap_mul_explorationPulls {K : Nat} (spec : ETC.Spec K) (model : FiniteBanditModel K) : pseudoRegret model (ETC.exploreArm spec) (spec.explorationPulls * K) <= ((Finset.univ : Finset (Fin K)).sum (fun a : Fin K => model.gap a)) * (((spec.explorationPulls : Nat) : Rat))

The pseudo-regret of the fixed-commit ETC trace at the exploration horizon is bounded by the sum of arm gaps times the configured number of exploration pulls per arm. This is the `ETC-ACTION-WITH-COMMIT-EXPLORATION-HORIZON-REGRET-BOUND` project-local deterministic regret scaffold.

theorem ETC.pseudoRegret_actionWithCommit_explorationPulls_mul_K_le_sum_gap_mul_explorationPulls {K : Nat} (spec : ETC.Spec K) (model : FiniteBanditModel K) (commitArm : Fin K) : pseudoRegret model (ETC.actionWithCommit spec commitArm) (spec.explorationPulls * K) <= ((Finset.univ : Finset (Fin K)).sum (fun a : Fin K => model.gap a)) * (((spec.explorationPulls : Nat) : Rat))

The fixed-commit ETC trace at an exploration horizon plus suffix `r` is bounded by the gap-weighted count budget that allocates `explorationPulls` to every arm and the suffix budget only to the committed arm. This is the `ETC-ACTION-WITH-COMMIT-SUFFIX-COUNT-BUDGET-REGRET` project-local deterministic regret scaffold. It deliberately keeps the right-hand side in the unsimplified per-arm budget form.

theorem ETC.pseudoRegret_actionWithCommit_explorationPulls_mul_K_add_le_sum_gap_mul_suffix_count_budget {K : Nat} (spec : ETC.Spec K) (model : FiniteBanditModel K) (commitArm : Fin K) (r : Nat) : pseudoRegret model (ETC.actionWithCommit spec commitArm) (spec.explorationPulls * K + r) <= (Finset.univ : Finset (Fin K)).sum (fun a : Fin K => model.gap a * (((spec.explorationPulls + (if commitArm = a then r else 0) : Nat) : Rat)))

The fixed-commit ETC trace after an exploration horizon plus suffix `r` also satisfies the coarser uniform count-budget regret bound where every arm is allowed `explorationPulls + r` pulls. This is the `ETC-ACTION-WITH-COMMIT-COARSE-SUFFIX-REGRET-BOUND` project-local deterministic regret scaffold.

theorem ETC.pseudoRegret_actionWithCommit_explorationPulls_mul_K_add_le_sum_gap_mul_explorationPulls_add_suffix {K : Nat} (spec : ETC.Spec K) (model : FiniteBanditModel K) (commitArm : Fin K) (r : Nat) : pseudoRegret model (ETC.actionWithCommit spec commitArm) (spec.explorationPulls * K + r) <= ((Finset.univ : Finset (Fin K)).sum (fun a : Fin K => model.gap a)) * ((((spec.explorationPulls + r : Nat) : Rat)))

The fixed-commit ETC trace splits pseudo-regret after the exploration horizon into the exploration-horizon pseudo-regret plus one committed-arm gap for each suffix pull. This is the `ETC-ACTION-WITH-COMMIT-PHASE-SPLIT-REGRET` project-local deterministic regret scaffold.

theorem ETC.pseudoRegret_actionWithCommit_explorationPulls_mul_K_add_eq_add_suffix_gap {K : Nat} (spec : ETC.Spec K) (model : FiniteBanditModel K) (commitArm : Fin K) (r : Nat) : pseudoRegret model (ETC.actionWithCommit spec commitArm) (spec.explorationPulls * K + r) = pseudoRegret model (ETC.actionWithCommit spec commitArm) (spec.explorationPulls * K) + (((r : Nat) : Rat) * model.gap commitArm)

If the fixed commit arm is the model's selected best arm, extending the ETC trace past the exploration horizon adds no pseudo-regret. This is the `ETC-ACTION-WITH-COMMIT-BESTARM-SUFFIX-NO-REGRET` project-local deterministic regret scaffold.

theorem ETC.pseudoRegret_actionWithCommit_explorationPulls_mul_K_add_eq_of_commitArm_eq_bestArm {K : Nat} (spec : ETC.Spec K) (model : FiniteBanditModel K) (commitArm : Fin K) (r : Nat) (hcommit : commitArm = model.bestArm) : pseudoRegret model (ETC.actionWithCommit spec commitArm) (spec.explorationPulls * K + r) = pseudoRegret model (ETC.actionWithCommit spec commitArm) (spec.explorationPulls * K)

If the fixed commit arm is the model's selected best arm, the ETC regret after any post-exploration suffix is bounded by the exploration-horizon regret budget. This is the `ETC-ACTION-WITH-COMMIT-BESTARM-SUFFIX-REGRET-BOUND` project-local deterministic regret scaffold.

theorem ETC.pseudoRegret_actionWithCommit_explorationPulls_mul_K_add_le_sum_gap_mul_explorationPulls_of_commitArm_eq_bestArm {K : Nat} (spec : ETC.Spec K) (model : FiniteBanditModel K) (commitArm : Fin K) (r : Nat) (hcommit : commitArm = model.bestArm) : pseudoRegret model (ETC.actionWithCommit spec commitArm) (spec.explorationPulls * K + r) <= ((Finset.univ : Finset (Fin K)).sum (fun a : Fin K => model.gap a)) * (((spec.explorationPulls : Nat) : Rat))

The phase-split equality and the exploration-horizon regret bound combine into a deterministic fixed-commit ETC regret bound with an explicit committed-arm suffix term. This is the `ETC-ACTION-WITH-COMMIT-PHASE-SPLIT-REGRET-BOUND` project-local deterministic regret scaffold.

theorem ETC.pseudoRegret_actionWithCommit_explorationPulls_mul_K_add_le_sum_gap_mul_explorationPulls_add_suffix_gap {K : Nat} (spec : ETC.Spec K) (model : FiniteBanditModel K) (commitArm : Fin K) (r : Nat) : pseudoRegret model (ETC.actionWithCommit spec commitArm) (spec.explorationPulls * K + r) <= ((Finset.univ : Finset (Fin K)).sum (fun a : Fin K => model.gap a)) * (((spec.explorationPulls : Nat) : Rat)) + (((r : Nat) : Rat) * model.gap commitArm)