@[simp]

theorem mem_effective_domain_inner_perturbation_iff {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (h : E → EReal) (a u : E) : (u ∈ effective_domain fun (v : E) => ↑(inner ℝ a v) + h v) ↔ u ∈ effective_domain h

Adding the everywhere-finite linear perturbation u ↦ ⟪a, u⟫ does not change the effective domain.

theorem zero_mem_subdifferential_inner_perturbation_iff_neg_mem_euclideanSubdifferential {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (h : E → EReal) (a x : E) : 0 ∈ ∂fun (u : E) => ↑(inner ℝ a u) + h u(x) ↔ -a ∈ euclideanSubdifferential h x

Zero is a subgradient of the affine perturbation u ↦ ⟪a, u⟫ + h(u) at x exactly when -a belongs to the Euclidean subdifferential of h at x.

theorem mem_admm_x_subproblem_solutions_iff_neg_adjoint_mem_euclideanSubdifferential {X : Type u} {Y : Type w} [NormedAddCommGroup X] [InnerProductSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup Y] [InnerProductSpace ℝ Y] [FiniteDimensional ℝ Y] (h₁ : X → EReal) (A : X →ₗ[ℝ] Y) (hh₁_dom : (effective_domain h₁).Nonempty) (y : Y) (x : X) : x ∈ unconstrained_problem_solutions (admm_x_subproblem h₁ A y) ↔ -(LinearMap.adjoint A) y ∈ euclideanSubdifferential h₁ x

A point minimizes the x-subproblem from Proposition 15.2 exactly when -Aᵀ y belongs to the Euclidean subdifferential of h₁ at that point.

theorem mem_admm_z_subproblem_solutions_iff_neg_adjoint_mem_euclideanSubdifferential {Z : Type v} {Y : Type w} [NormedAddCommGroup Z] [InnerProductSpace ℝ Z] [FiniteDimensional ℝ Z] [NormedAddCommGroup Y] [InnerProductSpace ℝ Y] [FiniteDimensional ℝ Y] (h₂ : Z → EReal) (B : Z →ₗ[ℝ] Y) (hh₂_dom : (effective_domain h₂).Nonempty) (y : Y) (z : Z) : z ∈ unconstrained_problem_solutions (admm_z_subproblem h₂ B y) ↔ -(LinearMap.adjoint B) y ∈ euclideanSubdifferential h₂ z

A point minimizes the z-subproblem from Proposition 15.2 exactly when -Bᵀ y belongs to the Euclidean subdifferential of h₂ at that point.

theorem admm_dual_optimality_condition_iff_exists_primal_subgradient_and_affine_update {X : Type u} {Z : Type v} {Y : Type w} [NormedAddCommGroup X] [InnerProductSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup Z] [InnerProductSpace ℝ Z] [FiniteDimensional ℝ Z] [NormedAddCommGroup Y] [InnerProductSpace ℝ Y] [FiniteDimensional ℝ Y] (ρ : ℝ) (h₁ : X → EReal) (h₂ : Z → EReal) (A : X →ₗ[ℝ] Y) (B : Z →ₗ[ℝ] Y) (c yk yNext : Y) (hPair : IsADMMConvexObjectivePair h₁ h₂) : admm_dual_optimality_condition ρ h₁ h₂ A B c yk yNext ↔ ∃ (xNext : X), -(LinearMap.adjoint A) yNext ∈ euclideanSubdifferential h₁ xNext ∧ ∃ (zNext : Z), -(LinearMap.adjoint B) yNext ∈ euclideanSubdifferential h₂ zNext ∧ yNext = yk + ρ • (A xNext + B zNext - c)

Proposition 15.3: equation (15.5) is equivalent to the existence of primal witnesses x^(k+1) and z^(k+1) satisfying the affine update (15.6) together with the Euclidean subdifferential conditions corresponding to (15.7) and (15.8).