noncomputable def dual_projected_subgradient_partial_average_rate_constant {E : Type u} {m : ℕ} [NeZero m] (f : E → ℝ) (fOpt qOpt : ℝ) (g : Fin m → E → ℝ) (xBar : E) (L : ℝ) (lam0 : Fin m → NNReal) : ℝ

The explicit numerator constant from Theorem 8.48, namely 2 * L * ((M + 2 * α)^2 + log 3) with M = dual_projected_subgradient_multiplier_norm_bound f fOpt qOpt g xBar L 1 lam0 and α = (f xBar - fOpt) / strict_feasibility_margin g xBar.

@[simp]

theorem dual_projected_subgradient_partial_average_rate_constant_def {E : Type u} {m : ℕ} [NeZero m] (f : E → ℝ) (fOpt qOpt : ℝ) (g : Fin m → E → ℝ) (xBar : E) (L : ℝ) (lam0 : Fin m → NNReal) : dual_projected_subgradient_partial_average_rate_constant f fOpt qOpt g xBar L lam0 = have α := (f xBar - fOpt) / strict_feasibility_margin g xBar; have M := dual_projected_subgradient_multiplier_norm_bound f fOpt qOpt g xBar L 1 lam0; 2 * L * ((M + 2 * α) ^ 2 + Real.log 3)

theorem partialGammaSqSum_eq_harmonicHalfTailSum (k : ℕ) : ∑ n ∈ Finset.Icc (k / 2) k, (fun (n : ℕ) => 1 / √(↑n + 1)) n ^ 2 = harmonicHalfTailSum k

Helper for Theorem 8.48: the squared suffix-window stepsizes are exactly the half-tail harmonic sum from Lemma 8.27.

theorem scaledPartialTailRatioLeRateConstant {L : ℝ} (hL : 0 ≤ L) (D : ℝ) (hD : 0 ≤ D) (k : ℕ) : L / 2 * (D + ∑ n ∈ Finset.Icc (k / 2) k, (fun (n : ℕ) => 1 / √(↑n + 1)) n ^ 2) / ∑ n ∈ Finset.Icc (k / 2) k, 1 / √(↑n + 1) ≤ 2 * L * (D + Real.log 3) / √(↑k + 2)

Helper for Theorem 8.48: scaling the half-tail harmonic ratio estimate by L / 2 yields the explicit O(1 / √k) suffix-window rate constant.

theorem partialAverageEqCenterMassOfActiveWindow {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {m : ℕ} [NeZero m] {X : Set E} {g : Fin m → E → ℝ} (xSel : (Fin m → NNReal) → { x : E // x ∈ X }) (lam0 : Fin m → NNReal) {k : ℕ} (hactive : ∀ n ∈ Finset.Icc (k / 2) k, (fun (n : ℕ) => dual_projected_subgradient_constraint_vector g ↑(dual_projected_subgradient_primal_iterate X g xSel (fun (n : ℕ) => 1 / √(↑n + 1)) lam0 n)) n ≠ 0) : dual_projected_subgradient_partial_average_iterate xSel (fun (n : ℕ) => 1 / √(↑n + 1)) lam0 k = (Finset.Icc (k / 2) k).centerMass (fun (n : ℕ) => (fun (n : ℕ) => 1 / √(↑n + 1)) n / ‖(fun (n : ℕ) => dual_projected_subgradient_constraint_vector g ↑(dual_projected_subgradient_primal_iterate X g xSel (fun (n : ℕ) => 1 / √(↑n + 1)) lam0 n)) n‖) fun (n : ℕ) => ↑(dual_projected_subgradient_primal_iterate X g xSel (fun (n : ℕ) => 1 / √(↑n + 1)) lam0 n)

Helper for Theorem 8.48: on the active suffix window, the repaired partial average is the centerMass attached to the suffix weights γ_n / ‖g(x^n)‖₂.

theorem partialAverageMem {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {m : ℕ} [NeZero m] {X XStar : Set E} {f : E → ℝ} {g : Fin m → E → ℝ} {fOpt : ℝ} (xSel : (Fin m → NNReal) → { x : E // x ∈ X }) (lam0 : Fin m → NNReal) (h_problem : IsDualProjectedSubgradientProblem X XStar f g fOpt) (h_admissible : dual_projected_subgradient_method_is_admissible X f g xSel fun (n : ℕ) => 1 / √(↑n + 1)) {k : ℕ} : dual_projected_subgradient_partial_average_iterate xSel (fun (n : ℕ) => 1 / √(↑n + 1)) lam0 k ∈ X

Helper for Theorem 8.48: the repaired suffix average remains in the feasible set X.

theorem slaterRatio_supportsPositiveConstraintViolation {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {m : ℕ} [NeZero m] {X XStar : Set E} {f : E → ℝ} {g : Fin m → E → ℝ} {fOpt : ℝ} {xBar : E} (h_problem : IsDualProjectedSubgradientProblem X XStar f g fOpt) (hxBar : xBar ∈ X) (hgBar : ∀ (i : Fin m), g i xBar < 0) {x : E} (hx : x ∈ X) : 0 ≤ f x - fOpt + (f xBar - fOpt) / strict_feasibility_margin g xBar * positive_constraint_violation (fun (y : E) (i : Fin m) => g i y) x

Helper for Theorem 8.48: the Slater ratio bounds the positive-part constraint violation from below through an optimal dual multiplier, so every feasible point satisfies the support inequality 0 ≤ f x - fOpt + α * positive_constraint_violation g x.

theorem partialAverageObjectiveGapLeRateBase {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {m : ℕ} [NeZero m] {X XStar : Set E} {f : E → ℝ} {g : Fin m → E → ℝ} {fOpt qOpt L : ℝ} (xSel : (Fin m → NNReal) → { x : E // x ∈ X }) (lam0 : Fin m → NNReal) {xBar : E} (h_problem : IsDualProjectedSubgradientProblem X XStar f g fOpt) (h_admissible : dual_projected_subgradient_method_is_admissible X f g xSel fun (n : ℕ) => 1 / √(↑n + 1)) (h_constraint_bound : ∀ x ∈ X, ‖dual_projected_subgradient_constraint_vector g x‖ ≤ L) (hdual_value : IsLUB (lagrangian_dual_objective X f (dual_constraint_vector g) '' dual_problem_feasible_set m) ↑qOpt) (hxBar : xBar ∈ X) (hgBar : ∀ (i : Fin m), g i xBar < 0) {k : ℕ} (hk : 2 ≤ k) : f (dual_projected_subgradient_partial_average_iterate xSel (fun (n : ℕ) => 1 / √(↑n + 1)) lam0 k) - fOpt ≤ 2 * L * (dual_projected_subgradient_multiplier_norm_bound f fOpt qOpt g xBar L 1 lam0 ^ 2 + Real.log 3) / √(↑k + 2)

Helper for Theorem 8.48: the suffix average satisfies the objective-gap half of the O(1 / √k) estimate, which is the α = 0 branch of the main theorem.

theorem partialAveragePenalizedGapLeRate {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {m : ℕ} [NeZero m] {X XStar : Set E} {f : E → ℝ} {g : Fin m → E → ℝ} {fOpt qOpt L : ℝ} (xSel : (Fin m → NNReal) → { x : E // x ∈ X }) (lam0 : Fin m → NNReal) {xBar : E} (h_problem : IsDualProjectedSubgradientProblem X XStar f g fOpt) (h_admissible : dual_projected_subgradient_method_is_admissible X f g xSel fun (n : ℕ) => 1 / √(↑n + 1)) (h_constraint_bound : ∀ x ∈ X, ‖dual_projected_subgradient_constraint_vector g x‖ ≤ L) (hdual_value : IsLUB (lagrangian_dual_objective X f (dual_constraint_vector g) '' dual_problem_feasible_set m) ↑qOpt) (hxBar : xBar ∈ X) (hgBar : ∀ (i : Fin m), g i xBar < 0) (hAlpha : 0 < (f xBar - fOpt) / strict_feasibility_margin g xBar) {k : ℕ} (hk : 2 ≤ k) : f (dual_projected_subgradient_partial_average_iterate xSel (fun (n : ℕ) => 1 / √(↑n + 1)) lam0 k) - fOpt + 2 * ((f xBar - fOpt) / strict_feasibility_margin g xBar) * positive_constraint_violation (fun (y : E) (i : Fin m) => g i y) (dual_projected_subgradient_partial_average_iterate xSel (fun (n : ℕ) => 1 / √(↑n + 1)) lam0 k) ≤ dual_projected_subgradient_partial_average_rate_constant f fOpt qOpt g xBar L lam0 / √(↑k + 2)

Helper for Theorem 8.48: the suffix average satisfies the penalized estimate corresponding to equation (8.89) with penalty coefficient 2 * α.

theorem dual_projected_subgradient_partial_average_rate_max_le {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {m : ℕ} [NeZero m] {X XStar : Set E} {f : E → ℝ} {g : Fin m → E → ℝ} {fOpt qOpt L : ℝ} (xSel : (Fin m → NNReal) → { x : E // x ∈ X }) (lam0 : Fin m → NNReal) {xBar : E} (h_problem : IsDualProjectedSubgradientProblem X XStar f g fOpt) (h_admissible : dual_projected_subgradient_method_is_admissible X f g xSel fun (n : ℕ) => 1 / √(↑n + 1)) (h_constraint_bound : ∀ x ∈ X, ‖dual_projected_subgradient_constraint_vector g x‖ ≤ L) (hdual_value : IsLUB (lagrangian_dual_objective X f (dual_constraint_vector g) '' dual_problem_feasible_set m) ↑qOpt) (hxBar : xBar ∈ X) (hgBar : ∀ (i : Fin m), g i xBar < 0) {k : ℕ} (hk : 2 ≤ k) : max (f (dual_projected_subgradient_partial_average_iterate xSel (fun (n : ℕ) => 1 / √(↑n + 1)) lam0 k) - fOpt) ((f xBar - fOpt) / strict_feasibility_margin g xBar * positive_constraint_violation (fun (y : E) (i : Fin m) => g i y) (dual_projected_subgradient_partial_average_iterate xSel (fun (n : ℕ) => 1 / √(↑n + 1)) lam0 k)) ≤ dual_projected_subgradient_partial_average_rate_constant f fOpt qOpt g xBar L lam0 / √(↑k + 2)

Theorem 8.48: for the partial averaging iterate generated by the dual projected subgradient method with stepsizes γ_k = 1 / √(k + 1), both the objective gap and the scaled constraint violation decay at rate O(1 / √k); equivalently, the maximum of f(x^(k)) - fOpt and α * positive_constraint_violation g (x^(k)) is bounded by the explicit constant built from the source quantities M and α.

theorem dual_projected_subgradient_partial_average_objective_gap_le {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {m : ℕ} [NeZero m] {X XStar : Set E} {f : E → ℝ} {g : Fin m → E → ℝ} {fOpt qOpt L : ℝ} (xSel : (Fin m → NNReal) → { x : E // x ∈ X }) (lam0 : Fin m → NNReal) {xBar : E} (h_problem : IsDualProjectedSubgradientProblem X XStar f g fOpt) (h_admissible : dual_projected_subgradient_method_is_admissible X f g xSel fun (n : ℕ) => 1 / √(↑n + 1)) (h_constraint_bound : ∀ x ∈ X, ‖dual_projected_subgradient_constraint_vector g x‖ ≤ L) (hdual_value : IsLUB (lagrangian_dual_objective X f (dual_constraint_vector g) '' dual_problem_feasible_set m) ↑qOpt) (hxBar : xBar ∈ X) (hgBar : ∀ (i : Fin m), g i xBar < 0) {k : ℕ} (hk : 2 ≤ k) : f (dual_projected_subgradient_partial_average_iterate xSel (fun (n : ℕ) => 1 / √(↑n + 1)) lam0 k) - fOpt ≤ dual_projected_subgradient_partial_average_rate_constant f fOpt qOpt g xBar L lam0 / √(↑k + 2)

The partial averaging iterate satisfies the objective-gap estimate (8.86).

theorem dual_projected_subgradient_partial_average_constraint_norm_le {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {m : ℕ} [NeZero m] {X XStar : Set E} {f : E → ℝ} {g : Fin m → E → ℝ} {fOpt qOpt L : ℝ} (xSel : (Fin m → NNReal) → { x : E // x ∈ X }) (lam0 : Fin m → NNReal) {xBar : E} (h_problem : IsDualProjectedSubgradientProblem X XStar f g fOpt) (h_admissible : dual_projected_subgradient_method_is_admissible X f g xSel fun (n : ℕ) => 1 / √(↑n + 1)) (h_constraint_bound : ∀ x ∈ X, ‖dual_projected_subgradient_constraint_vector g x‖ ≤ L) (hdual_value : IsLUB (lagrangian_dual_objective X f (dual_constraint_vector g) '' dual_problem_feasible_set m) ↑qOpt) (hxBar : xBar ∈ X) (hgBar : ∀ (i : Fin m), g i xBar < 0) (hAlpha : 0 < (f xBar - fOpt) / strict_feasibility_margin g xBar) {k : ℕ} (hk : 2 ≤ k) : positive_constraint_violation (fun (y : E) (i : Fin m) => g i y) (dual_projected_subgradient_partial_average_iterate xSel (fun (n : ℕ) => 1 / √(↑n + 1)) lam0 k) ≤ dual_projected_subgradient_partial_average_rate_constant f fOpt qOpt g xBar L lam0 / ((f xBar - fOpt) / strict_feasibility_margin g xBar * √(↑k + 2))

If the Slater ratio α is positive, the partial averaging iterate satisfies the constraint-violation estimate (8.87).