theorem qualification_nonempty_iff_exists_ri_map_eq {E : Type u} {V : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [AddCommGroup V] [Module ℝ V] [TopologicalSpace V] (f : E → EReal) (g : V → EReal) (A : E →ₗ[ℝ] V) : (intrinsicInterior ℝ (effective_domain f) ∩ ⇑A ⁻¹' intrinsicInterior ℝ (effective_domain g)).Nonempty ↔ ∃ xHat ∈ intrinsicInterior ℝ (effective_domain f), ∃ zHat ∈ intrinsicInterior ℝ (effective_domain g), A xHat = zHat

The relative-interior qualification for the linear map A is equivalent to the source wording that there exist x̂ ∈ ri(dom f) and ẑ ∈ ri(dom g) with A x̂ = ẑ.

class IsDualBasedProximalGradientProblem {E : Type u} {V : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [AddCommGroup V] [Module ℝ V] [TopologicalSpace V] (f : E → EReal) (g : V → EReal) (A : E →ₗ[ℝ] V) (σ : ↑PosReal) extends IsProperExtendedRealFunction f : Prop

Definition 12.1.1: Assumption 12.1 means that f : E → (-∞, ∞] is proper, closed, and σ-strongly convex for a positive parameter σ : PosReal; g : V → (-∞, ∞] is proper, closed, and convex; A : E →ₗ[ℝ] V is linear; and the relative interiors of dom f and dom g satisfy the qualification ri (dom f) ∩ A⁻¹' (ri (dom g)) ≠ ∅, equivalently there exist x̂ ∈ ri(dom f) and ẑ ∈ ri(dom g) with A x̂ = ẑ.

• ne_bot (x : E) : f x ≠ ⊥
• effective_domain_nonempty : (effective_domain f).Nonempty
• f_closed : LowerSemicontinuous f
• f_strongly_convex : StrongConvexOn (effective_domain f) ↑σ fun (x : E) => (f x).toReal
• g_proper : IsProperExtendedRealFunction g
• g_closed : LowerSemicontinuous g
• g_convex : is_convex_function g
• qualification : (intrinsicInterior ℝ (effective_domain f) ∩ ⇑A ⁻¹' intrinsicInterior ℝ (effective_domain g)).Nonempty

theorem IsDualBasedProximalGradientProblem.strongConvexOn_and_qualification {E : Type u} {V : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [AddCommGroup V] [Module ℝ V] [TopologicalSpace V] {f : E → EReal} {g : V → EReal} {A : E →ₗ[ℝ] V} {σ : ↑PosReal} (h : IsDualBasedProximalGradientProblem f g A σ) : (StrongConvexOn (effective_domain f) ↑σ fun (x : E) => (f x).toReal) ∧ (intrinsicInterior ℝ (effective_domain f) ∩ ⇑A ⁻¹' intrinsicInterior ℝ (effective_domain g)).Nonempty

Assumption 12.1 packages primal strong convexity together with the relative-interior qualification used throughout the Chapter 12 duality arguments.

theorem IsDualBasedProximalGradientProblem.exists_mem_intrinsicInterior_map_eq {E : Type u} {V : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [AddCommGroup V] [Module ℝ V] [TopologicalSpace V] {f : E → EReal} {g : V → EReal} {A : E →ₗ[ℝ] V} {σ : ↑PosReal} (h : IsDualBasedProximalGradientProblem f g A σ) : ∃ xHat ∈ intrinsicInterior ℝ (effective_domain f), ∃ zHat ∈ intrinsicInterior ℝ (effective_domain g), A xHat = zHat

Assumption 12.1 provides a point x̂ ∈ ri(dom f) whose image A x̂ lies in ri(dom g). Equivalently, there exist x̂ ∈ ri(dom f) and ẑ ∈ ri(dom g) with A x̂ = ẑ.