def compositeObjective {X : Type u} (f : X → ℝ) (Ψ : X → WithTop ℝ) : X → WithTop ℝ

The extended composite objective x ↦ f x + Ψ x built from a real-valued smooth term and an extended-valued regularizer on the same ambient space.

@[simp]

theorem compositeObjective_apply {X : Type u} (f : X → ℝ) (Ψ : X → WithTop ℝ) (x : X) : compositeObjective f Ψ x = ↑(f x) + Ψ x

Evaluating the extended composite objective recovers the defining sum f x + Ψ x.

structure CompositeConvexMinimizationProblem (E : Type u) [NormedAddCommGroup E] [NormedSpace ℝ E] extends SetConstrainedMinimizationProblem E : Type u

Definition 3.21, generalized from the textbook ℝⁿ setting: a composite convex minimization problem consists of a closed feasible set Q, a smooth convex part f that belongs to ConvexC1On Q, and a closed convex term Ψ on Q, representing the objective x ↦ f x + Ψ x minimized over Q. The ambient smooth pair (Q, f) is owned canonically by SetConstrainedMinimizationProblem, the smooth regularity/convexity package by ConvexC1On, and the nonsmooth term by ClosedConvexOn. The textbook ℝⁿ case is the specialization CompositeConvexMinimizationProblem (EuclideanSpace ℝ (Fin n)).

• feasibleSet : Set E
• objective : E → ℝ
• feasibleSet_closed : IsClosed self.feasibleSet

  The feasible set Q is closed.

• smoothPart_convexC1 : ConvexC1On self.feasibleSet self.objective

  The smooth term belongs to the canonical Chapter 2 owner ConvexC1On Q.

• nonsmoothPart : E → WithTop ℝ

  The closed convex term Ψ : ℝⁿ → ℝ ∪ {+∞}.

• nonsmoothPart_closedConvex : ClosedConvexOn self.feasibleSet self.nonsmoothPart

  The nonsmooth term is closed and convex on Q.

@[reducible, inline]

abbrev CompositeConvexMinimizationProblem.smoothPart {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] (problem : CompositeConvexMinimizationProblem E) : E → ℝ

The source-facing smooth term f is the inherited Chapter 1 objective.

theorem CompositeConvexMinimizationProblem.smoothPart_convex {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] (problem : CompositeConvexMinimizationProblem E) : ConvexOn ℝ problem.feasibleSet problem.smoothPart

The smooth term is convex on the feasible set Q.

theorem CompositeConvexMinimizationProblem.smoothPart_contDiff {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] (problem : CompositeConvexMinimizationProblem E) : ContDiffOn ℝ 1 problem.smoothPart problem.feasibleSet

The smooth term is C¹ on the feasible set Q.

theorem CompositeConvexMinimizationProblem.feasibleSet_convex {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] (problem : CompositeConvexMinimizationProblem E) : Convex ℝ problem.feasibleSet

The feasible set of a composite convex minimization problem is convex.

@[implicit_reducible]

instance CompositeConvexMinimizationProblem.instCoeFunForallWithTopReal {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] : CoeFun (CompositeConvexMinimizationProblem E) fun (x : CompositeConvexMinimizationProblem E) => E → WithTop ℝ

A composite convex minimization problem can be used as its extended-valued objective x ↦ f(x) + Ψ(x).

@[simp]

theorem CompositeConvexMinimizationProblem.coe_apply {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] (problem : CompositeConvexMinimizationProblem E) (x : E) : compositeObjective problem.smoothPart problem.nonsmoothPart x = ↑(problem.smoothPart x) + problem.nonsmoothPart x

Evaluating a composite convex minimization problem gives its composite objective value.