theorem helperForCorollary_6_28_1_kuhnTuckerObjective_convexOn_of_multiplier_nonneg {n m r : ℕ} (P : BookOrdinaryConvexProgram n m r) (lambda : Fin m → ℝ) (hlambda_nonneg : ∀ (i : Fin r), 0 ≤ P.inequalityMultipliers lambda i) : ConvexOn ℝ P.constraintSet (P.kuhnTuckerObjective lambda)

Helper for Corollary 6.28.1: nonnegative inequality multipliers preserve convexity of the weighted Kuhn--Tucker objective on the ambient constraint set.

theorem helperForCorollary_6_28_1_closedExtendedKuhnTuckerObjective_of_closedConstraintSet {n m r : ℕ} (P : BookOrdinaryConvexProgram n m r) (lambda : Fin m → ℝ) (hlambda_nonneg : ∀ (i : Fin r), 0 ≤ P.inequalityMultipliers lambda i) (hobjective_closed : LowerSemicontinuous P.objective) (hinequality_closed : ∀ (i : Fin r), LowerSemicontinuous (P.inequalityConstraint i)) (hconstraint_closed : IsClosed P.constraintSet) : ClosedConvexFunction (P.extendedKuhnTuckerObjective lambda)

Helper for Corollary 6.28.1: if the ambient constraint set is closed, then the indicator-extended Kuhn--Tucker objective is a closed convex function on ℝ^n.

theorem helperForCorollary_6_28_1_properExtendedKuhnTuckerObjective_of_multiplier_nonneg {n m r : ℕ} (P : BookOrdinaryConvexProgram n m r) (lambda : Fin m → ℝ) (hlambda_nonneg : ∀ (i : Fin r), 0 ≤ P.inequalityMultipliers lambda i) (hconstraint_nonempty : P.constraintSet.Nonempty) : ProperConvexFunctionOn Set.univ (P.extendedKuhnTuckerObjective lambda)

Helper for Corollary 6.28.1: once the ambient constraint set is known to be nonempty, the indicator-extended Kuhn--Tucker objective is already a proper convex function on ℝ^n.

theorem helperForCorollary_6_28_1_uniqueOptimalSolution_of_closedConstraintSet {n m r : ℕ} (P : BookOrdinaryConvexProgram n m r) (lambda : Fin m → ℝ) (xbar : Fin n → ℝ) (hKT : P.IsKuhnTuckerVector lambda) (hobjective_closed : LowerSemicontinuous P.objective) (hinequality_closed : ∀ (i : Fin r), LowerSemicontinuous (P.inequalityConstraint i)) (hequality_closed : ∀ (i : Fin (m - r)), LowerSemicontinuous (P.equalityConstraint i)) (hconstraint_closed : IsClosed P.constraintSet) (hxbar_min : ∀ (y : Fin n → ℝ), P.extendedKuhnTuckerObjective lambda xbar ≤ P.extendedKuhnTuckerObjective lambda y) (hunique : ∀ (y : Fin n → ℝ), (∀ (z : Fin n → ℝ), P.extendedKuhnTuckerObjective lambda y ≤ P.extendedKuhnTuckerObjective lambda z) → y = xbar) : P.IsOptimalSolution xbar ∧ ∀ (y : Fin n → ℝ), P.IsOptimalSolution y → y = xbar

Helper for Corollary 6.28.1: once the ambient constraint set is closed, the existing closed/proper bridge proves that the unique minimizer of the indicator-extended Kuhn--Tucker objective is the unique optimal solution of the program.

theorem helperForCorollary_6_28_1_existsOptimalSolution_of_closedConstraintSet {n m r : ℕ} (P : BookOrdinaryConvexProgram n m r) (lambda : Fin m → ℝ) (xbar : Fin n → ℝ) (hKT : P.IsKuhnTuckerVector lambda) (hobjective_closed : LowerSemicontinuous P.objective) (hinequality_closed : ∀ (i : Fin r), LowerSemicontinuous (P.inequalityConstraint i)) (hequality_closed : ∀ (i : Fin (m - r)), LowerSemicontinuous (P.equalityConstraint i)) (hconstraint_closed : IsClosed P.constraintSet) (hxbar_min : ∀ (y : Fin n → ℝ), P.extendedKuhnTuckerObjective lambda xbar ≤ P.extendedKuhnTuckerObjective lambda y) (hunique : ∀ (y : Fin n → ℝ), (∀ (z : Fin n → ℝ), P.extendedKuhnTuckerObjective lambda y ≤ P.extendedKuhnTuckerObjective lambda z) → y = xbar) : ∃ (y : Fin n → ℝ), P.IsOptimalSolution y

Helper for Corollary 6.28.1: once the ambient constraint set is closed, the unique minimizer xbar supplied by the corollary is already an explicit optimal-solution witness.

theorem helperForCorollary_6_28_1_isOptimalSolution_of_existsOptimalSolution {n m r : ℕ} (P : BookOrdinaryConvexProgram n m r) (lambda : Fin m → ℝ) (xbar : Fin n → ℝ) (hKT : P.IsKuhnTuckerVector lambda) (hunique : ∀ (y : Fin n → ℝ), (∀ (z : Fin n → ℝ), P.extendedKuhnTuckerObjective lambda y ≤ P.extendedKuhnTuckerObjective lambda z) → y = xbar) : (∃ (y : Fin n → ℝ), P.IsOptimalSolution y) → P.IsOptimalSolution xbar

Helper for Corollary 6.28.1: once some optimal solution exists, Theorem 6.28.1 already identifies that witness with the unique global minimizer xbar, so xbar is optimal.

theorem helperForCorollary_6_28_1_uniqueOptimalSolution_of_existsOptimalSolution {n m r : ℕ} (P : BookOrdinaryConvexProgram n m r) (lambda : Fin m → ℝ) (xbar : Fin n → ℝ) (hKT : P.IsKuhnTuckerVector lambda) (hunique : ∀ (y : Fin n → ℝ), (∀ (z : Fin n → ℝ), P.extendedKuhnTuckerObjective lambda y ≤ P.extendedKuhnTuckerObjective lambda z) → y = xbar) : (∃ (y : Fin n → ℝ), P.IsOptimalSolution y) → P.IsOptimalSolution xbar ∧ ∀ (y : Fin n → ℝ), P.IsOptimalSolution y → y = xbar

Helper for Corollary 6.28.1: once some optimal solution of (P) is known to exist, Theorem 6.28.1 and uniqueness of the global minimizer already force that optimal solution to equal xbar, so xbar is itself the unique optimal solution.

theorem helperForCorollary_6_28_1_isOptimalSolution_of_feasible_objective_eq_optimalValue {n m r : ℕ} (P : BookOrdinaryConvexProgram n m r) {y : Fin n → ℝ} (hyFeasible : y ∈ P.feasibleSet) (hyValue : ↑(P.objective y) = P.optimalValue) : P.IsOptimalSolution y

Helper for Corollary 6.28.1: a feasible point whose objective value realizes P.optimalValue is already an optimal solution.

theorem helperForCorollary_6_28_1_objective_eq_optimalValue_of_isOptimalSolution {n m r : ℕ} (P : BookOrdinaryConvexProgram n m r) {y : Fin n → ℝ} (hyOptimal : P.IsOptimalSolution y) : ↑(P.objective y) = P.optimalValue

Helper for Corollary 6.28.1: every optimal solution attains the primal optimal value.

theorem helperForCorollary_6_28_1_exists_feasible_objective_eq_optimalValue_of_existsOptimalSolution {n m r : ℕ} (P : BookOrdinaryConvexProgram n m r) : (∃ (y : Fin n → ℝ), P.IsOptimalSolution y) → ∃ y ∈ P.feasibleSet, ↑(P.objective y) = P.optimalValue

Helper for Corollary 6.28.1: an existing optimal solution can be repackaged as a feasible point whose objective realizes P.optimalValue.

theorem helperForCorollary_6_28_1_existsOptimalSolution_iff_exists_feasible_objective_eq_optimalValue {n m r : ℕ} (P : BookOrdinaryConvexProgram n m r) : (∃ (y : Fin n → ℝ), P.IsOptimalSolution y) ↔ ∃ y ∈ P.feasibleSet, ↑(P.objective y) = P.optimalValue

Helper for Corollary 6.28.1: primal optimal-solution existence is equivalent to the attainment of P.optimalValue by some feasible point.

theorem helperForCorollary_6_28_1_exists_feasible_objective_eq_optimalValue_of_closedConstraintSet {n m r : ℕ} (P : BookOrdinaryConvexProgram n m r) (lambda : Fin m → ℝ) (xbar : Fin n → ℝ) (hKT : P.IsKuhnTuckerVector lambda) (hobjective_closed : LowerSemicontinuous P.objective) (hinequality_closed : ∀ (i : Fin r), LowerSemicontinuous (P.inequalityConstraint i)) (hequality_closed : ∀ (i : Fin (m - r)), LowerSemicontinuous (P.equalityConstraint i)) (hconstraint_closed : IsClosed P.constraintSet) (hxbar_min : ∀ (y : Fin n → ℝ), P.extendedKuhnTuckerObjective lambda xbar ≤ P.extendedKuhnTuckerObjective lambda y) (hunique : ∀ (y : Fin n → ℝ), (∀ (z : Fin n → ℝ), P.extendedKuhnTuckerObjective lambda y ≤ P.extendedKuhnTuckerObjective lambda z) → y = xbar) : ∃ y ∈ P.feasibleSet, ↑(P.objective y) = P.optimalValue

Helper for Corollary 6.28.1: whenever the closed-constraint-set route is available, the distinguished minimizer xbar yields the feasible primal value-attainer needed by the local endgame.

theorem helperForCorollary_6_28_1_uniqueOptimalSolution_of_exists_feasible_objective_eq_optimalValue {n m r : ℕ} (P : BookOrdinaryConvexProgram n m r) (lambda : Fin m → ℝ) (xbar : Fin n → ℝ) (hKT : P.IsKuhnTuckerVector lambda) (hunique : ∀ (y : Fin n → ℝ), (∀ (z : Fin n → ℝ), P.extendedKuhnTuckerObjective lambda y ≤ P.extendedKuhnTuckerObjective lambda z) → y = xbar) : (∃ y ∈ P.feasibleSet, ↑(P.objective y) = P.optimalValue) → P.IsOptimalSolution xbar ∧ ∀ (y : Fin n → ℝ), P.IsOptimalSolution y → y = xbar

Helper for Corollary 6.28.1: once a feasible point attains P.optimalValue, the earlier optimal-witness helper identifies that point with the unique minimizer xbar.

theorem helperForCorollary_6_28_1_xbar_feasible_objective_eq_optimalValue_of_exists_feasible_objective_eq_optimalValue {n m r : ℕ} (P : BookOrdinaryConvexProgram n m r) (lambda : Fin m → ℝ) (xbar : Fin n → ℝ) (hKT : P.IsKuhnTuckerVector lambda) (hunique : ∀ (y : Fin n → ℝ), (∀ (z : Fin n → ℝ), P.extendedKuhnTuckerObjective lambda y ≤ P.extendedKuhnTuckerObjective lambda z) → y = xbar) : (∃ y ∈ P.feasibleSet, ↑(P.objective y) = P.optimalValue) → xbar ∈ P.feasibleSet ∧ ↑(P.objective xbar) = P.optimalValue

Helper for Corollary 6.28.1: once some feasible point realizes P.optimalValue, the unique global minimizer xbar itself becomes a feasible value-attainer.

theorem helperForCorollary_6_28_1_uniqueOptimalSolution_iff_exists_feasible_objective_eq_optimalValue {n m r : ℕ} (P : BookOrdinaryConvexProgram n m r) (lambda : Fin m → ℝ) (xbar : Fin n → ℝ) (hKT : P.IsKuhnTuckerVector lambda) (hunique : ∀ (y : Fin n → ℝ), (∀ (z : Fin n → ℝ), P.extendedKuhnTuckerObjective lambda y ≤ P.extendedKuhnTuckerObjective lambda z) → y = xbar) : (P.IsOptimalSolution xbar ∧ ∀ (y : Fin n → ℝ), P.IsOptimalSolution y → y = xbar) ↔ ∃ y ∈ P.feasibleSet, ↑(P.objective y) = P.optimalValue

Helper for Corollary 6.28.1: under the unique-minimizer hypothesis, the corollary conclusion is equivalent to the existence of a feasible point attaining P.optimalValue.

theorem helperForCorollary_6_28_1_xbar_mem_constraintSet_and_extendedObjective_eq_optimalValue {n m r : ℕ} (P : BookOrdinaryConvexProgram n m r) (lambda : Fin m → ℝ) (xbar : Fin n → ℝ) (hKT : P.IsKuhnTuckerVector lambda) (hxbar_min : ∀ (y : Fin n → ℝ), P.extendedKuhnTuckerObjective lambda xbar ≤ P.extendedKuhnTuckerObjective lambda y) : xbar ∈ P.constraintSet ∧ P.extendedKuhnTuckerObjective lambda xbar = P.optimalValue

Helper for Corollary 6.28.1: the global minimizer xbar already lies in the ambient constraint set and attains the common extended Kuhn--Tucker value P.optimalValue.

theorem helperForCorollary_6_28_1_feasible_objective_eq_optimalValue_of_tendsto_nearOptimal_feasibleSequence {n m r : ℕ} (P : BookOrdinaryConvexProgram n m r) (xbar : Fin n → ℝ) {v : ℝ} (hobjective_closed : LowerSemicontinuous P.objective) (hinequality_closed : ∀ (i : Fin r), LowerSemicontinuous (P.inequalityConstraint i)) (hxbarC : xbar ∈ P.constraintSet) (hopt : P.optimalValue = ↑v) (xSeq : ℕ → Fin n → ℝ) (hxSeqFeas : ∀ (k : ℕ), xSeq k ∈ P.feasibleSet) (hxSeqNear : ∀ (k : ℕ), P.objective (xSeq k) ≤ v + 1 / (↑k + 1)) (hxSeq_tendsto : Filter.Tendsto xSeq Filter.atTop (nhds xbar)) : xbar ∈ P.feasibleSet ∧ ↑(P.objective xbar) = P.optimalValue

Helper for Corollary 6.28.1: once a near-optimal feasible sequence converges to a point already known to lie in the ambient constraint set, the closed-data hypotheses force that limit point to be a feasible point attaining P.optimalValue.

theorem helperForCorollary_6_28_1_exists_convergentNearOptimal_feasibleSequence_of_xbar_feasible_objective_eq_optimalValue {n m r : ℕ} (P : BookOrdinaryConvexProgram n m r) (xbar : Fin n → ℝ) {v : ℝ} (hopt : P.optimalValue = ↑v) (hxbarFeasible : xbar ∈ P.feasibleSet) (hxbarValue : ↑(P.objective xbar) = P.optimalValue) : ∃ (xSeq : ℕ → Fin n → ℝ), (∀ (k : ℕ), xSeq k ∈ P.feasibleSet) ∧ (∀ (k : ℕ), P.objective (xSeq k) ≤ v + 1 / (↑k + 1)) ∧ Filter.Tendsto xSeq Filter.atTop (nhds xbar)

Helper for Corollary 6.28.1: once xbar itself is already known to be feasible and to realize P.optimalValue, the required convergent near-optimal feasible sequence is the constant sequence at xbar.

theorem helperForCorollary_6_28_1_exists_convergentNearOptimal_feasibleSequence_iff_xbar_feasible_objective_eq_optimalValue {n m r : ℕ} (P : BookOrdinaryConvexProgram n m r) (xbar : Fin n → ℝ) {v : ℝ} (hobjective_closed : LowerSemicontinuous P.objective) (hinequality_closed : ∀ (i : Fin r), LowerSemicontinuous (P.inequalityConstraint i)) (hxbarC : xbar ∈ P.constraintSet) (hopt : P.optimalValue = ↑v) : (∃ (xSeq : ℕ → Fin n → ℝ), (∀ (k : ℕ), xSeq k ∈ P.feasibleSet) ∧ (∀ (k : ℕ), P.objective (xSeq k) ≤ v + 1 / (↑k + 1)) ∧ Filter.Tendsto xSeq Filter.atTop (nhds xbar)) ↔ xbar ∈ P.feasibleSet ∧ ↑(P.objective xbar) = P.optimalValue

Helper for Corollary 6.28.1: under the closed-data limit argument already proved above, asking for a convergent near-optimal feasible sequence is equivalent to asking directly that xbar be feasible and attain P.optimalValue.

theorem helperForCorollary_6_28_1_xbar_feasible_objective_eq_optimalValue_of_uniqueOptimalSolution {n m r : ℕ} (P : BookOrdinaryConvexProgram n m r) (xbar : Fin n → ℝ) (hxbarUnique : P.IsOptimalSolution xbar ∧ ∀ (y : Fin n → ℝ), P.IsOptimalSolution y → y = xbar) : xbar ∈ P.feasibleSet ∧ ↑(P.objective xbar) = P.optimalValue

Helper for Corollary 6.28.1: once the corollary conclusion itself is known, xbar is already feasible and its objective value realizes P.optimalValue.

theorem helperForCorollary_6_28_1_exists_convergentNearOptimal_feasibleSequence_of_uniqueOptimalSolution {n m r : ℕ} (P : BookOrdinaryConvexProgram n m r) (xbar : Fin n → ℝ) {v : ℝ} (hopt : P.optimalValue = ↑v) (hxbarUnique : P.IsOptimalSolution xbar ∧ ∀ (y : Fin n → ℝ), P.IsOptimalSolution y → y = xbar) : ∃ (xSeq : ℕ → Fin n → ℝ), (∀ (k : ℕ), xSeq k ∈ P.feasibleSet) ∧ (∀ (k : ℕ), P.objective (xSeq k) ≤ v + 1 / (↑k + 1)) ∧ Filter.Tendsto xSeq Filter.atTop (nhds xbar)

Helper for Corollary 6.28.1: if the corollary conclusion is already known, the constant sequence at xbar is a convergent near-optimal feasible sequence.

theorem helperForCorollary_6_28_1_xbar_feasible_objective_eq_optimalValue_of_closedData {n m r : ℕ} (P : BookOrdinaryConvexProgram n m r) (lambda : Fin m → ℝ) (xbar : Fin n → ℝ) (hKT : P.IsKuhnTuckerVector lambda) (hobjective_closed : LowerSemicontinuous P.objective) (hinequality_closed : ∀ (i : Fin r), LowerSemicontinuous (P.inequalityConstraint i)) (hequality_closed : ∀ (i : Fin (m - r)), LowerSemicontinuous (P.equalityConstraint i)) (hconstraint_closed : IsClosed P.constraintSet) (hxbar_min : ∀ (y : Fin n → ℝ), P.extendedKuhnTuckerObjective lambda xbar ≤ P.extendedKuhnTuckerObjective lambda y) (hunique : ∀ (y : Fin n → ℝ), (∀ (z : Fin n → ℝ), P.extendedKuhnTuckerObjective lambda y ≤ P.extendedKuhnTuckerObjective lambda z) → y = xbar) : xbar ∈ P.feasibleSet ∧ ↑(P.objective xbar) = P.optimalValue

Helper for Corollary 6.28.1: the remaining closed-data bridge can be stated directly as feasibility of xbar together with equality of its objective value and P.optimalValue.

theorem helperForCorollary_6_28_1_uniqueOptimalSolution_of_xbar_feasible_objective_eq_optimalValue {n m r : ℕ} (P : BookOrdinaryConvexProgram n m r) (lambda : Fin m → ℝ) (xbar : Fin n → ℝ) (hKT : P.IsKuhnTuckerVector lambda) (hunique : ∀ (y : Fin n → ℝ), (∀ (z : Fin n → ℝ), P.extendedKuhnTuckerObjective lambda y ≤ P.extendedKuhnTuckerObjective lambda z) → y = xbar) (hxbarFeasible : xbar ∈ P.feasibleSet) (hxbarValue : ↑(P.objective xbar) = P.optimalValue) : P.IsOptimalSolution xbar ∧ ∀ (y : Fin n → ℝ), P.IsOptimalSolution y → y = xbar

Helper for Corollary 6.28.1: once xbar itself is known to be feasible and to realize P.optimalValue, the corollary conclusion follows from the existing optimality and uniqueness bridges.

theorem helperForCorollary_6_28_1_isOptimalSolution_of_closedData {n m r : ℕ} (P : BookOrdinaryConvexProgram n m r) (lambda : Fin m → ℝ) (xbar : Fin n → ℝ) (hKT : P.IsKuhnTuckerVector lambda) (hobjective_closed : LowerSemicontinuous P.objective) (hinequality_closed : ∀ (i : Fin r), LowerSemicontinuous (P.inequalityConstraint i)) (hequality_closed : ∀ (i : Fin (m - r)), LowerSemicontinuous (P.equalityConstraint i)) (hconstraint_closed : IsClosed P.constraintSet) (hxbar_min : ∀ (y : Fin n → ℝ), P.extendedKuhnTuckerObjective lambda xbar ≤ P.extendedKuhnTuckerObjective lambda y) (hunique : ∀ (y : Fin n → ℝ), (∀ (z : Fin n → ℝ), P.extendedKuhnTuckerObjective lambda y ≤ P.extendedKuhnTuckerObjective lambda z) → y = xbar) : P.IsOptimalSolution xbar

Helper for Corollary 6.28.1: the closed-data hypotheses already force the unique minimizer xbar to be an optimal solution of the primal problem.