def dual_projected_subgradient_constraint_vector {E : Type u} {m : ℕ} (g : Fin m → E → ℝ) (x : E) : EuclideanSpace ℝ (Fin m)

The constraint vector g(x) attached to a primal point x, viewed in the Euclidean multiplier space ℝ^m.

@[simp]

theorem dual_projected_subgradient_constraint_vector_apply {E : Type u} {m : ℕ} [NormedAddCommGroup E] (g : Fin m → E → ℝ) (x : E) (i : Fin m) : (dual_projected_subgradient_constraint_vector g x).ofLp i = g i x

Evaluating dual_projected_subgradient_constraint_vector g x at i returns g_i(x).

noncomputable def dual_projected_subgradient_multiplier_update {E : Type u} {m : ℕ} (g : Fin m → E → ℝ) (γ : ℝ) (lam : Fin m → NNReal) (x : E) : Fin m → NNReal

The positive-part multiplier update [λ + γ g(x) / ‖g(x)‖]_+, written coordinatewise in ℝ_+^m.

@[simp]

theorem dual_projected_subgradient_multiplier_update_apply {E : Type u} {m : ℕ} [NormedAddCommGroup E] (g : Fin m → E → ℝ) (γ : ℝ) (lam : Fin m → NNReal) (x : E) (i : Fin m) : dual_projected_subgradient_multiplier_update g γ lam x i = (↑(lam i) + γ * (dual_projected_subgradient_constraint_vector g x).ofLp i / ‖dual_projected_subgradient_constraint_vector g x‖).toNNReal

The i-th coordinate of the multiplier update is the positive part of the normalized subgradient step in that coordinate.

def dual_projected_subgradient_method {E : Type u} {m : ℕ} (X : Set E) (g : Fin m → E → ℝ) (xSel : (Fin m → NNReal) → { x : E // x ∈ X }) (γ : ℕ → ℝ) (lam0 : Fin m → NNReal) : ℕ → Fin m → NNReal

Algorithm 8.14: given an initial multiplier λ^0 ∈ ℝ_+^m, positive stepsizes γ_k, and a rule selecting for each multiplier λ a minimizer of the Lagrangian over X, the dual projected subgradient method generates the multiplier sequence λ^k; if g(x^k) = 0 it stays at λ^k, and otherwise updates by λ^{k+1} = [λ^k + γ_k g(x^k) / ‖g(x^k)‖]_+, where x^k is the selected Lagrangian minimizer at λ^k.

noncomputable def dual_projected_subgradient_primal_iterate {E : Type u} {m : ℕ} (X : Set E) (g : Fin m → E → ℝ) (xSel : (Fin m → NNReal) → { x : E // x ∈ X }) (γ : ℕ → ℝ) (lam0 : Fin m → NNReal) (k : ℕ) : { x : E // x ∈ X }

The primal point selected from argmin_X (f + λ^T g) at the current multiplier iterate.

def dual_projected_subgradient_method_is_admissible {E : Type u} {m : ℕ} (X : Set E) (f : E → ℝ) (g : Fin m → E → ℝ) (xSel : (Fin m → NNReal) → { x : E // x ∈ X }) (γ : ℕ → ℝ) : Prop

A selection rule and stepsize sequence are admissible for the dual projected subgradient method when every stepsize is positive and each selected point minimizes the corresponding Lagrangian over X.

@[simp]

theorem dual_projected_subgradient_method_zero {E : Type u} {m : ℕ} [NormedAddCommGroup E] (X : Set E) (g : Fin m → E → ℝ) (xSel : (Fin m → NNReal) → { x : E // x ∈ X }) (γ : ℕ → ℝ) (lam0 : Fin m → NNReal) : dual_projected_subgradient_method X g xSel γ lam0 0 = lam0

The dual projected-subgradient multiplier sequence starts at the prescribed initial multiplier.

@[simp]

theorem dual_projected_subgradient_primal_iterate_eq {E : Type u} {m : ℕ} [NormedAddCommGroup E] (X : Set E) (g : Fin m → E → ℝ) (xSel : (Fin m → NNReal) → { x : E // x ∈ X }) (γ : ℕ → ℝ) (lam0 : Fin m → NNReal) (k : ℕ) : dual_projected_subgradient_primal_iterate X g xSel γ lam0 k = xSel (dual_projected_subgradient_method X g xSel γ lam0 k)

The primal iterate x^k is obtained by applying the minimizer-selection rule to λ^k.

theorem dual_projected_subgradient_method_succ_of_constraint_vector_eq_zero {E : Type u} {m : ℕ} [NormedAddCommGroup E] (X : Set E) (g : Fin m → E → ℝ) (xSel : (Fin m → NNReal) → { x : E // x ∈ X }) (γ : ℕ → ℝ) (lam0 : Fin m → NNReal) (k : ℕ) (hk : dual_projected_subgradient_constraint_vector g ↑(dual_projected_subgradient_primal_iterate X g xSel γ lam0 k) = 0) : dual_projected_subgradient_method X g xSel γ lam0 (k + 1) = dual_projected_subgradient_method X g xSel γ lam0 k

If the current constraint vector is zero, the multiplier iterate does not move.

theorem dual_projected_subgradient_method_succ_of_constraint_vector_ne_zero {E : Type u} {m : ℕ} [NormedAddCommGroup E] (X : Set E) (g : Fin m → E → ℝ) (xSel : (Fin m → NNReal) → { x : E // x ∈ X }) (γ : ℕ → ℝ) (lam0 : Fin m → NNReal) (k : ℕ) (hk : dual_projected_subgradient_constraint_vector g ↑(dual_projected_subgradient_primal_iterate X g xSel γ lam0 k) ≠ 0) : dual_projected_subgradient_method X g xSel γ lam0 (k + 1) = dual_projected_subgradient_multiplier_update g (γ k) (dual_projected_subgradient_method X g xSel γ lam0 k) ↑(dual_projected_subgradient_primal_iterate X g xSel γ lam0 k)

If the current constraint vector is nonzero, the next multiplier iterate is the normalized positive-part update from Algorithm 8.14.

theorem dual_projected_subgradient_method_stepsize_pos {E : Type u} {m : ℕ} [NormedAddCommGroup E] (X : Set E) (g : Fin m → E → ℝ) (xSel : (Fin m → NNReal) → { x : E // x ∈ X }) (γ : ℕ → ℝ) {f : E → ℝ} (h : dual_projected_subgradient_method_is_admissible X f g xSel γ) (k : ℕ) : 0 < γ k

Under the admissibility condition, every stepsize in the dual projected subgradient method is strictly positive.

theorem dual_projected_subgradient_primal_iterate_isMinOn {E : Type u} {m : ℕ} [NormedAddCommGroup E] (X : Set E) (g : Fin m → E → ℝ) (xSel : (Fin m → NNReal) → { x : E // x ∈ X }) (γ : ℕ → ℝ) (lam0 : Fin m → NNReal) {f : E → ℝ} (h : dual_projected_subgradient_method_is_admissible X f g xSel γ) (k : ℕ) : IsMinOn (fun (x : E) => f x + ∑ i : Fin m, ↑(dual_projected_subgradient_method X g xSel γ lam0 k i) * g i x) X ↑(dual_projected_subgradient_primal_iterate X g xSel γ lam0 k)

Under the admissibility condition, the selected primal iterate x^k minimizes the Lagrangian over X at the current multiplier λ^k.