BanditRLProof.Algorithms.ETCSumRewardsDiff

Real-valued centered pairwise reward-difference summand for arm `a` against the model's selected best arm at one ETC exploration-horizon time index. The expression remains deterministic and pointwise. Future probability leaves may impose independence or sub-Gaussian contracts on this function.

noncomputable def centeredPairwiseRewardDiff {Omega : Type u} {K : Nat} (spec : ETC.Spec K) (model : FiniteBanditModel K) (commitArm : Fin K) (reward : Omega -> RewardTrace Rat) (a : Fin K) (t : Nat) (omega : Omega) : Real

Real-valued threshold corresponding to `explorationPulls` copies of the mean gap between the selected best arm and arm `a`.

noncomputable def centeredPairwiseGapThreshold {K : Nat} (spec : ETC.Spec K) (model : FiniteBanditModel K) (a : Fin K) : Real

The selected centered reward sum for one arm equals its selected reward total minus its pull count times the supplied mean. This helper is part of the `ETC-SUMREWARDS-PAIRWISE-DIFF-FINSET` bridge. It uses the existing Mathlib-backed `sumRewards` and `pullCount` Finset wrappers.

theorem selectedSubMean_sum_eq_sumRewards_sub_pullCount_mul {Action : Type} [DecidableEq Action] (action : ActionTrace Action) (reward : RewardTrace Rat) (a : Action) (n : Nat) (mu : Rat) : (Finset.range n).sum (fun t : Nat => if action t = a then reward t - mu else 0) = sumRewards action reward a n - (pullCount action a n : Rat) * mu

The selected negative centered reward sum for one arm equals its pull count times the supplied mean minus its selected reward total. This is the best-arm companion to `selectedSubMean_sum_eq_sumRewards_sub_pullCount_mul`.

theorem meanSubSelected_sum_eq_pullCount_mul_sub_sumRewards {Action : Type} [DecidableEq Action] (action : ActionTrace Action) (reward : RewardTrace Rat) (a : Action) (n : Nat) (mu : Rat) : (Finset.range n).sum (fun t : Nat => if action t = a then mu - reward t else 0) = (pullCount action a n : Rat) * mu - sumRewards action reward a n

If two arms have the same pull count by a horizon and the fixed-horizon reward sum of `b` is at most that of `a`, then the centered pairwise reward-difference finite sum is at least `m * (muB - muA)`. This is the deterministic algebra core of `ETC-SUMREWARDS-PAIRWISE-DIFF-FINSET`. The equal-count assumptions are kept explicit so ETC can discharge them with its exploration-horizon count theorem.

theorem sumRewards_le_imp_centered_pairwise_sum_ge {Action : Type} [DecidableEq Action] (action : ActionTrace Action) (reward : RewardTrace Rat) (a b : Action) (n m : Nat) (muA muB : Rat) (hcount_a : pullCount action a n = m) (hcount_b : pullCount action b n = m) (hraw : sumRewards action reward b n <= sumRewards action reward a n) : (m : Rat) * (muB - muA) <= (Finset.range n).sum (fun t : Nat => (if action t = a then reward t - muA else 0) + (if action t = b then muB - reward t else 0))

Concrete ETC event inclusion from the empirical-mean comparison event to the centered pairwise reward-difference finite-sum event over the configured exploration horizon. This leaf instantiates the earlier abstract event-shape adapter with `idx := Finset.range (spec.explorationPulls * K)` and the centered non-best-minus-best reward-difference summands. It still does not prove independence, sub-Gaussianity, filtration, or final ETC regret.

theorem empMeanAtExploration_ge_best_event_subset_centered_pairwise_sum_event {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) : Set.Subset {omega : Omega | ETC.empMeanAtExploration spec commitArm (reward omega) a >= ETC.empMeanAtExploration spec commitArm (reward omega) model.bestArm} {omega : Omega | ETC.centeredPairwiseGapThreshold spec model a <= (Finset.range (spec.explorationPulls * K)).sum (fun t : Nat => ETC.centeredPairwiseRewardDiff spec model commitArm reward a t omega)}