theorem PrimalEqualityConstrainedProblem.LagrangianMinimizerSelection.isMinOn_feasibleSet_of_dualResidual_eq_zero {E : Type u} {Λ : Type v} [AddCommMonoid E] [Module ℝ E] [NormedAddCommGroup Λ] [InnerProductSpace ℝ Λ] {problem : PrimalEqualityConstrainedProblem E Λ} (selection : problem.LagrangianMinimizerSelection) {uStar : Λ} (hresidual : selection.dualResidual uStar = 0) : ↑(selection uStar) ∈ problem.equalityFeasibleSet ∧ IsMinOn problem.objective problem.equalityFeasibleSet ↑(selection uStar)

The owner-facing core of Proposition 2.20: if the selected dual residual vanishes at uStar, then the selected minimizer is feasible and minimizes the primal objective on the feasible set.

theorem PrimalEqualityConstrainedProblem.LagrangianMinimizerSelection.selectedDualProfile_eq_objective_of_mem_feasibleSet {E : Type u} {Λ : Type v} [AddCommMonoid E] [Module ℝ E] [NormedAddCommGroup Λ] [InnerProductSpace ℝ Λ] {problem : PrimalEqualityConstrainedProblem E Λ} (selection : problem.LagrangianMinimizerSelection) {u : Λ} (hfeasible : ↑(selection u) ∈ problem.equalityFeasibleSet) : selection.selectedDualProfile u = problem.objective ↑(selection u)

At a feasible selected minimizer, the equality-constraint term in the selected dual profile vanishes, so the selected dual profile equals the primal objective.

theorem PrimalEqualityConstrainedProblem.LagrangianMinimizerSelection.isMinOn_feasibleSet_of_dualOptimal {E : Type u} {Λ : Type v} [AddCommMonoid E] [Module ℝ E] [NormedAddCommGroup Λ] [InnerProductSpace ℝ Λ] {problem : PrimalEqualityConstrainedProblem E Λ} (selection : problem.LagrangianMinimizerSelection) [CompleteSpace Λ] {uStar : Λ} (huStar : IsMaxOn selection.selectedDualProfile Set.univ uStar) (hprofile_grad : HasGradientAt selection.selectedDualProfile (selection.dualResidual uStar) uStar) : ↑(selection uStar) ∈ problem.equalityFeasibleSet ∧ IsMinOn problem.objective problem.equalityFeasibleSet ↑(selection uStar)

Proposition 2.20 in textbook form: if the canonical selected dual profile selection.selectedDualProfile is maximized at uStar and has gradient there equal to the dual residual, then the selected minimizer at uStar solves the primal problem.

theorem PrimalEqualityConstrainedProblem.LagrangianMinimizerSelection.isMinOn_feasibleSet_of_dualOptimal_of_gradient_eq_dualResidual {E : Type u} {Λ : Type v} [AddCommMonoid E] [Module ℝ E] [NormedAddCommGroup Λ] [InnerProductSpace ℝ Λ] {problem : PrimalEqualityConstrainedProblem E Λ} (selection : problem.LagrangianMinimizerSelection) [CompleteSpace Λ] {uStar : Λ} (huStar : IsMaxOn selection.selectedDualProfile Set.univ uStar) (hprofile_diff : DifferentiableAt ℝ selection.selectedDualProfile uStar) (hprofile_grad : gradient selection.selectedDualProfile uStar = selection.dualResidual uStar) : ↑(selection uStar) ∈ problem.equalityFeasibleSet ∧ IsMinOn problem.objective problem.equalityFeasibleSet ↑(selection uStar)

Companion reformulation of Proposition 2.20 using mathlib's total gradient at the single point uStar: differentiability at uStar upgrades the pointwise identity ∇ φ(uStar) = selection.dualResidual uStar to the HasGradientAt hypothesis used by the main theorem.

theorem PrimalEqualityConstrainedProblem.LagrangianMinimizerSelection.primalOptimalValue_eq_dualFunction_eq_objective_of_isMinOn_feasibleSet {E : Type u} {Λ : Type v} [AddCommMonoid E] [Module ℝ E] [NormedAddCommGroup Λ] [InnerProductSpace ℝ Λ] {problem : PrimalEqualityConstrainedProblem E Λ} (selection : problem.LagrangianMinimizerSelection) {uStar : Λ} (hoptimal : ↑(selection uStar) ∈ problem.equalityFeasibleSet ∧ IsMinOn problem.objective problem.equalityFeasibleSet ↑(selection uStar)) : problem.primalOptimalValue = problem.dualFunction uStar ∧ problem.dualFunction uStar = ↑(problem.objective ↑(selection uStar))

Once the selected point is known to minimize the primal problem, strong duality identifies the primal optimal value with the dual value and the recovered primal objective value.