noncomputable def adpmm_proximal_objective {E : Type u} {F : Type v} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (ρ : ↑PosReal) (h : E → EReal) (L : E →ₗ[ℝ] F) (P : E →ₗ[ℝ] E) (a : E) : E → EReal

The one-block proximal objective from Definition 15.4(D): u ↦ h(u) + (ρ / 2) ‖L u‖² + (1 / 2) ⟪u, P u⟫ + ⟪a, u⟫.

@[simp]

theorem adpmm_proximal_objective_apply {E : Type u} {F : Type v} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (ρ : ↑PosReal) (h : E → EReal) (L : E →ₗ[ℝ] F) (P : E →ₗ[ℝ] E) (a u : E) : adpmm_proximal_objective ρ h L P a u = h u + ↑(↑ρ / 2 * ‖L u‖ ^ 2) + ↑(1 / 2 * inner ℝ u (P u)) + ↑(inner ℝ a u)

Evaluating adpmm_proximal_objective gives h(u) + (ρ / 2) ‖L u‖² + (1 / 2) ⟪u, P u⟫ + ⟪a, u⟫.

class IsADPMMProblem {X : Type u} {Z : Type v} {Y : Type w} [NormedAddCommGroup X] [InnerProductSpace ℝ X] [NormedAddCommGroup Z] [InnerProductSpace ℝ Z] [NormedAddCommGroup Y] [NormedSpace ℝ Y] (ρ : ↑PosReal) (h₁ : X → EReal) (h₂ : Z → EReal) (A : X →ₗ[ℝ] Y) (B : Z →ₗ[ℝ] Y) (G : X →ₗ[ℝ] X) (Q : Z →ₗ[ℝ] Z) (c : Y) extends IsADMMConvexObjectivePair h₁ h₂ : Prop

Definition 15.4: Assumption 15.2 for the AD-PMM problem means that h₁ and h₂ form an ADMM convex objective pair, the proximal operators G and Q are symmetric positive semidefinite, every proximal one-block subproblem from clause (D) attains a minimizer, there exist x̂ ∈ ri(dom h₁) and ẑ ∈ ri(dom h₂) with A x̂ + B ẑ = c, and the canonical primal optimal set constrained_problem_solutions (H[h₁, h₂]) (admm_feasible_set A B c) is nonempty. The primal optimal value remains the canonical owner H_opt[h₁, h₂; A, B, c].

• ne_bot (x : X) : h₁ x ≠ ⊥
• effective_domain_nonempty : (effective_domain h₁).Nonempty
• h₂_proper : IsProperExtendedRealFunction h₂
• h₁_closed : LowerSemicontinuous h₁
• h₂_closed : LowerSemicontinuous h₂
• h₁_convex : is_convex_function h₁
• h₂_convex : is_convex_function h₂
• G_positive : G.IsPositive
• Q_positive : Q.IsPositive
• x_subproblem_argmin_nonempty (a : X) : (unconstrained_problem_solutions (adpmm_proximal_objective ρ h₁ A G a)).Nonempty
• z_subproblem_argmin_nonempty (b : Z) : (unconstrained_problem_solutions (adpmm_proximal_objective ρ h₂ B Q b)).Nonempty
• ri_qualification : ∃ xHat ∈ intrinsicInterior ℝ (effective_domain h₁), ∃ zHat ∈ intrinsicInterior ℝ (effective_domain h₂), A xHat + B zHat = c
• optimal_set_nonempty : (constrained_problem_solutions H[h₁, h₂] (admm_feasible_set A B c)).Nonempty

instance instFactOptimalSetNonemptyOfIsADPMMProblem {X : Type u} {Z : Type v} {Y : Type w} [NormedAddCommGroup X] [InnerProductSpace ℝ X] [NormedAddCommGroup Z] [InnerProductSpace ℝ Z] [NormedAddCommGroup Y] [NormedSpace ℝ Y] {ρ : ↑PosReal} {h₁ : X → EReal} {h₂ : Z → EReal} {A : X →ₗ[ℝ] Y} {B : Z →ₗ[ℝ] Y} {G : X →ₗ[ℝ] X} {Q : Z →ₗ[ℝ] Z} {c : Y} (h : IsADPMMProblem ρ h₁ h₂ A B G Q c) : Fact (constrained_problem_solutions H[h₁, h₂] (admm_feasible_set A B c)).Nonempty

Companion instance exposing nonemptiness of the canonical primal optimal set to typeclass search.