Arithmetic core: hit-rate lower bound from the potential bound #
The real-analytic step of the MWU regret argument. Starting from the T-step
potential upper bound (1 - η)^H ≤ N · (1 - η · v)^T on an individual
column, together with sufficiently small η and sufficiently large T,
deduce the per-column hit-rate lower bound v - ε ≤ H / T.
Pure real-analysis: Real.log monotonicity + log (1-x) ≤ -x +
-η/(1-η) ≤ log(1-η) + linarith/nlinarith bookkeeping.
theorem
ProbabilityTheory.hitRate_from_potential
{N H T : ℕ}
{η v ε : ℝ}
(hNpos : 0 < ↑N)
(hη : 0 < η)
(hη1 : η < 1)
(hv1 : v ≤ 1)
(hTpos : 0 < T)
(hpot : (1 - η) ^ H ≤ ↑N * (1 - η * v) ^ T)
(hηsmall : η ≤ ε / 4)
(hlargeT : Real.log ↑N / (η * ↑T) ≤ ε / 4)
:
Arithmetic core of the MWU regret bound. From the potential bound plus the step-size
feasibility conditions, deduce v - ε ≤ H / T.