BanditRLProof.DelayedFeedback.StochasticGapHalfSet

Arithmetic mean of a finite family of real gaps. Lean's total division makes this definition equal to zero when `K = 0`; the counting theorem below handles that empty case before using the denominator.

noncomputable def finiteAverageGap {K : Nat} (gap : Fin K -> Real) : Real

Indices whose gaps are strictly greater than twice the finite average, matching the strict word "greater" in the source statement of Lemma D.11.

noncomputable def aboveTwiceAverageGap {K : Nat} (gap : Fin K -> Real) : Finset (Fin K)

Nonnegative-domain deterministic content used by the source's Lemma D.11. Nonnegativity is explicit rather than extending the promoted contract to an arbitrary signed family. The theorem includes `K = 0`; for positive `K`, its proof separately closes the zero-average branch before cancelling the positive average in the usual counting/Markov argument.

theorem two_mul_card_aboveTwiceAverageGap_le {K : Nat} (gap : Fin K -> Real) (hgap : forall i, 0 <= gap i) : 2 * (aboveTwiceAverageGap gap).card <= K

The stochastic loss gap convention used by the delayed-SAPO source: smaller mean loss is better, so the gap of arm `i` is `mean i - mean optimal`.

def sourceStochasticLossGap {K : Nat} (mean : Fin K -> Real) (optimal i : Fin K) : Real

An optimal arm makes every source stochastic loss gap nonnegative.

theorem sourceStochasticLossGap_nonneg {K : Nat} (mean : Fin K -> Real) (optimal : Fin K) (hoptimal : forall i, mean optimal <= mean i) (i : Fin K) : 0 <= sourceStochasticLossGap mean optimal i

Bandit specialization of the nonnegative-domain D.11 counting statement. Among the `K` stochastic loss gaps from an optimal arm, strictly fewer than half can exceed twice their average (and hence their cardinality is at most half). This is a deterministic producer; it does not assume or claim any generated delayed-feedback probability law.

theorem two_mul_card_sourceStochasticLossGap_aboveTwiceAverage_le {K : Nat} (mean : Fin K -> Real) (optimal : Fin K) (hoptimal : forall i, mean optimal <= mean i) : 2 * (aboveTwiceAverageGap (sourceStochasticLossGap mean optimal)).card <= K