noncomputable def dual_based_proximal_gradient_primal_optimal_value {E : Type u} {Y : Type v} (f : E → EReal) (g : Y → EReal) (A : E → Y) : EReal

The optimal value f_opt of the dual-based primal model is the infimum of the range of the primal objective x ↦ f x + g (A x).

@[simp]

theorem dual_based_proximal_gradient_primal_optimal_value_eq_sInf {E : Type u} {Y : Type v} (f : E → EReal) (g : Y → EReal) (A : E → Y) : dual_based_proximal_gradient_primal_optimal_value f g A = sInf (Set.range (composite_model_objective f (g ∘ A)))

Expanding the primal optimal value gives the infimum of the attained objective values.