Lean module · ETC
BanditRLProof.Algorithms.ETC
# Explore-Then-Commit surfaces
Module map
Imports
Imported by
BanditRLProof, BanditRLProof.Algorithms.ETCCountLemmas, BanditRLProof.Algorithms.ETCMeasurability, BanditRLProof.Algorithms.ETCTrace, BanditRLProof.Literature
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
structure
BanditRLProof.ETC.Spec
Compiled
Parameters for a finite-arm Explore-Then-Commit run.
structure Spec (K : Nat) where
def
BanditRLProof.ETC.exploreArm
Compiled
Round-robin exploration arm at time `t`.
def exploreArm (spec : Spec K) (t : Nat) : Fin K
theorem
BanditRLProof.ETC.exploreArm_val
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
@[simp] theorem exploreArm_val (spec : Spec K) (t : Nat) : (exploreArm spec t).val = t % K
theorem
BanditRLProof.ETC.exploreArm_eq_of_mod_eq
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem exploreArm_eq_of_mod_eq (spec : Spec K) {s t : Nat} (h : s % K = t % K) : exploreArm spec s = exploreArm spec t
theorem
BanditRLProof.ETC.exploreArm_eq_iff_mod_eq_val
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem exploreArm_eq_iff_mod_eq_val (spec : Spec K) (t : Nat) (a : Fin K) : exploreArm spec t = a ↔ t % K = a.val
theorem
BanditRLProof.ETC.exploreArm_add_K
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem exploreArm_add_K (spec : Spec K) (t : Nat) : exploreArm spec (t + K) = exploreArm spec t
structure
BanditRLProof.ETC.CommitOracle
Compiled
Commit-phase selector. A concrete theorem should replace this by argmax.
structure CommitOracle (K : Nat) where
def
BanditRLProof.ETC.obligationNames
Compiled
The proof-DAG leaves usually needed for ETC regret formalization.
def obligationNames : List String