BanditRLProof.Algorithms.ETCEmpiricalMean

Empirical mean of arm `a` at the configured ETC exploration horizon for a fixed-commit trace. This is the `ETC-EMP-MEAN-ACTION-WITH-COMMIT-EXPLORATION` project-local leaf.

def empMeanAtExploration {K : Nat} (spec : ETC.Spec K) (commitArm : Fin K) (reward : RewardTrace Rat) (a : Fin K) : Rat

Exploration empirical means depend only on the reward coordinates observed before the configured exploration horizon. This is the prefix-congruence bridge needed to reconstruct the ETC commit score from a finite reward history after exploration, rather than from an ambient reward trace with future coordinates.

theorem empMeanAtExploration_eq_of_eq_on_prefix {K : Nat} (spec : ETC.Spec K) (commitArm : Fin K) (reward0 reward1 : RewardTrace Rat) (hprefix : forall t, t < spec.explorationPulls * K -> reward0 t = reward1 t) (a : Fin K) : ETC.empMeanAtExploration spec commitArm reward0 a = ETC.empMeanAtExploration spec commitArm reward1 a

Once a finite reward history reaches the configured exploration horizon, its default-completed trace gives the same ETC exploration empirical mean as the ambient reward trace. This is the history-reconstruction bridge for a later generated commit policy: at generated action time `t + 1`, the state reads a history through `t`, so the explicit `spec.explorationPulls * K <= t + 1` contract supplies every score coordinate used by the commit rule.

theorem empMeanAtExploration_completeRewardTrace_eq_of_explorationHorizon_le {K : Nat} (spec : ETC.Spec K) (commitArm : Fin K) (reward : RewardTrace Rat) (t : Nat) (horizon_le : spec.explorationPulls * K <= t + 1) (a : Fin K) : ETC.empMeanAtExploration spec commitArm (History.completeRewardTrace t (History.finiteRewardHistoryOfTrace reward t) (0 : Rat)) a = ETC.empMeanAtExploration spec commitArm reward a

The empirical-mean denominator at the ETC exploration horizon rewrites to the configured number of exploration pulls per arm.

theorem empMeanAtExploration_eq_sumRewards_div_explorationPulls {K : Nat} (spec : ETC.Spec K) (commitArm : Fin K) (reward : RewardTrace Rat) (a : Fin K) : ETC.empMeanAtExploration spec commitArm reward a = sumRewards (ETC.actionWithCommit spec commitArm) reward a (spec.explorationPulls * K) / ((spec.explorationPulls : Nat) : Rat)

At a positive exploration count, comparing two fixed-commit ETC empirical means is equivalent to comparing their fixed-horizon reward sums. This is the `ETC-EMP-MEAN-COMPARISON-AS-FINITE-SUM` deterministic algebra leaf. It only removes the common positive denominator from two empirical means; it does not introduce probability, concentration, filtration, or final ETC regret.

theorem empMeanAtExploration_le_iff_sumRewards_le_of_explorationPulls_pos {K : Nat} (spec : ETC.Spec K) (commitArm : Fin K) (reward : RewardTrace Rat) (a b : Fin K) (hexplorationPulls_pos : 0 < spec.explorationPulls) : ETC.empMeanAtExploration spec commitArm reward b <= ETC.empMeanAtExploration spec commitArm reward a ↔ sumRewards (ETC.actionWithCommit spec commitArm) reward b (spec.explorationPulls * K) <= sumRewards (ETC.actionWithCommit spec commitArm) reward a (spec.explorationPulls * K)

At a positive exploration count, a pointwise implication from the fixed-horizon reward-sum comparison into a real finite-sum tail event yields the matching event inclusion from the non-best empirical-mean comparison event. This is the `ETC-EMPMEAN-EVENT-SUBSET-SUMREWARDS-TAIL-EVENT` bridge. It is only an event-shape adapter; it does not instantiate centered reward differences, prove sub-Gaussianity, introduce filtrations, or prove final ETC regret.

theorem empMeanAtExploration_ge_best_event_subset_sumRewards_tail_event_of_imp {Omega : Type u} {K : Nat} (spec : ETC.Spec K) (model : FiniteBanditModel K) (commitArm : Fin K) (reward : Omega -> RewardTrace Rat) (a : Fin K) (hexplorationPulls_pos : 0 < spec.explorationPulls) {Idx : Type v} (idx : Finset Idx) (X : Idx -> Omega -> Real) (eps : Real) (himp : forall omega : Omega, sumRewards (ETC.actionWithCommit spec commitArm) (reward omega) model.bestArm (spec.explorationPulls * K) <= sumRewards (ETC.actionWithCommit spec commitArm) (reward omega) a (spec.explorationPulls * K) -> eps <= idx.sum (fun i => X i omega)) : Set.Subset {omega : Omega | ETC.empMeanAtExploration spec commitArm (reward omega) a >= ETC.empMeanAtExploration spec commitArm (reward omega) model.bestArm} {omega : Omega | eps <= idx.sum (fun i => X i omega)}