theorem finite_sum_stochastic_projected_subgradient_expected_best_value_gap_le {E : Type u} {Ω : Type v} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] [MeasurableSpace E] [BorelSpace E] {f : E → ℝ} {C XStar : Set E} {fOpt δ Θ : ℝ} {m : ℕ} (L : Fin m → ℝ) (h_problem : IsConstrainedConvexProblem (fun (x : E) => ↑(f x)) C XStar fOpt) (i : ℕ → Ω → Fin m) (g : ℕ → ↑C → Fin m → E) (x0 : ↑C) (h_oracle : StochasticProjectedSubgradientOracle μ f (fun (n : ℕ) (ω : Ω) => ↑(finite_sum_stochastic_projected_subgradient_method C ⋯ ⋯ Θ L i g x0 n ω)) fun (n : ℕ) (ω : Ω) => g n (finite_sum_stochastic_projected_subgradient_method C ⋯ ⋯ Θ L i g x0 n ω) (i n ω)) (hΘ : C.HasHalfSquaredDiameterBound Θ) (h_stepsize : projectedSubgradientUsesHalfSquaredDiameterStepsize Θ h_oracle.L_tilde_f (finite_sum_stochastic_projected_subgradient_stepsize Θ L)) (h_oracle_bound : 2 * (1 + Real.log 3) * h_oracle.L_tilde_f ≤ δ * finite_sum_stochastic_subgradient_bound_constant L) {k : ℕ} (hk : 2 ≤ k) : ∫ (x : Ω), (fun (ω : Ω) => best_achieved_function_value f (fun (n : ℕ) => ↑(finite_sum_stochastic_projected_subgradient_method C ⋯ ⋯ Θ L i g x0 n ω)) k) x ∂μ - fOpt ≤ δ * finite_sum_stochastic_subgradient_bound_constant L * √(2 * Θ) / √(↑k + 2)

Proposition 8.8: if the stochastic projected subgradient oracle along the sampled Algorithm 8.12 iterates has bound constant L_tilde_f controlled by δ * finite_sum_stochastic_subgradient_bound_constant L, and Algorithm 8.12 uses the canonical half-squared-diameter stepsize rule from Theorem 8.30, then the expected best objective gap of the first k + 1 iterates satisfies the finite-sum O(1 / √k) estimate E(f_best^k) - fOpt ≤ δ * finite_sum_stochastic_subgradient_bound_constant L * √(2 Θ) / √(k + 2).

theorem finite_sum_stochastic_projected_subgradient_expected_best_value_gap_le_epsilon_of_iteration_count {E : Type u} {Ω : Type v} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] [MeasurableSpace E] [BorelSpace E] {f : E → ℝ} {C XStar : Set E} {fOpt δ Θ : ℝ} {m : ℕ} (L : Fin m → ℝ) (h_problem : IsConstrainedConvexProblem (fun (x : E) => ↑(f x)) C XStar fOpt) (i : ℕ → Ω → Fin m) (g : ℕ → ↑C → Fin m → E) (x0 : ↑C) (h_oracle : StochasticProjectedSubgradientOracle μ f (fun (n : ℕ) (ω : Ω) => ↑(finite_sum_stochastic_projected_subgradient_method C ⋯ ⋯ Θ L i g x0 n ω)) fun (n : ℕ) (ω : Ω) => g n (finite_sum_stochastic_projected_subgradient_method C ⋯ ⋯ Θ L i g x0 n ω) (i n ω)) (hΘ : C.HasHalfSquaredDiameterBound Θ) (h_stepsize : projectedSubgradientUsesHalfSquaredDiameterStepsize Θ h_oracle.L_tilde_f (finite_sum_stochastic_projected_subgradient_stepsize Θ L)) (h_oracle_bound : 2 * (1 + Real.log 3) * h_oracle.L_tilde_f ≤ δ * finite_sum_stochastic_subgradient_bound_constant L) {ε : ℝ} (hε : 0 < ε) (k : ℕ) (hk : max (δ ^ 2 * (2 * Θ) * finite_sum_stochastic_subgradient_bound_constant L ^ 2 / ε ^ 2 - 2) 2 ≤ ↑k) : ∫ (x : Ω), (fun (ω : Ω) => best_achieved_function_value f (fun (n : ℕ) => ↑(finite_sum_stochastic_projected_subgradient_method C ⋯ ⋯ Θ L i g x0 n ω)) k) x ∂μ - fOpt ≤ ε

If the iteration index is at least the finite-sum complexity threshold from Proposition 8.8, then the expected best objective gap is at most ε.