theorem helperForCorollary_6_30_5_exists_dualKuhnTucker_of_primalConsistency_and_strongDualConsistency {m n : ℕ} (F : { F : (Fin m → ℝ) → (Fin n → ℝ) → EReal // ClosedConvexBifunction F }) (hP : IsConsistentConvexProgram ⟨↑F, ⋯⟩) (hPStarStrong : IsStronglyConsistentDualProgramOfConvexProgram ⟨↑F, ⋯⟩) : ∃ (x : Fin n → ℝ), IsKuhnTuckerVectorForDualProgram ⟨↑F, ⋯⟩ x

Helper for Corollary 6.30.5: primal consistency together with strong dual consistency yields a Chapter 30 dual Kuhn--Tucker vector by applying Corollary 6.29.4 to the generalized program with perturbation x* ↦ - sup_{u*} F*(x*, u*).

theorem helperForCorollary_6_30_5_exists_dualOptimalSolution_of_strongPrimalConsistency {m n : ℕ} (F : { F : (Fin m → ℝ) → (Fin n → ℝ) → EReal // ClosedConvexBifunction F }) (hPStrong : IsStronglyConsistentConvexProgram ⟨↑F, ⋯⟩) (hPStar : IsConsistentDualProgramOfConvexProgram ⟨↑F, ⋯⟩) : ∃ (uStar : Fin m → ℝ), uStar ∈ dualOptimalSolutionSetOfConvexProgram ⟨↑F, ⋯⟩

Helper for Corollary 6.30.5: strong primal consistency together with dual consistency yields a dual optimal solution through a generalized Kuhn--Tucker witness for F.

theorem consistent_and_stronglyConsistent_primal_dual_programs_have_optimalSolutions {m n : ℕ} (F : { F : (Fin m → ℝ) → (Fin n → ℝ) → EReal // ClosedConvexBifunction F }) : (IsConsistentConvexProgram ⟨↑F, ⋯⟩ → IsStronglyConsistentDualProgramOfConvexProgram ⟨↑F, ⋯⟩ → ∃ (x : Fin n → ℝ), x ∈ primalOptimalSolutionSetOfConvexProgram ⟨↑F, ⋯⟩) ∧ (IsStronglyConsistentConvexProgram ⟨↑F, ⋯⟩ → IsConsistentDualProgramOfConvexProgram ⟨↑F, ⋯⟩ → ∃ (uStar : Fin m → ℝ), uStar ∈ dualOptimalSolutionSetOfConvexProgram ⟨↑F, ⋯⟩)

Corollary 6.30.5 (Corollary 30.5.2): let F be a closed convex bifunction from ℝ^m to ℝ^n, and let (P) be the convex program associated with F. If (P) is consistent and (P*) is strongly consistent, then (P) has an optimal solution. Dually, if (P) is strongly consistent and (P*) is consistent, then (P*) has an optimal solution.

def ordinaryConvexProgramFeasibleSet {m n : ℕ} (f : Fin m → (Fin n → ℝ) → EReal) (u : Fin m → ℝ) : Set (Fin n → ℝ)

The feasible set of the perturbed ordinary convex program with perturbation vector u.

noncomputable def ordinaryConvexProgramBifunction {m n : ℕ} (f0 : (Fin n → ℝ) → EReal) (f : Fin m → (Fin n → ℝ) → EReal) : (Fin m → ℝ) → (Fin n → ℝ) → EReal

The convex bifunction associated with an ordinary convex program: F_u(x) = f₀(x) on the constraint set fᵢ(x) ≤ uᵢ and +∞ outside it.

noncomputable def ordinaryConvexProgramWeightedObjective {m n : ℕ} (f0 : (Fin n → ℝ) → EReal) (f : Fin m → (Fin n → ℝ) → EReal) (uStar : Fin m → ℝ) : (Fin n → ℝ) → EReal

The weighted objective x ↦ f₀(x) + ∑ᵢ uᵢ* fᵢ(x) appearing in the adjoint formula for an ordinary convex program.

theorem helperForTheorem_6_30_20_coe_sum_mul_eq_sum_coe_mul {m : ℕ} (a b : Fin m → ℝ) : ∑ i : Fin m, ↑(a i) * ↑(b i) = ↑(∑ i : Fin m, a i * b i)

Helper for Theorem 6.30.20: coercion from ℝ to EReal commutes with finite sums of coordinatewise products.

theorem helperForTheorem_6_30_20_dotProduct_ge_weightedSum_of_feasible {m n : ℕ} (f : Fin m → (Fin n → ℝ) → EReal) (uStar : Fin m → ℝ) (hnonneg : ∀ (i : Fin m), 0 ≤ uStar i) {u : Fin m → ℝ} {x : Fin n → ℝ} (hx : x ∈ ordinaryConvexProgramFeasibleSet f u) : ∑ i : Fin m, ↑(uStar i) * f i x ≤ ↑(u ⬝ᵥ uStar)

Helper for Theorem 6.30.20: for a feasible pair (u, x) and nonnegative multipliers u*, the weighted constraint sum is bounded above by ⟪u, u*⟫.

theorem helperForTheorem_6_30_20_exists_feasible_u_of_finite_constraints {m n : ℕ} (f : Fin m → (Fin n → ℝ) → EReal) (hf : ∀ (i : Fin m), ProperConvexERealFunction (f i)) (uStar : Fin m → ℝ) (x : Fin n → ℝ) (hfinite : ∀ (i : Fin m), f i x ≠ ⊤) : ∃ (uX : Fin m → ℝ), x ∈ ordinaryConvexProgramFeasibleSet f uX ∧ ↑(uX ⬝ᵥ uStar) = ∑ i : Fin m, ↑(uStar i) * f i x

Helper for Theorem 6.30.20: if each fᵢ(x) is finite above (≠ ⊤), one can choose a feasible perturbation vector u with coordinates uᵢ = (fᵢ(x)).toReal, and this choice realizes ⟪u, u*⟫ = ∑ᵢ uᵢ* fᵢ(x) in EReal.

theorem helperForTheorem_6_30_20_exists_feasible_u_achieving_weightedSum {m n : ℕ} (C : Set (Fin n → ℝ)) (f0 : (Fin n → ℝ) → EReal) (f : Fin m → (Fin n → ℝ) → EReal) (hf0 : ProperConvexERealFunction f0) (hf : ∀ (i : Fin m), ProperConvexERealFunction (f i)) (hdom_f0 : effectiveDomain Set.univ f0 = C) (hdom_f : ∀ (i : Fin m), C ⊆ effectiveDomain Set.univ (f i)) (uStar : Fin m → ℝ) (x : Fin n → ℝ) (hx0 : f0 x ≠ ⊤) : ∃ (uX : Fin m → ℝ), x ∈ ordinaryConvexProgramFeasibleSet f uX ∧ ↑(uX ⬝ᵥ uStar) = ∑ i : Fin m, ↑(uStar i) * f i x

Helper for Theorem 6.30.20: if f₀(x) is finite above (≠ ⊤), the standing domain assumptions imply each fᵢ(x) is finite above, hence there exists a feasible perturbation vector realizing ⟪u, u*⟫ = ∑ᵢ uᵢ* fᵢ(x).

theorem helperForTheorem_6_30_20_sInf_range_weightedObjective_sub_dot_eq_neg_fenchelConjugate {m n : ℕ} (f0 : (Fin n → ℝ) → EReal) (f : Fin m → (Fin n → ℝ) → EReal) (uStar : Fin m → ℝ) (xStar : Fin n → ℝ) : sInf (Set.range fun (x : Fin n → ℝ) => ordinaryConvexProgramWeightedObjective f0 f uStar x - ↑(x ⬝ᵥ xStar)) = -fenchelConjugate n (ordinaryConvexProgramWeightedObjective f0 f uStar) xStar

Helper for Theorem 6.30.20: the infimum of x ↦ ordinaryConvexProgramWeightedObjective f₀ f u*(x) - ⟪x, x*⟫ equals the negative Fenchel conjugate of the weighted objective at x*.

theorem helperForTheorem_6_30_20_sInf_range_weightedObjective_sub_dot_le_adjoint_of_nonnegative {m n : ℕ} (f0 : (Fin n → ℝ) → EReal) (f : Fin m → (Fin n → ℝ) → EReal) (F : { F : (Fin m → ℝ) → (Fin n → ℝ) → EReal // ConvexBifunction F }) (hF : ↑F = ordinaryConvexProgramBifunction f0 f) (hf0 : ProperConvexERealFunction f0) (uStar : Fin m → ℝ) (xStar : Fin n → ℝ) (hnonneg : ∀ (i : Fin m), 0 ≤ uStar i) : sInf (Set.range fun (x : Fin n → ℝ) => ordinaryConvexProgramWeightedObjective f0 f uStar x - ↑(x ⬝ᵥ xStar)) ≤ adjointOfConvexBifunction F xStar uStar

Helper for Theorem 6.30.20: in the nonnegative-multiplier branch, every adjoint-integrand value dominates the x-only integrand, so sInf_x (weightedObjective - ⟪x, x*⟫) ≤ adjointOfConvexBifunction F x* u*.

theorem helperForTheorem_6_30_20_adjoint_le_sInf_range_weightedObjective_sub_dot_of_nonnegative {m n : ℕ} (C : Set (Fin n → ℝ)) (f0 : (Fin n → ℝ) → EReal) (f : Fin m → (Fin n → ℝ) → EReal) (F : { F : (Fin m → ℝ) → (Fin n → ℝ) → EReal // ConvexBifunction F }) (hF : ↑F = ordinaryConvexProgramBifunction f0 f) (hf0 : ProperConvexERealFunction f0) (hf : ∀ (i : Fin m), ProperConvexERealFunction (f i)) (hdom_f0 : effectiveDomain Set.univ f0 = C) (hdom_f : ∀ (i : Fin m), C ⊆ effectiveDomain Set.univ (f i)) (uStar : Fin m → ℝ) (xStar : Fin n → ℝ) (hnonneg : ∀ (i : Fin m), 0 ≤ uStar i) : adjointOfConvexBifunction F xStar uStar ≤ sInf (Set.range fun (x : Fin n → ℝ) => ordinaryConvexProgramWeightedObjective f0 f uStar x - ↑(x ⬝ᵥ xStar))

Helper for Theorem 6.30.20: in the nonnegative-multiplier branch, for every fixed x, one can produce an adjoint witness matching the value weightedObjective(x) - ⟪x, x*⟫, hence adjointOfConvexBifunction F x* u* ≤ sInf_x (weightedObjective - ⟪x, x*⟫).

theorem helperForTheorem_6_30_20_negativeMultiplierRayWitnessValue {m n : ℕ} (f0 : (Fin n → ℝ) → EReal) (f : Fin m → (Fin n → ℝ) → EReal) (xStar : Fin n → ℝ) (uStar u0 : Fin m → ℝ) (x0 : Fin n → ℝ) (hu0Feas : x0 ∈ ordinaryConvexProgramFeasibleSet f u0) (i0 : Fin m) (t : ℝ) (ht : 0 ≤ t) : have u := u0 + Pi.single i0 t; ordinaryConvexProgramBifunction f0 f u x0 - ↑(x0 ⬝ᵥ xStar) + ↑(u ⬝ᵥ uStar) = f0 x0 - ↑(x0 ⬝ᵥ xStar) + ↑(u0 ⬝ᵥ uStar) + ↑(t * uStar i0)

Helper for Theorem 6.30.20: along the feasible ray u(t) = u₀ + t e_{i₀} at fixed x₀, the adjoint integrand is affine in t with slope u* i₀.

theorem helperForTheorem_6_30_20_adjoint_eq_bot_of_exists_negativeMultiplier {m n : ℕ} (C : Set (Fin n → ℝ)) (f0 : (Fin n → ℝ) → EReal) (f : Fin m → (Fin n → ℝ) → EReal) (F : { F : (Fin m → ℝ) → (Fin n → ℝ) → EReal // ConvexBifunction F }) (hF : ↑F = ordinaryConvexProgramBifunction f0 f) (hf0 : ProperConvexERealFunction f0) (hf : ∀ (i : Fin m), ProperConvexERealFunction (f i)) (hdom_f0 : effectiveDomain Set.univ f0 = C) (hdom_f : ∀ (i : Fin m), C ⊆ effectiveDomain Set.univ (f i)) (uStar : Fin m → ℝ) (xStar : Fin n → ℝ) (hneg : ∃ (i0 : Fin m), uStar i0 < 0) : adjointOfConvexBifunction F xStar uStar = ⊥

Helper for Theorem 6.30.20: if one multiplier coordinate is negative, the adjoint value is -∞ (by sending that perturbation coordinate to +∞ along a feasible ray).

theorem adjointOfOrdinaryConvexProgramBifunction_eq_neg_fenchelConjugate_weightedObjective {m n : ℕ} (C : Set (Fin n → ℝ)) (f0 : (Fin n → ℝ) → EReal) (f : Fin m → (Fin n → ℝ) → EReal) (F : { F : (Fin m → ℝ) → (Fin n → ℝ) → EReal // ConvexBifunction F }) (hF : ↑F = ordinaryConvexProgramBifunction f0 f) (hf0 : ProperConvexERealFunction f0) (hf : ∀ (i : Fin m), ProperConvexERealFunction (f i)) (hdom_f0 : effectiveDomain Set.univ f0 = C) (hdom_f : ∀ (i : Fin m), C ⊆ effectiveDomain Set.univ (f i)) (hri_f : ∀ (i : Fin m), euclideanRelativeInterior_fin n C ⊆ euclideanRelativeInterior_fin n (effectiveDomain Set.univ (f i))) (uStar : Fin m → ℝ) (xStar : Fin n → ℝ) : adjointOfConvexBifunction F xStar uStar = if ∀ (i : Fin m), 0 ≤ uStar i then -fenchelConjugate n (ordinaryConvexProgramWeightedObjective f0 f uStar) xStar else ⊥

Theorem 6.30.20: for the ordinary convex program min_x f₀(x) subject to fᵢ(x) ≤ 0, where f₀, …, f_m are proper convex and dom f₀ = C, C ⊆ dom fᵢ, ri C ⊆ ri (dom fᵢ), let F be the associated convex bifunction F_u(x) = f₀(x) + δ(x | fᵢ(x) ≤ uᵢ). Then the adjoint satisfies F*(x*, u*) = -(f₀ + ∑ᵢ uᵢ* fᵢ)^*(x*) for u* ≥ 0, and F*(x*, u*) = -∞ otherwise.