Lean module · ETC

BanditRLProof.Algorithms.ETCTrace

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

Source: BanditRLProof/Algorithms/ETCTrace.lean
Teaching chapter: 3. Explore-Then-Commit
Declarations: 4
Placeholders: 0

Imports

BanditRLProof.Core, BanditRLProof.Algorithms.ETC

Imported by

BanditRLProof, BanditRLProof.Algorithms.ETCTraceCountLemmas

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`.

Used in these reading views: Bandit Book

3. Explore-Then-Commit

Canonical node identity

declaration:BanditRLProof.ETC.actionWithCommit

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

def actionWithCommit {K : Nat} (spec : ETC.Spec K) (commitArm : Fin K) : ActionTrace (Fin K)

Source line 17 Chapter context: ETC

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.

Used in these reading views: Bandit Book

3. Explore-Then-Commit

Canonical node identity

declaration:BanditRLProof.ETC.actionWithCommit_eq_exploreArm_of_lt

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

@[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

Source line 32 Chapter context: ETC

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.

Used in these reading views: Bandit Book

3. Explore-Then-Commit

Canonical node identity

declaration:BanditRLProof.ETC.actionWithCommit_eq_commitArm_of_ge

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

@[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

Source line 45 Chapter context: ETC

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.

Used in these reading views: Bandit Book

3. Explore-Then-Commit

Canonical node identity

declaration:BanditRLProof.ETC.actionWithCommit_eq_bestArm_of_commitArm_eq_bestArm_of_explorationPulls_mul_K_le

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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

Source line 59 Chapter context: ETC