theorem scaledObjective_convergence_rate_bound {X : Type u} {ι : Type u_1} [Fintype ι] (m : ι → ℕ) (f : X → ℝ) (xHat : X) {fBar : ℝ} {N : ℕ} (hP : 0 < ∑ j : ι, ↑(m j)) (hbound : ↑(f xHat) - { feasibleSet := Set.univ, objective := f }.optimalValue ≤ 2 * ↑(∑ j : ι, ↑(m j)) * ↑fBar / ↑√(↑N * (↑N + 1))) : ↑(averageIndividualExpense (∑ j : ι, ↑(m j)) f xHat) - { feasibleSet := Set.univ, objective := averageIndividualExpense (∑ j : ι, ↑(m j)) f }.optimalValue ≤ 2 * ↑fBar / ↑√(↑N * (↑N + 1))

Proposition 6.18: if P = \sum_j m_j is positive and an iterate xHat satisfies f(xHat) - f* ≤ 2 P \bar f / √(N (N + 1)), then the scaled objective \bar f(x) = f(x) / P satisfies \bar f(xHat) - \bar f* ≤ 2 \bar f / √(N (N + 1)), with both optimal values taken through the Chapter 1 whole-space owner in EReal.