theorem conjugate_primal_eq_pairing_sub_of_mem_primal_argmax {E : Type u} {V : Type v} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] (f : E → EReal) (g : V → EReal) (A : E →ₗ[ℝ] V) (σ : ↑PosReal) (h_problem : IsDualBasedProximalGradientProblem f g A σ) (yBar : V) (xBar : E) (hxBar : xBar ∈ dual_proximal_gradient_primal_x_argmax f A yBar) : f∗ ((LinearMap.adjoint A) yBar) = ↑(inner ℝ xBar ((LinearMap.adjoint A) yBar)) - f xBar

Helper for Lemma 12.7: an argmax point of x ↦ ⟪x, Aᵀ yBar⟫ - f x attains the conjugate value (f∗) (A.adjoint yBar).

theorem ereal_neg_sub_real (a : EReal) (r : ℝ) : -(a - ↑r) = ↑r - a

Helper for Lemma 12.7: negating a - r with a finite real term r gives r - a.

theorem ereal_neg_real_sub (a : EReal) (r : ℝ) : -(↑r - a) = a - ↑r

Helper for Lemma 12.7: negating r - a with a finite real term r gives a - r.

theorem isMinOn_shifted_objective_of_mem_primal_argmax {E : Type u} {V : Type v} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] (f : E → EReal) (g : V → EReal) (A : E →ₗ[ℝ] V) (σ : ↑PosReal) (h_problem : IsDualBasedProximalGradientProblem f g A σ) (yBar : V) (xBar : E) (hxBar : xBar ∈ dual_proximal_gradient_primal_x_argmax f A yBar) : IsMinOn (fun (x : E) => f x - ↑(inner ℝ x ((LinearMap.adjoint A) yBar))) Set.univ xBar

Helper for Lemma 12.7: the Chapter 12 primal argmax point is the minimizer of the shifted objective x ↦ f x - ⟪x, Aᵀ yBar⟫.

theorem primal_minimizer_mem_effective_domain {E : Type u} {V : Type v} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] (f : E → EReal) (g : V → EReal) (A : E →ₗ[ℝ] V) (σ : ↑PosReal) (h_problem : IsDualBasedProximalGradientProblem f g A σ) (xStar : E) (hxStar : IsMinOn (composite_model_objective f (g ∘ ⇑A)) Set.univ xStar) : xStar ∈ effective_domain f

Helper for Lemma 12.7: every primal minimizer has finite f-value, because the qualification point provides a finite comparison value for the primal objective.

theorem shifted_objective_effective_domain_eq {E : Type u} {V : Type v} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] (f : E → EReal) (g : V → EReal) (A : E →ₗ[ℝ] V) (σ : ↑PosReal) (h_problem : IsDualBasedProximalGradientProblem f g A σ) (yBar : V) : (effective_domain fun (x : E) => f x - ↑(inner ℝ x ((LinearMap.adjoint A) yBar))) = effective_domain f

Helper for Lemma 12.7: subtracting the finite linear term ⟪x, Aᵀ yBar⟫ does not change the effective domain of f.

theorem shifted_objective_gap_ge_half_sigma_sqdist_of_mem_primal_argmax {E : Type u} {V : Type v} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] (f : E → EReal) (g : V → EReal) (A : E →ₗ[ℝ] V) (σ : ↑PosReal) (h_problem : IsDualBasedProximalGradientProblem f g A σ) (yBar : V) (xBar : E) (hxBar : xBar ∈ dual_proximal_gradient_primal_x_argmax f A yBar) (x : E) (hx : x ∈ effective_domain f) : ↑(↑σ / 2 * ‖x - xBar‖ ^ 2) ≤ f x - ↑(inner ℝ x ((LinearMap.adjoint A) yBar)) - (f xBar - ↑(inner ℝ xBar ((LinearMap.adjoint A) yBar)))

Helper for Lemma 12.7: the shifted objective inherits the strong-convexity gap (σ / 2) ‖x - xBar‖² ≤ φ(x) - φ(xBar) from f.

theorem primal_minimizer_value_eq_dual_problem_value {E : Type u} {V : Type v} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] (f : E → EReal) (g : V → EReal) (A : E →ₗ[ℝ] V) (σ : ↑PosReal) (h_problem : IsDualBasedProximalGradientProblem f g A σ) (xStar : E) (hxStar : IsMinOn (composite_model_objective f (g ∘ ⇑A)) Set.univ xStar) : composite_model_objective f (g ∘ ⇑A) xStar = dual_based_proximal_gradient_lagrange_dual_problem_value f g A

Helper for Lemma 12.7: the value attained by any primal minimizer is the dual problem value qOpt, by primal attainment plus strong duality.

theorem fenchel_neg_conjugate_le_primal_plus_pairing {E : Type u} {V : Type v} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] (f : E → EReal) (g : V → EReal) (A : E →ₗ[ℝ] V) (σ : ↑PosReal) (h_problem : IsDualBasedProximalGradientProblem f g A σ) (yBar z : V) : -g∗ (-yBar) ≤ g z + ↑(inner ℝ yBar z)

Helper for Lemma 12.7: Fenchel's inequality at (-yBar) gives -(g∗) (-yBar) ≤ g z + ⟪yBar, z⟫.

theorem ereal_add_real_cancel_sub (a b : EReal) (r : ℝ) : a + (↑r + (-↑r - b)) = a - b

Helper for Lemma 12.7: the normalized EReal shape a + (r + (-r - b)) collapses to a - b.

theorem ereal_sub_real_add_real_cancel (a b : EReal) (r : ℝ) : a - ↑r + (b + ↑r) = a + b

Helper for Lemma 12.7: the normalized EReal shape (a - r) + (b + r) collapses to a + b.

theorem dual_objective_ne_top {E : Type u} {V : Type v} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] (f : E → EReal) (g : V → EReal) (A : E →ₗ[ℝ] V) (σ : ↑PosReal) (h_problem : IsDualBasedProximalGradientProblem f g A σ) (yBar : V) : dual_based_proximal_gradient_lagrange_dual_objective_primal f g A yBar ≠ ⊤

Helper for Lemma 12.7: every Chapter 12 primal-space dual objective value avoids ⊤.

theorem half_sigma_sqdist_add_dual_objective_le_primal_value_of_primal_argmax {E : Type u} {V : Type v} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] (f : E → EReal) (g : V → EReal) (A : E →ₗ[ℝ] V) (σ : ↑PosReal) (h_problem : IsDualBasedProximalGradientProblem f g A σ) (yBar : V) (xBar xStar : E) (hxBar : xBar ∈ dual_proximal_gradient_primal_x_argmax f A yBar) (hxStar : IsMinOn (composite_model_objective f (g ∘ ⇑A)) Set.univ xStar) : ↑(↑σ / 2 * ‖xBar - xStar‖ ^ 2) + dual_based_proximal_gradient_lagrange_dual_objective_primal f g A yBar ≤ composite_model_objective f (g ∘ ⇑A) xStar

Helper for Lemma 12.7: the source proof naturally produces the additive inequality (σ / 2) ‖xBar - xStar‖² + q(yBar) ≤ f(xStar) + g(A xStar).

theorem half_sigma_sqdist_le_dual_gap_of_primal_argmax {E : Type u} {V : Type v} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] (f : E → EReal) (g : V → EReal) (A : E →ₗ[ℝ] V) (σ : ↑PosReal) (h_problem : IsDualBasedProximalGradientProblem f g A σ) (yBar : V) (xBar xStar : E) (hxBar : xBar ∈ dual_proximal_gradient_primal_x_argmax f A yBar) (hxStar : IsMinOn (composite_model_objective f (g ∘ ⇑A)) Set.univ xStar) : ↑(↑σ / 2 * ‖xBar - xStar‖ ^ 2) ≤ dual_based_proximal_gradient_lagrange_dual_problem_value f g A - dual_based_proximal_gradient_lagrange_dual_objective_primal f g A yBar

Lemma 12.7: under Assumption 12.1, if xBar belongs to the primal argmax set argmax_x {⟪x, Aᵀ yBar⟫ - f x}, then for every primal optimizer xStar the canonical Chapter 12 dual gap at yBar dominates (σ / 2) ‖xBar - xStar‖². This is the owner-level form of the textbook inequality ‖xBar - xStar‖² ≤ (2 / σ) (q_opt - q(yBar)), stated directly with dual_based_proximal_gradient_lagrange_dual_objective_primal.