Lean module · ETC
BanditRLProof.Algorithms.ETCTrace
# ETC phase-switching traces This module introduces the first deterministic boundary for phase-switching Explore-Then-Commit traces. The commit arm is supplied explicitly; empirical mean selection, probability, concentration, and regret facts live in later leaves.
Module map
Imports
BanditRLProof.Core, BanditRLProof.Algorithms.ETC
Imported by
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
def
BanditRLProof.ETC.actionWithCommit
Compiled
Explore by round-robin until the configured horizon, then play `commitArm`.
def actionWithCommit {K : Nat} (spec : ETC.Spec K) (commitArm : Fin K) : ActionTrace (Fin K)
theorem
BanditRLProof.ETC.actionWithCommit_eq_exploreArm_of_lt
Compiled
During the configured exploration prefix, the phase-switching ETC trace agrees with the pure round-robin exploration trace. This is the `ETC-ACTION-WITH-COMMIT-EXPLORE-PHASE` project-local trace-boundary leaf.
@[simp] theorem actionWithCommit_eq_exploreArm_of_lt {K : Nat} (spec : ETC.Spec K) (commitArm : Fin K) {t : Nat} (h : t < spec.explorationPulls * K) : ETC.actionWithCommit spec commitArm t = ETC.exploreArm spec t
theorem
BanditRLProof.ETC.actionWithCommit_eq_commitArm_of_ge
Compiled
After the configured exploration prefix, the phase-switching ETC trace plays the supplied commit arm. This is the `ETC-ACTION-WITH-COMMIT-COMMIT-PHASE` project-local trace-boundary leaf.
@[simp] theorem actionWithCommit_eq_commitArm_of_ge {K : Nat} (spec : ETC.Spec K) (commitArm : Fin K) {t : Nat} (h : spec.explorationPulls * K <= t) : ETC.actionWithCommit spec commitArm t = commitArm
theorem
BanditRLProof.ETC.actionWithCommit_eq_bestArm_of_commitArm_eq_bestArm_of_explorationPulls_mul_K_le
Compiled
After the configured exploration prefix, if the supplied commit arm is the model's selected best arm, the phase-switching ETC trace plays that best arm. This is the `ETC-ACTION-WITH-COMMIT-BESTARM-COMMIT-PHASE` project-local trace-boundary leaf.
theorem actionWithCommit_eq_bestArm_of_commitArm_eq_bestArm_of_explorationPulls_mul_K_le {K : Nat} (spec : ETC.Spec K) (model : FiniteBanditModel K) (commitArm : Fin K) (t : Nat) (hcommit : commitArm = model.bestArm) (ht : spec.explorationPulls * K <= t) : ETC.actionWithCommit spec commitArm t = model.bestArm