Lean module · ETC
BanditRLProof.Algorithms.ETCTraceCountLemmas
# ETC phase-switching trace count lemmas This module contains deterministic pull-count facts for the fixed-commit ETC trace. It stays below regret, empirical commit selection, probability, and concentration.
Module map
Imports
BanditRLProof.LeafLemmas, BanditRLProof.Algorithms.ETCTrace, BanditRLProof.Algorithms.ETCCountLemmas
Imported by
BanditRLProof, BanditRLProof.Algorithms.ETCEmpiricalMean, BanditRLProof.Algorithms.ETCExpectedPullCount, BanditRLProof.Algorithms.ETCRegretLemmas
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.ETC.pullCount_actionWithCommit_eq_pullCount_exploreArm_of_le
Compiled
On any prefix contained inside the configured exploration horizon, the fixed-commit ETC trace has the same pull counts as the pure round-robin exploration trace. This is the `ETC-ACTION-WITH-COMMIT-EXPLORE-PREFIX-PULLCOUNT` project-local trace/count transfer leaf.
theorem ETC.pullCount_actionWithCommit_eq_pullCount_exploreArm_of_le {K : Nat} (spec : ETC.Spec K) (commitArm a : Fin K) (n : Nat) (hn : n <= spec.explorationPulls * K) : pullCount (ETC.actionWithCommit spec commitArm) a n = pullCount (ETC.exploreArm spec) a n
theorem
BanditRLProof.ETC.pullCount_actionWithCommit_explorationPulls_mul_K_eq
Compiled
At the configured exploration horizon, the fixed-commit ETC trace has pulled each arm exactly `spec.explorationPulls` times. This is the `ETC-ACTION-WITH-COMMIT-EXPLORATION-HORIZON-COUNT` project-local trace/count adapter.
theorem ETC.pullCount_actionWithCommit_explorationPulls_mul_K_eq {K : Nat} (spec : ETC.Spec K) (commitArm a : Fin K) : pullCount (ETC.actionWithCommit spec commitArm) a (spec.explorationPulls * K) = spec.explorationPulls
theorem
BanditRLProof.ETC.pullCount_actionWithCommit_explorationPulls_mul_K_pos
Compiled
At the configured exploration horizon, every arm in the fixed-commit ETC trace has a positive pull count whenever the configured number of exploration pulls is positive. This is the first denominator-positivity leaf for future empirical-mean construction. It stays purely deterministic and Nat-valued.
theorem ETC.pullCount_actionWithCommit_explorationPulls_mul_K_pos {K : Nat} (spec : ETC.Spec K) (commitArm a : Fin K) (hexplorationPulls_pos : 0 < spec.explorationPulls) : 0 < pullCount (ETC.actionWithCommit spec commitArm) a (spec.explorationPulls * K)
theorem
BanditRLProof.ETC.ratCast_pullCount_actionWithCommit_explorationPulls_mul_K_pos
Compiled
Rat-cast form of the fixed-commit ETC exploration pull-count positivity leaf. This is the first denominator adapter for future Rat-valued empirical means. It only transports the compiled Nat positivity theorem across the Nat-to-Rat cast.
theorem ETC.ratCast_pullCount_actionWithCommit_explorationPulls_mul_K_pos {K : Nat} (spec : ETC.Spec K) (commitArm a : Fin K) (hexplorationPulls_pos : 0 < spec.explorationPulls) : (0 : Rat) < (pullCount (ETC.actionWithCommit spec commitArm) a (spec.explorationPulls * K) : Rat)
theorem
BanditRLProof.ETC.ratCast_pullCount_actionWithCommit_explorationPulls_mul_K_ne_zero
Compiled
Nonzero Rat-denominator form of the fixed-commit ETC exploration pull-count positivity leaf. This is still only a deterministic denominator adapter. It does not define empirical means or introduce probability assumptions.
theorem ETC.ratCast_pullCount_actionWithCommit_explorationPulls_mul_K_ne_zero {K : Nat} (spec : ETC.Spec K) (commitArm a : Fin K) (hexplorationPulls_pos : 0 < spec.explorationPulls) : Not ((pullCount (ETC.actionWithCommit spec commitArm) a (spec.explorationPulls * K) : Rat) = 0)
theorem
BanditRLProof.ETC.pullCount_actionWithCommit_succ_eq_add_if_commitArm_of_ge
Compiled
After the configured exploration horizon, one step of the fixed-commit ETC trace updates pull counts according to whether the queried arm is the commit arm. This is the `ETC-ACTION-WITH-COMMIT-POST-COMMIT-SUCC-COUNT` project-local trace/count update leaf.
theorem ETC.pullCount_actionWithCommit_succ_eq_add_if_commitArm_of_ge {K : Nat} (spec : ETC.Spec K) (commitArm a : Fin K) {t : Nat} (ht : spec.explorationPulls * K <= t) : pullCount (ETC.actionWithCommit spec commitArm) a (Nat.succ t) = pullCount (ETC.actionWithCommit spec commitArm) a t + if commitArm = a then 1 else 0
theorem
BanditRLProof.ETC.pullCount_actionWithCommit_explorationPulls_mul_K_add_eq
Compiled
After the configured exploration horizon, the fixed-commit ETC trace has a closed-form pull count: the commit arm receives every suffix pull, while all other arms keep their exploration-horizon count. This is the `ETC-ACTION-WITH-COMMIT-SUFFIX-COUNT` project-local trace/count closed-form leaf.
theorem ETC.pullCount_actionWithCommit_explorationPulls_mul_K_add_eq {K : Nat} (spec : ETC.Spec K) (commitArm a : Fin K) (r : Nat) : pullCount (ETC.actionWithCommit spec commitArm) a (spec.explorationPulls * K + r) = spec.explorationPulls + (if commitArm = a then r else 0)
theorem
BanditRLProof.ETC.pullCount_actionWithCommit_explorationPulls_mul_K_add_eq_of_ne
Compiled
After the configured exploration horizon, every non-commit arm keeps its exploration-horizon pull count. This is the `ETC-ACTION-WITH-COMMIT-NONCOMMIT-SUFFIX-COUNT` project-local trace/count corollary.
theorem ETC.pullCount_actionWithCommit_explorationPulls_mul_K_add_eq_of_ne {K : Nat} (spec : ETC.Spec K) {commitArm a : Fin K} (hne : commitArm ≠ a) (r : Nat) : pullCount (ETC.actionWithCommit spec commitArm) a (spec.explorationPulls * K + r) = spec.explorationPulls
theorem
BanditRLProof.ETC.pullCount_actionWithCommit_explorationPulls_mul_K_add_eq_commitArm
Compiled
After the configured exploration horizon, the commit arm has the exploration count plus every suffix pull. This is the `ETC-ACTION-WITH-COMMIT-COMMITARM-SUFFIX-COUNT` project-local trace/count corollary.
theorem ETC.pullCount_actionWithCommit_explorationPulls_mul_K_add_eq_commitArm {K : Nat} (spec : ETC.Spec K) (commitArm : Fin K) (r : Nat) : pullCount (ETC.actionWithCommit spec commitArm) commitArm (spec.explorationPulls * K + r) = spec.explorationPulls + r