theorem dynamicGammaSqSum_eq_harmonicPrefixSum (k : ℕ) : ∑ n ∈ Finset.range (k + 1), (fun (n : ℕ) => 1 / √(↑n + 1)) n ^ 2 = harmonicPrefixSum k

Helper for Theorem 8.46: the squared dynamic stepsizes form the harmonic prefix sum from Lemma 8.27.

theorem dynamicGammaSum_eq_inverseSqrtPrefixSum (k : ℕ) : ∑ n ∈ Finset.range (k + 1), 1 / √(↑n + 1) = inverseSqrtPrefixSum k

Helper for Theorem 8.46: the dynamic stepsizes themselves form the inverse-square-root prefix sum from Lemma 8.27.

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

Helper for Theorem 8.46: scaling the harmonic-prefix ratio estimate by L / 2 preserves the O(log(k) / √k) bound for the dynamic stepsize sequence.

theorem fullAverage_eq_centerMass_of_activeWindow {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 : Fin (k + 1)), (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_full_average_iterate xSel (fun (n : ℕ) => 1 / √(↑n + 1)) lam0 k = (Finset.Icc 0 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.46: on the active full-history branch, the repaired average is the centerMass of the same weights used in the full-window bridge from Lemma 8.45.

theorem fullAverage_mem {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_full_average_iterate xSel (fun (n : ℕ) => 1 / √(↑n + 1)) lam0 k ∈ X

Helper for Theorem 8.46: the repaired full-history average remains in the feasible ambient set X.

theorem dualFeasiblePairing_le_positiveConstraintViolation {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {m : ℕ} [NeZero m] {g : Fin m → E → ℝ} {x : E} {lam : EuclideanSpace ℝ (Fin m)} (hLam : lam ∈ dual_problem_feasible_set m) : ∑ i : Fin m, lam.ofLp i * g i x ≤ ‖lam‖ * positive_constraint_violation (fun (x : E) (i : Fin m) => g i x) x

Helper for Theorem 8.46: any feasible dual multiplier pairs with the constraint vector by at most the Euclidean norm of the positive constraint violation.

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

Helper for Theorem 8.46: the Slater ratio controls the positive-part constraint violation from below through any optimal dual multiplier.

theorem fullAverageObjectiveGapLeLogOverSqrtBase {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {m : ℕ} [NeZero m] {X XStar : Set E} {f : E → ℝ} {g : Fin m → E → ℝ} {fOpt L : ℝ} (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)) (h_constraint_bound : ∀ x ∈ X, ‖dual_projected_subgradient_constraint_vector g x‖ ≤ L) {k : ℕ} (hk : 1 ≤ k) : f (dual_projected_subgradient_full_average_iterate xSel (fun (n : ℕ) => 1 / √(↑n + 1)) lam0 k) - fOpt ≤ L / 2 * (‖dual_projected_subgradient_multiplier_vector lam0‖ ^ 2 + 1 + Real.log (↑k + 1)) / √(↑k + 1)

Helper for Theorem 8.46: the full-history average satisfies the objective-gap O(log(k) / √k) bound for the dynamic stepsize sequence.

theorem fullAveragePenalizedGapLeLogOverSqrt {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {m : ℕ} [NeZero m] {X XStar : Set E} {f : E → ℝ} {g : Fin m → E → ℝ} {fOpt L : ℝ} (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)) (h_constraint_bound : ∀ x ∈ X, ‖dual_projected_subgradient_constraint_vector g x‖ ≤ L) {xBar : E} (hxBar : xBar ∈ X) (hgBar : ∀ (i : Fin m), g i xBar < 0) (hAlpha : 0 < (f xBar - fOpt) / strict_feasibility_margin g xBar) {k : ℕ} (hk : 1 ≤ k) : have α := (f xBar - fOpt) / strict_feasibility_margin g xBar; f (dual_projected_subgradient_full_average_iterate xSel (fun (n : ℕ) => 1 / √(↑n + 1)) lam0 k) - fOpt + 2 * α * positive_constraint_violation (fun (x : E) (i : Fin m) => g i x) (dual_projected_subgradient_full_average_iterate xSel (fun (n : ℕ) => 1 / √(↑n + 1)) lam0 k) ≤ L / 2 * ((‖dual_projected_subgradient_multiplier_vector lam0‖ + 2 * α) ^ 2 + 1 + Real.log (↑k + 1)) / √(↑k + 1)

Helper for Theorem 8.46: the full-history average satisfies the penalized objective-plus-violation O(log(k) / √k) bound with penalty coefficient 2 α.

theorem dual_projected_subgradient_full_average_rate_max_le_log_over_sqrt {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {m : ℕ} [NeZero m] {X XStar : Set E} {f : E → ℝ} {g : Fin m → E → ℝ} {fOpt L : ℝ} (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)) (h_constraint_bound : ∀ x ∈ X, ‖dual_projected_subgradient_constraint_vector g x‖ ≤ L) {xBar : E} (hxBar : xBar ∈ X) (hgBar : ∀ (i : Fin m), g i xBar < 0) {k : ℕ} (hk : 1 ≤ k) : have α := (f xBar - fOpt) / strict_feasibility_margin g xBar; have rhs := L / 2 * ((‖dual_projected_subgradient_multiplier_vector lam0‖ + 2 * α) ^ 2 + 1 + Real.log (↑k + 1)) / √(↑k + 1); max (f (dual_projected_subgradient_full_average_iterate xSel (fun (n : ℕ) => 1 / √(↑n + 1)) lam0 k) - fOpt) (α * positive_constraint_violation (fun (x : E) (i : Fin m) => g i x) (dual_projected_subgradient_full_average_iterate xSel (fun (n : ℕ) => 1 / √(↑n + 1)) lam0 k)) ≤ rhs

Theorem 8.46: under Assumption 8.41, if ‖g x‖ ≤ L on X and xBar is a strict feasible point, then the full-history averaged iterate generated by the dual projected subgradient method with stepsizes γ_k = 1 / √(k + 1) satisfies the O(log(k) / √k) bound on the maximum of the objective gap and the Slater-scaled positive-part constraint violation.

theorem dual_projected_subgradient_full_average_objective_gap_le_log_over_sqrt {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {m : ℕ} [NeZero m] {X XStar : Set E} {f : E → ℝ} {g : Fin m → E → ℝ} {fOpt L : ℝ} (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)) (h_constraint_bound : ∀ x ∈ X, ‖dual_projected_subgradient_constraint_vector g x‖ ≤ L) {xBar : E} (hxBar : xBar ∈ X) (hgBar : ∀ (i : Fin m), g i xBar < 0) {k : ℕ} (hk : 1 ≤ k) : f (dual_projected_subgradient_full_average_iterate xSel (fun (n : ℕ) => 1 / √(↑n + 1)) lam0 k) - fOpt ≤ L / 2 * ((‖dual_projected_subgradient_multiplier_vector lam0‖ + 2 * ((f xBar - fOpt) / strict_feasibility_margin g xBar)) ^ 2 + 1 + Real.log (↑k + 1)) / √(↑k + 1)

The full-history averaged iterate satisfies the objective-gap half of the O(log(k) / √k) rate bound.

theorem dual_projected_subgradient_full_average_constraint_norm_le_log_over_sqrt {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {m : ℕ} [NeZero m] {X XStar : Set E} {f : E → ℝ} {g : Fin m → E → ℝ} {fOpt L : ℝ} (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)) (h_constraint_bound : ∀ x ∈ X, ‖dual_projected_subgradient_constraint_vector g x‖ ≤ L) {xBar : E} (hxBar : xBar ∈ X) (hgBar : ∀ (i : Fin m), g i xBar < 0) (hAlpha : 0 < (f xBar - fOpt) / strict_feasibility_margin g xBar) {k : ℕ} (hk : 1 ≤ k) : positive_constraint_violation (fun (x : E) (i : Fin m) => g i x) (dual_projected_subgradient_full_average_iterate xSel (fun (n : ℕ) => 1 / √(↑n + 1)) lam0 k) ≤ L / (2 * ((f xBar - fOpt) / strict_feasibility_margin g xBar)) * ((‖dual_projected_subgradient_multiplier_vector lam0‖ + 2 * ((f xBar - fOpt) / strict_feasibility_margin g xBar)) ^ 2 + 1 + Real.log (↑k + 1)) / √(↑k + 1)

If the Slater ratio is positive, the full-history averaged iterate also satisfies the positive-part-constraint-violation half of the O(log(k) / √k) rate bound.