Lean module · ETC
BanditRLProof.Algorithms.ETCCountLemmas
# Deterministic ETC count lemmas This module records small Explore-Then-Commit count facts over the existing round-robin exploration primitive. It deliberately stays below full ETC traces, commit behavior, probability, concentration, and regret bounds.
Module map
Imports
BanditRLProof.MathlibWrappers, BanditRLProof.Algorithms.ETC
Imported by
BanditRLProof, BanditRLProof.Algorithms.ETCTraceCountLemmas, BanditRLProof.Algorithms.UCBArmStreamExpectedPullCount, BanditRLProof.Algorithms.UCBConditionalRewardLawPolicy
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.ETC.pullCount_exploreArm_K_eq_one
Compiled
During the first full round-robin exploration cycle, every arm is pulled exactly once. This is the `ETC-ROUND-ROBIN-FIRST-CYCLE-COUNT` project-local deterministic count scaffold.
theorem ETC.pullCount_exploreArm_K_eq_one {K : Nat} (spec : ETC.Spec K) (a : Fin K) : pullCount (ETC.exploreArm spec) a K = 1
theorem
BanditRLProof.ETC.pullCount_exploreArm_add_K_eq_add_one
Compiled
Extending a round-robin ETC exploration prefix by one full cycle adds exactly one pull of every arm. This is the `ETC-ROUND-ROBIN-ADD-K-COUNT` project-local deterministic count scaffold.
theorem ETC.pullCount_exploreArm_add_K_eq_add_one {K : Nat} (spec : ETC.Spec K) (a : Fin K) (t : Nat) : pullCount (ETC.exploreArm spec) a (t + K) = pullCount (ETC.exploreArm spec) a t + 1
theorem
BanditRLProof.ETC.pullCount_exploreArm_mul_K_eq
Compiled
Across `m` full round-robin ETC exploration cycles, every arm is pulled exactly `m` times. This is the `ETC-ROUND-ROBIN-MUL-K-COUNT` project-local deterministic count scaffold.
theorem ETC.pullCount_exploreArm_mul_K_eq {K : Nat} (spec : ETC.Spec K) (a : Fin K) (m : Nat) : pullCount (ETC.exploreArm spec) a (m * K) = m
theorem
BanditRLProof.ETC.pullCount_exploreArm_explorationPulls_mul_K_eq
Compiled
At the configured ETC exploration horizon, every arm has been pulled exactly `spec.explorationPulls` times. This is the `ETC-ROUND-ROBIN-EXPLORATION-PULLS-COUNT` project-local deterministic count adapter.
theorem ETC.pullCount_exploreArm_explorationPulls_mul_K_eq {K : Nat} (spec : ETC.Spec K) (a : Fin K) : pullCount (ETC.exploreArm spec) a (spec.explorationPulls * K) = spec.explorationPulls