noncomputable def stochastic_projected_subgradient_strongly_convex_average_iterate {Ω : Type v} {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → EReal} {C XStar : Set E} {fOpt : ℝ} (h_problem : IsConstrainedConvexProblem f C XStar fOpt) (g : ℕ → ↑C → Ω → E) (t : ℕ → ℝ) (x0 : ↑C) (k : ℕ) : Ω → E

The weighted average random iterate x^(k) used in the strongly convex stochastic projected-subgradient rate. It uses the canonical weight convention from Theorem 8.31, so x^(0) = x^0 and for k > 0 the coefficients are α_n^k = 2 n / (k (k + 1)).

theorem stochastic_projected_subgradient_strongly_convex_average_iterate_eq_sum {Ω : Type v} {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → EReal} {C XStar : Set E} {fOpt : ℝ} (h_problem : IsConstrainedConvexProblem f C XStar fOpt) (g : ℕ → ↑C → Ω → E) (t : ℕ → ℝ) (x0 : ↑C) (k : ℕ) : stochastic_projected_subgradient_strongly_convex_average_iterate h_problem g t x0 k = fun (ω : Ω) => ∑ n ∈ Finset.range (k + 1), projected_subgradient_strongly_convex_average_weight k n • stochastic_projected_subgradient_method_iterate C ⋯ ⋯ ⋯ g t x0 n ω

Evaluating the stochastic strongly convex averaged iterate at k gives the weighted sum ∑_{n=0}^k α_n^k x^n(ω) with the canonical Chapter 8 ergodic weights α_n^k.

theorem stochastic_projected_subgradient_strongly_convex_average_iterate_zero {Ω : Type v} {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → EReal} {C XStar : Set E} {fOpt : ℝ} (h_problem : IsConstrainedConvexProblem f C XStar fOpt) (g : ℕ → ↑C → Ω → E) (t : ℕ → ℝ) (x0 : ↑C) (ω : Ω) : stochastic_projected_subgradient_strongly_convex_average_iterate h_problem g t x0 0 ω = stochastic_projected_subgradient_method_iterate C ⋯ ⋯ ⋯ g t x0 0 ω

The stochastic strongly convex weighted average at k = 0 is the initial random iterate x^0.

theorem toDualMap_mem_subdifferential_of_mem_euclideanSubdifferentialAt_toReal {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {f : E → EReal} {C XStar : Set E} {fOpt : ℝ} (h_problem : IsConstrainedConvexProblem f C XStar fOpt) {x v : E} (hx : x ∈ effective_domain f) (hv : v ∈ euclideanSubdifferentialAt (fun (y : E) => (f y).toReal) x) : ↑((InnerProductSpace.toDualMap ℝ E) v) ∈ ∂f(x)

Helper for Theorem 8.37: a Euclidean subgradient of the real-valued restriction x ↦ (f x).toReal at a finite point yields a genuine subgradient of the original extended-real objective.

theorem strongly_convex_support_at_optimal_point {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {f : E → EReal} {C XStar : Set E} {fOpt σ : ℝ} (h_problem : IsConstrainedConvexProblem f C XStar fOpt) (h_strong : StrongConvexOn (effective_domain f) σ fun (x : E) => (f x).toReal) (hσ : 0 < σ) {x xStar v : E} (hxC : x ∈ C) (hxStar : xStar ∈ XStar) (hv : v ∈ euclideanSubdifferentialAt (fun (y : E) => (f y).toReal) x) : (f x).toReal - fOpt + σ / 2 * ‖x - xStar‖ ^ 2 ≤ inner ℝ v (x - xStar)

Helper for Theorem 8.37: every Euclidean subgradient at a feasible point supports the strongly convex objective at an optimal point with the quadratic correction term.

@[reducible, inline]

noncomputable abbrev stochastic_iterate_sigma_algebra {Ω : Type v} {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → EReal} {C XStar : Set E} {fOpt : ℝ} (h_problem : IsConstrainedConvexProblem f C XStar fOpt) (g : ℕ → ↑C → Ω → E) (t : ℕ → ℝ) (x0 : ↑C) [MeasurableSpace E] (n : ℕ) : MeasurableSpace Ω

The sigma-algebra generated by the stochastic iterate x[n].

theorem ae_condexp_inner_ge_gap_add_strong_term {Ω : Type v} {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → EReal} {C XStar : Set E} {fOpt σ : ℝ} (h_problem : IsConstrainedConvexProblem f C XStar fOpt) (g : ℕ → ↑C → Ω → E) (t : ℕ → ℝ) (x0 : ↑C) [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasurableSpace E] (h_strong : StrongConvexOn (effective_domain f) σ fun (x : E) => (f x).toReal) (hσ : 0 < σ) (h_oracle : StochasticProjectedSubgradientOracle μ (fun (x : E) => (f x).toReal) (stochastic_projected_subgradient_method_iterate C ⋯ ⋯ ⋯ g t x0) fun (n : ℕ) (ω : Ω) => g n (stochastic_projected_subgradient_method C ⋯ ⋯ ⋯ g t x0 n ω) ω) {xStar : E} (hxStar : xStar ∈ XStar) (n : ℕ) : ∀ᵐ (ω : Ω) ∂μ, (f (stochastic_projected_subgradient_method_iterate C ⋯ ⋯ ⋯ g t x0 n ω)).toReal - fOpt + σ / 2 * ‖stochastic_projected_subgradient_method_iterate C ⋯ ⋯ ⋯ g t x0 n ω - xStar‖ ^ 2 ≤ inner ℝ (μ[fun (ω : Ω) => g n (stochastic_projected_subgradient_method C ⋯ ⋯ ⋯ g t x0 n ω) ω | stochastic_iterate_sigma_algebra h_problem g t x0 n] ω) (stochastic_projected_subgradient_method_iterate C ⋯ ⋯ ⋯ g t x0 n ω - xStar)

Helper for Theorem 8.37: the oracle unbiasedness clause lifts the deterministic strong support inequality to the conditional expectation subgradient almost surely.

theorem condexp_inner_of_aestronglyMeasurable_right {Ω : Type v} {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {m : MeasurableSpace Ω} {u v : Ω → E} (hv : MeasureTheory.AEStronglyMeasurable v μ) (huv : MeasureTheory.Integrable (fun (ω : Ω) => inner ℝ (u ω) (v ω)) μ) (hu : MeasureTheory.Integrable u μ) : μ[fun (ω : Ω) => inner ℝ (u ω) (v ω) | m] =ᵐ[μ] fun (ω : Ω) => inner ℝ (μ[u | m] ω) (v ω)

Helper for Theorem 8.37: once the right factor is measurable with respect to the conditioning sigma-algebra, the conditional expectation of the inner product pulls through that factor.

theorem stochastic_iterate_aestronglyMeasurable {Ω : Type v} {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → EReal} {C XStar : Set E} {fOpt : ℝ} (h_problem : IsConstrainedConvexProblem f C XStar fOpt) (g : ℕ → ↑C → Ω → E) (t : ℕ → ℝ) (x0 : ↑C) [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasurableSpace E] (h_oracle : StochasticProjectedSubgradientOracle μ (fun (x : E) => (f x).toReal) (stochastic_projected_subgradient_method_iterate C ⋯ ⋯ ⋯ g t x0) fun (n : ℕ) (ω : Ω) => g n (stochastic_projected_subgradient_method C ⋯ ⋯ ⋯ g t x0 n ω) ω) (n : ℕ) : MeasureTheory.AEStronglyMeasurable (stochastic_projected_subgradient_method_iterate C ⋯ ⋯ ⋯ g t x0 n) μ

Helper for Theorem 8.37: each stochastic iterate is almost surely strongly measurable.

theorem projected_sqdist_step_growth_bound {Ω : Type v} {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → EReal} {C XStar : Set E} {fOpt : ℝ} (h_problem : IsConstrainedConvexProblem f C XStar fOpt) (g : ℕ → ↑C → Ω → E) (t : ℕ → ℝ) (x0 : ↑C) {xStar : E} (hxStar : xStar ∈ XStar) (n : ℕ) (ω : Ω) : ‖stochastic_projected_subgradient_method_iterate C ⋯ ⋯ ⋯ g t x0 (n + 1) ω - xStar‖ ^ 2 ≤ 2 * ‖stochastic_projected_subgradient_method_iterate C ⋯ ⋯ ⋯ g t x0 n ω - xStar‖ ^ 2 + 2 * t n ^ 2 * ‖g n (stochastic_projected_subgradient_method C ⋯ ⋯ ⋯ g t x0 n ω) ω‖ ^ 2

Helper for Theorem 8.37: one stochastic projection step has a coarse quadratic growth bound, used only to bootstrap square-integrability of the iterates.

theorem stochastic_iterate_sqdist_integrable {Ω : Type v} {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → EReal} {C XStar : Set E} {fOpt : ℝ} (h_problem : IsConstrainedConvexProblem f C XStar fOpt) (g : ℕ → ↑C → Ω → E) (t : ℕ → ℝ) (x0 : ↑C) [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] [MeasurableSpace E] (h_oracle : StochasticProjectedSubgradientOracle μ (fun (x : E) => (f x).toReal) (stochastic_projected_subgradient_method_iterate C ⋯ ⋯ ⋯ g t x0) fun (n : ℕ) (ω : Ω) => g n (stochastic_projected_subgradient_method C ⋯ ⋯ ⋯ g t x0 n ω) ω) {xStar : E} (hxStar : xStar ∈ XStar) (n : ℕ) : MeasureTheory.Integrable (fun (ω : Ω) => ‖stochastic_projected_subgradient_method_iterate C ⋯ ⋯ ⋯ g t x0 n ω - xStar‖ ^ 2) μ

Helper for Theorem 8.37: the squared distance to the optimal point is integrable at every iterate, obtained from the coarse quadratic growth recursion.

theorem projected_sqdist_step_pointwise {Ω : Type v} {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → EReal} {C XStar : Set E} {fOpt : ℝ} (h_problem : IsConstrainedConvexProblem f C XStar fOpt) (g : ℕ → ↑C → Ω → E) (t : ℕ → ℝ) (x0 : ↑C) {xStar : E} (hxStar : xStar ∈ XStar) (n : ℕ) (ω : Ω) : ‖stochastic_projected_subgradient_method_iterate C ⋯ ⋯ ⋯ g t x0 (n + 1) ω - xStar‖ ^ 2 ≤ ‖stochastic_projected_subgradient_method_iterate C ⋯ ⋯ ⋯ g t x0 n ω - xStar‖ ^ 2 - 2 * t n * inner ℝ (g n (stochastic_projected_subgradient_method C ⋯ ⋯ ⋯ g t x0 n ω) ω) (stochastic_projected_subgradient_method_iterate C ⋯ ⋯ ⋯ g t x0 n ω - xStar) + t n ^ 2 * ‖g n (stochastic_projected_subgradient_method C ⋯ ⋯ ⋯ g t x0 n ω) ω‖ ^ 2

Helper for Theorem 8.37: the pathwise projection step satisfies the exact squared-distance expansion from equation (8.55) before conditioning.

theorem integrable_inner_iterate_offset {Ω : Type v} {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → EReal} {C XStar : Set E} {fOpt : ℝ} (h_problem : IsConstrainedConvexProblem f C XStar fOpt) (g : ℕ → ↑C → Ω → E) (t : ℕ → ℝ) (x0 : ↑C) [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] [MeasurableSpace E] (h_oracle : StochasticProjectedSubgradientOracle μ (fun (x : E) => (f x).toReal) (stochastic_projected_subgradient_method_iterate C ⋯ ⋯ ⋯ g t x0) fun (n : ℕ) (ω : Ω) => g n (stochastic_projected_subgradient_method C ⋯ ⋯ ⋯ g t x0 n ω) ω) (n : ℕ) {xStar : E} (hxStar : xStar ∈ XStar) : MeasureTheory.Integrable (fun (ω : Ω) => inner ℝ (g n (stochastic_projected_subgradient_method C ⋯ ⋯ ⋯ g t x0 n ω) ω) (stochastic_projected_subgradient_method_iterate C ⋯ ⋯ ⋯ g t x0 n ω - xStar)) μ

Helper for Theorem 8.37: the inner-product term in the projected-square expansion is integrable, because both the stochastic subgradient and the iterate offset belong to L².

theorem conditional_projected_sqdist_le_of_strongly_convex_support {Ω : Type v} {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → EReal} {C XStar : Set E} {fOpt σ : ℝ} (h_problem : IsConstrainedConvexProblem f C XStar fOpt) (g : ℕ → ↑C → Ω → E) (t : ℕ → ℝ) (x0 : ↑C) [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] [MeasurableSpace E] [BorelSpace E] (h_strong : StrongConvexOn (effective_domain f) σ fun (x : E) => (f x).toReal) (hσ : 0 < σ) (h_stepsize : ∀ (n : ℕ), t n = 2 / (σ * (↑n + 1))) (h_oracle : StochasticProjectedSubgradientOracle μ (fun (x : E) => (f x).toReal) (stochastic_projected_subgradient_method_iterate C ⋯ ⋯ ⋯ g t x0) fun (n : ℕ) (ω : Ω) => g n (stochastic_projected_subgradient_method C ⋯ ⋯ ⋯ g t x0 n ω) ω) {xStar : E} (hxStar : xStar ∈ XStar) (n : ℕ) (hm : stochastic_iterate_sigma_algebra h_problem g t x0 n ≤ inst✝) : ∀ᵐ (ω : Ω) ∂μ, μ[fun (ω : Ω) => ‖stochastic_projected_subgradient_method_iterate C ⋯ ⋯ ⋯ g t x0 (n + 1) ω - xStar‖ ^ 2 | stochastic_iterate_sigma_algebra h_problem g t x0 n] ω ≤ ‖stochastic_projected_subgradient_method_iterate C ⋯ ⋯ ⋯ g t x0 n ω - xStar‖ ^ 2 - 2 * t n * ((f (stochastic_projected_subgradient_method_iterate C ⋯ ⋯ ⋯ g t x0 n ω)).toReal - fOpt + σ / 2 * ‖stochastic_projected_subgradient_method_iterate C ⋯ ⋯ ⋯ g t x0 n ω - xStar‖ ^ 2) + t n ^ 2 * μ[fun (ω : Ω) => ‖g n (stochastic_projected_subgradient_method C ⋯ ⋯ ⋯ g t x0 n ω) ω‖ ^ 2 | stochastic_iterate_sigma_algebra h_problem g t x0 n] ω

Helper for Theorem 8.37: the conditional projected-square estimate at the sigma-algebra generated by the measurable iterate x[n]. This is the source-faithful (8.55) + (8.u196) bridge before any integration or telescoping.

theorem expectedGapStepWithStrongRemainder_le {Ω : Type v} {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → EReal} {C XStar : Set E} {fOpt σ : ℝ} (h_problem : IsConstrainedConvexProblem f C XStar fOpt) (g : ℕ → ↑C → Ω → E) (t : ℕ → ℝ) (x0 : ↑C) [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] [MeasurableSpace E] [BorelSpace E] (h_strong : StrongConvexOn (effective_domain f) σ fun (x : E) => (f x).toReal) (hσ : 0 < σ) (h_stepsize : ∀ (n : ℕ), t n = 2 / (σ * (↑n + 1))) (h_iterate_meas : ∀ (n : ℕ), Measurable (stochastic_projected_subgradient_method_iterate C ⋯ ⋯ ⋯ g t x0 n)) (h_oracle : StochasticProjectedSubgradientOracle μ (fun (x : E) => (f x).toReal) (stochastic_projected_subgradient_method_iterate C ⋯ ⋯ ⋯ g t x0) fun (n : ℕ) (ω : Ω) => g n (stochastic_projected_subgradient_method C ⋯ ⋯ ⋯ g t x0 n ω) ω) {xStar : E} (hxStar : xStar ∈ XStar) (n : ℕ) : 2 * t n * (∫ (x : Ω), (fun (ω : Ω) => (f (stochastic_projected_subgradient_method_iterate C ⋯ ⋯ ⋯ g t x0 n ω)).toReal) x ∂μ - fOpt) + σ * t n * ∫ (x : Ω), (fun (ω : Ω) => ‖stochastic_projected_subgradient_method_iterate C ⋯ ⋯ ⋯ g t x0 n ω - xStar‖ ^ 2) x ∂μ + ∫ (x : Ω), (fun (ω : Ω) => ‖stochastic_projected_subgradient_method_iterate C ⋯ ⋯ ⋯ g t x0 (n + 1) ω - xStar‖ ^ 2) x ∂μ ≤ ∫ (x : Ω), (fun (ω : Ω) => ‖stochastic_projected_subgradient_method_iterate C ⋯ ⋯ ⋯ g t x0 n ω - xStar‖ ^ 2) x ∂μ + t n ^ 2 * h_oracle.L_tilde_f ^ 2

Theorem 8.37: integrating the conditional one-step inequality first yields the stable expectation-level remainder estimate before the stepsize coefficients are normalized.

theorem expected_one_step_gap_le_of_strongly_convex_stepsize {Ω : Type v} {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → EReal} {C XStar : Set E} {fOpt σ : ℝ} (h_problem : IsConstrainedConvexProblem f C XStar fOpt) (g : ℕ → ↑C → Ω → E) (t : ℕ → ℝ) (x0 : ↑C) [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] [MeasurableSpace E] [BorelSpace E] (h_strong : StrongConvexOn (effective_domain f) σ fun (x : E) => (f x).toReal) (hσ : 0 < σ) (h_stepsize : ∀ (n : ℕ), t n = 2 / (σ * (↑n + 1))) (h_iterate_meas : ∀ (n : ℕ), Measurable (stochastic_projected_subgradient_method_iterate C ⋯ ⋯ ⋯ g t x0 n)) (h_oracle : StochasticProjectedSubgradientOracle μ (fun (x : E) => (f x).toReal) (stochastic_projected_subgradient_method_iterate C ⋯ ⋯ ⋯ g t x0) fun (n : ℕ) (ω : Ω) => g n (stochastic_projected_subgradient_method C ⋯ ⋯ ⋯ g t x0 n ω) ω) {xStar : E} (hxStar : xStar ∈ XStar) (n : ℕ) : ∫ (x : Ω), (fun (ω : Ω) => (f (stochastic_projected_subgradient_method_iterate C ⋯ ⋯ ⋯ g t x0 n ω)).toReal) x ∂μ - fOpt ≤ σ * (↑n - 1) / 4 * ∫ (x : Ω), (fun (ω : Ω) => ‖stochastic_projected_subgradient_method_iterate C ⋯ ⋯ ⋯ g t x0 n ω - xStar‖ ^ 2) x ∂μ - σ * (↑n + 1) / 4 * ∫ (x : Ω), (fun (ω : Ω) => ‖stochastic_projected_subgradient_method_iterate C ⋯ ⋯ ⋯ g t x0 (n + 1) ω - xStar‖ ^ 2) x ∂μ + h_oracle.L_tilde_f ^ 2 / (σ * (↑n + 1))

theorem weighted_expected_gap_sum_with_tail_le_of_strongly_convex_stepsize {Ω : Type v} {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → EReal} {C XStar : Set E} {fOpt σ : ℝ} (h_problem : IsConstrainedConvexProblem f C XStar fOpt) (g : ℕ → ↑C → Ω → E) (t : ℕ → ℝ) (x0 : ↑C) [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] [MeasurableSpace E] [BorelSpace E] (h_strong : StrongConvexOn (effective_domain f) σ fun (x : E) => (f x).toReal) (hσ : 0 < σ) (h_stepsize : ∀ (n : ℕ), t n = 2 / (σ * (↑n + 1))) (h_iterate_meas : ∀ (n : ℕ), Measurable (stochastic_projected_subgradient_method_iterate C ⋯ ⋯ ⋯ g t x0 n)) (h_oracle : StochasticProjectedSubgradientOracle μ (fun (x : E) => (f x).toReal) (stochastic_projected_subgradient_method_iterate C ⋯ ⋯ ⋯ g t x0) fun (n : ℕ) (ω : Ω) => g n (stochastic_projected_subgradient_method C ⋯ ⋯ ⋯ g t x0 n ω) ω) {xStar : E} (hxStar : xStar ∈ XStar) (k : ℕ) : ∑ n ∈ Finset.range (k + 1), ↑n * (∫ (x : Ω), (fun (ω : Ω) => (f (stochastic_projected_subgradient_method_iterate C ⋯ ⋯ ⋯ g t x0 n ω)).toReal) x ∂μ - fOpt) ≤ -(σ * ↑k * (↑k + 1) / 4) * ∫ (x : Ω), (fun (ω : Ω) => ‖stochastic_projected_subgradient_method_iterate C ⋯ ⋯ ⋯ g t x0 (k + 1) ω - xStar‖ ^ 2) x ∂μ + h_oracle.L_tilde_f ^ 2 * ↑k / σ

Helper for Theorem 8.37: the weighted telescope keeps the negative squared-distance tail before it is discarded in the final bound.

theorem weighted_expected_gap_sum_le_of_strongly_convex_stepsize {Ω : Type v} {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → EReal} {C XStar : Set E} {fOpt σ : ℝ} (h_problem : IsConstrainedConvexProblem f C XStar fOpt) (g : ℕ → ↑C → Ω → E) (t : ℕ → ℝ) (x0 : ↑C) [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] [MeasurableSpace E] [BorelSpace E] (h_strong : StrongConvexOn (effective_domain f) σ fun (x : E) => (f x).toReal) (hσ : 0 < σ) (h_stepsize : ∀ (n : ℕ), t n = 2 / (σ * (↑n + 1))) (h_iterate_meas : ∀ (n : ℕ), Measurable (stochastic_projected_subgradient_method_iterate C ⋯ ⋯ ⋯ g t x0 n)) (h_oracle : StochasticProjectedSubgradientOracle μ (fun (x : E) => (f x).toReal) (stochastic_projected_subgradient_method_iterate C ⋯ ⋯ ⋯ g t x0) fun (n : ℕ) (ω : Ω) => g n (stochastic_projected_subgradient_method C ⋯ ⋯ ⋯ g t x0 n ω) ω) {xStar : E} (hxStar : xStar ∈ XStar) (k : ℕ) : ∑ n ∈ Finset.range (k + 1), ↑n * (∫ (x : Ω), (fun (ω : Ω) => (f (stochastic_projected_subgradient_method_iterate C ⋯ ⋯ ⋯ g t x0 n ω)).toReal) x ∂μ - fOpt) ≤ h_oracle.L_tilde_f ^ 2 * ↑k / σ

Helper for Theorem 8.37: the n-weighted telescope obtained by summing the integrated one-step inequalities.

theorem normalized_strongly_convex_weighted_gap_le {Ω : Type v} {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → EReal} {C XStar : Set E} {fOpt σ : ℝ} (h_problem : IsConstrainedConvexProblem f C XStar fOpt) (g : ℕ → ↑C → Ω → E) (t : ℕ → ℝ) (x0 : ↑C) [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] [MeasurableSpace E] [BorelSpace E] (h_strong : StrongConvexOn (effective_domain f) σ fun (x : E) => (f x).toReal) (hσ : 0 < σ) (h_stepsize : ∀ (n : ℕ), t n = 2 / (σ * (↑n + 1))) (h_iterate_meas : ∀ (n : ℕ), Measurable (stochastic_projected_subgradient_method_iterate C ⋯ ⋯ ⋯ g t x0 n)) (h_oracle : StochasticProjectedSubgradientOracle μ (fun (x : E) => (f x).toReal) (stochastic_projected_subgradient_method_iterate C ⋯ ⋯ ⋯ g t x0) fun (n : ℕ) (ω : Ω) => g n (stochastic_projected_subgradient_method C ⋯ ⋯ ⋯ g t x0 n ω) ω) {xStar : E} (hxStar : xStar ∈ XStar) {k : ℕ} (hk : 0 < k) : ∑ n ∈ Finset.range (k + 1), 2 * ↑n / (↑k * (↑k + 1)) * (∫ (x : Ω), (fun (ω : Ω) => (f (stochastic_projected_subgradient_method_iterate C ⋯ ⋯ ⋯ g t x0 n ω)).toReal) x ∂μ - fOpt) ≤ 2 * h_oracle.L_tilde_f ^ 2 / (σ * (↑k + 1))

Helper for Theorem 8.37: normalizing the weighted telescope gives the exact simplex-weighted objective-gap estimate used in the ergodic part of the proof.

theorem strongly_convex_average_iterate_mem_feasible {Ω : Type v} {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → EReal} {C XStar : Set E} {fOpt : ℝ} (h_problem : IsConstrainedConvexProblem f C XStar fOpt) (g : ℕ → ↑C → Ω → E) (t : ℕ → ℝ) (x0 : ↑C) {k : ℕ} (hk : 0 < k) (ω : Ω) : stochastic_projected_subgradient_strongly_convex_average_iterate h_problem g t x0 k ω ∈ C

Helper for Theorem 8.37: for k > 0, the weighted average iterate is a convex combination of feasible iterates, hence it remains in C pathwise.

theorem averageIterateGap_le_weightedExpectedGaps {Ω : Type v} {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → EReal} {C XStar : Set E} {fOpt σ : ℝ} (h_problem : IsConstrainedConvexProblem f C XStar fOpt) (g : ℕ → ↑C → Ω → E) (t : ℕ → ℝ) (x0 : ↑C) [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] [MeasurableSpace E] [BorelSpace E] (h_strong : StrongConvexOn (effective_domain f) σ fun (x : E) => (f x).toReal) (hσ : 0 < σ) (h_oracle : StochasticProjectedSubgradientOracle μ (fun (x : E) => (f x).toReal) (stochastic_projected_subgradient_method_iterate C ⋯ ⋯ ⋯ g t x0) fun (n : ℕ) (ω : Ω) => g n (stochastic_projected_subgradient_method C ⋯ ⋯ ⋯ g t x0 n ω) ω) {k : ℕ} (hk : 0 < k) : ∫ (x : Ω), (fun (ω : Ω) => (f (stochastic_projected_subgradient_strongly_convex_average_iterate h_problem g t x0 k ω)).toReal) x ∂μ - fOpt ≤ ∑ n ∈ Finset.range (k + 1), projected_subgradient_strongly_convex_average_weight k n * (∫ (x : Ω), (fun (ω : Ω) => (f (stochastic_projected_subgradient_method_iterate C ⋯ ⋯ ⋯ g t x0 n ω)).toReal) x ∂μ - fOpt)

Helper for Theorem 8.37: for k > 0, Jensen's inequality converts the value gap at the stochastic weighted average iterate into the simplex-weighted sum of the expected iterate gaps.

theorem stochastic_projected_subgradient_best_value_gap_le_of_strongly_convex_stepsize {Ω : Type v} {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → EReal} {C XStar : Set E} {fOpt σ : ℝ} (h_problem : IsConstrainedConvexProblem f C XStar fOpt) (g : ℕ → ↑C → Ω → E) (t : ℕ → ℝ) (x0 : ↑C) [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] [MeasurableSpace E] [BorelSpace E] (h_strong : StrongConvexOn (effective_domain f) σ fun (x : E) => (f x).toReal) (hσ : 0 < σ) (h_stepsize : ∀ (n : ℕ), t n = 2 / (σ * (↑n + 1))) (h_iterate_meas : ∀ (n : ℕ), Measurable (stochastic_projected_subgradient_method_iterate C ⋯ ⋯ ⋯ g t x0 n)) (h_oracle : StochasticProjectedSubgradientOracle μ (fun (x : E) => (f x).toReal) (stochastic_projected_subgradient_method_iterate C ⋯ ⋯ ⋯ g t x0) fun (n : ℕ) (ω : Ω) => g n (stochastic_projected_subgradient_method C ⋯ ⋯ ⋯ g t x0 n ω) ω) (k : ℕ) : ∫ (x : Ω), (fun (ω : Ω) => best_achieved_function_value (fun (x : E) => (f x).toReal) (fun (n : ℕ) => stochastic_projected_subgradient_method_iterate C ⋯ ⋯ ⋯ g t x0 n ω) k) x ∂μ - fOpt ≤ 2 * h_oracle.L_tilde_f ^ 2 / (σ * (↑k + 1))

Part (1) of Theorem 8.37: under Assumptions 8.7 and 8.34, if f is σ-strongly convex with σ > 0, the stochastic projected subgradient method uses the stepsizes t_k = 2 / (σ (k + 1)), and the sampled directions satisfy the oracle assumptions along the generated iterates, with each iterate x^n measurable as a random variable, then the expected best objective value attained among the first k + 1 stochastic iterates satisfies E(f_best^k) - fOpt ≤ 2 L_tilde_f^2 / (σ (k + 1)).

theorem stochastic_projected_subgradient_average_value_gap_le_of_strongly_convex_stepsize {Ω : Type v} {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → EReal} {C XStar : Set E} {fOpt σ : ℝ} (h_problem : IsConstrainedConvexProblem f C XStar fOpt) (g : ℕ → ↑C → Ω → E) (t : ℕ → ℝ) (x0 : ↑C) [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] [MeasurableSpace E] [BorelSpace E] (h_strong : StrongConvexOn (effective_domain f) σ fun (x : E) => (f x).toReal) (hσ : 0 < σ) (h_stepsize : ∀ (n : ℕ), t n = 2 / (σ * (↑n + 1))) (h_iterate_meas : ∀ (n : ℕ), Measurable (stochastic_projected_subgradient_method_iterate C ⋯ ⋯ ⋯ g t x0 n)) (h_oracle : StochasticProjectedSubgradientOracle μ (fun (x : E) => (f x).toReal) (stochastic_projected_subgradient_method_iterate C ⋯ ⋯ ⋯ g t x0) fun (n : ℕ) (ω : Ω) => g n (stochastic_projected_subgradient_method C ⋯ ⋯ ⋯ g t x0 n ω) ω) (k : ℕ) : ∫ (x : Ω), (fun (ω : Ω) => (f (stochastic_projected_subgradient_strongly_convex_average_iterate h_problem g t x0 k ω)).toReal) x ∂μ - fOpt ≤ 2 * h_oracle.L_tilde_f ^ 2 / (σ * (↑k + 1))

Part (2) of Theorem 8.37: with the same assumptions as in part (1), the weighted average random iterate x^(k) = ∑_{n=0}^k α_n^k x^n, where α_n^k = 2 n / (k (k + 1)) for k > 0 and x^(0) = x^0, satisfies the same expected objective-gap bound E(f(x^(k))) - fOpt ≤ 2 L_tilde_f^2 / (σ (k + 1)).