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.
Used in these reading views: Bandit Book
Canonical node identity
declaration:BanditRLProof.ETC.SpecReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
structure Spec (K : Nat) where
def
BanditRLProof.ETC.exploreArm
Compiled
Round-robin exploration arm at time `t`.
Used in these reading views: Bandit Book
Canonical node identity
declaration:BanditRLProof.ETC.exploreArmReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
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.
Used in these reading views: Bandit Book
Canonical node identity
declaration:BanditRLProof.ETC.exploreArm_valReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
@[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.
Used in these reading views: Bandit Book
Canonical node identity
declaration:BanditRLProof.ETC.exploreArm_eq_of_mod_eqReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
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.
Used in these reading views: Bandit Book
Canonical node identity
declaration:BanditRLProof.ETC.exploreArm_eq_iff_mod_eq_valReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
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.
Used in these reading views: Bandit Book
Canonical node identity
declaration:BanditRLProof.ETC.exploreArm_add_KReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
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.
Used in these reading views: Bandit Book
Canonical node identity
declaration:BanditRLProof.ETC.CommitOracleReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
structure CommitOracle (K : Nat) where
def
BanditRLProof.ETC.obligationNames
Compiled
The proof-DAG leaves usually needed for ETC regret formalization.
Used in these reading views: Bandit Book
Canonical node identity
declaration:BanditRLProof.ETC.obligationNamesReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
def obligationNames : List String