class IsSublevelDistanceBoundedSmoothConvexMinimizationProblem {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : E → ℝ) (XStar : outParam (Set E)) (fOpt : outParam ℝ) (Lf : outParam NNReal) extends IsFastProximalGradientProblem f 0 XStar fOpt Lf : Prop

Definition 10.65: clauses (A)-(C) mean that f : E → ℝ is convex and globally L_f-smooth, XStar = X^* is the nonempty optimal set of min_x f(x) with optimal value fOpt = f_opt, and for every α > 0 there is R_α > 0 such that every point x with f x ≤ α lies within distance at most R_α of the optimal set XStar. The convexity, smoothness, optimal-set, and optimal-value clauses are inherited from the canonical Chapter 10 owner IsFastProximalGradientProblem for the zero regularizer.

• g_proper : IsProperExtendedRealFunction 0
• g_closed : LowerSemicontinuous 0
• g_convex : is_convex_function 0
• f_convex : ConvexOn ℝ Set.univ f
• f_smooth : is_l_smooth_on f Set.univ Lf
• optimal_set_eq : XStar = unconstrained_problem_solutions (composite_model_objective (Function.toEReal f) 0)
• optimal_set_nonempty : XStar.Nonempty
• optimal_value_isGLB : IsGLB (Set.range (composite_model_objective (Function.toEReal f) 0)) ↑fOpt
• bounded_sublevel_distance_to_optimal_set (α : ↑PosReal) : ∃ (Rα : ↑PosReal), ∀ ⦃x : E⦄, f x ≤ ↑α → Metric.infDist x XStar ≤ ↑Rα

instance instFactConvexOnUnivOfIsSublevelDistanceBoundedSmoothConvexMinimizationProblem {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {XStar : Set E} {fOpt : ℝ} {Lf : NNReal} (h : IsSublevelDistanceBoundedSmoothConvexMinimizationProblem f XStar fOpt Lf) : Fact (ConvexOn ℝ Set.univ f)

In Definition 10.65, the real-valued objective is convex on the whole space.