theorem helperForTheorem_6_30_17_polyhedralDual_implies_polyhedralPrimal_of_globalProperness {m n : ℕ} (F : { F : (Fin m → ℝ) → (Fin n → ℝ) → EReal // ClosedConvexBifunction F }) (hProper : ProperConvexBifunction ↑F) (hPolyDual : PolyhedralConcaveBifunction (adjointOfConvexBifunction ⟨↑F, ⋯⟩)) : PolyhedralConvexBifunction ↑F

Helper for Theorem 6.30.17: under global properness, polyhedrality of the dual adjoint transports back across the biadjoint correspondence to polyhedrality of the original primal bifunction.

theorem helperForTheorem_6_30_17_dualKuhnTucker_of_polyhedral_negAdjoint_and_finiteDualValue {m n : ℕ} (F : { F : (Fin m → ℝ) → (Fin n → ℝ) → EReal // ClosedConvexBifunction F }) (hProper : ProperConvexBifunction ↑F) (hPolyDual : PolyhedralConcaveBifunction (adjointOfConvexBifunction ⟨↑F, ⋯⟩)) (hFiniteDual : HasFiniteDualOptimalValueOfConvexProgram ⟨↑F, ⋯⟩) : ∃ (x : Fin n → ℝ), IsKuhnTuckerVectorForDualProgram ⟨↑F, ⋯⟩ x

Helper for Theorem 6.30.17: the finite polyhedral dual branch is a Chapter 29 generalized convex program for the negated adjoint bifunction, and its generalized Kuhn--Tucker vector is exactly a Chapter 30 dual Kuhn--Tucker vector.

theorem helperForTheorem_6_30_17_dualConjugateObjective_eq_negAdjointZeroSlice {m n : ℕ} (F : { F : (Fin m → ℝ) → (Fin n → ℝ) → EReal // ClosedConvexBifunction F }) : (fun (uStar : Fin m → ℝ) => fenchelConjugate m (convexProgramAssociatedWith ↑F) (-uStar)) = fun (uStar : Fin m → ℝ) => -adjointOfConvexBifunction ⟨↑F, ⋯⟩ 0 uStar

Helper for Theorem 6.30.17: the two bounded dual branches share the same remaining transport problem from bounded Chapter 27 data for uStar ↦ fenchelConjugate m (convexProgramAssociatedWith F.1) (-uStar) to primal strict consistency.

theorem helperForTheorem_6_30_17_boundedPrimalOptimalSet_nonfiniteCorner {m n : ℕ} (F : { F : (Fin m → ℝ) → (Fin n → ℝ) → EReal // ClosedConvexBifunction F }) (hProper : ProperConvexBifunction ↑F) (hMin : HasNonemptyBoundedPrimalOptimalSolutionSetOfConvexProgram ⟨↑F, ⋯⟩) (hx : ∃ (x : Fin n → ℝ), ↑F 0 x = convexProgramAssociatedWith (↑F) 0) (hNotFinite : ¬HasFinitePrimalOptimalValueOfConvexProgram ⟨↑F, ⋯⟩) : IsNormalConvexProgram ⟨↑F, ⋯⟩ ∧ IsNormalDualProgramOfConvexProgram ⟨↑F, ⋯⟩

Helper for Theorem 6.30.17: if the primal optimal set is nonempty and bounded but the primal value is still non-finite, then the only remaining case is the +∞ corner. In positive dimension that forces the minimum set to be all of space, contradicting boundedness; in dimension 0 the closed-slice identity rewrites the singleton primal value directly to the dual value, so the existing value-equality normality sink applies.

theorem helperForTheorem_6_30_17_boundedDualConjugateData_implies_primalStrictConsistency {m n : ℕ} (F : { F : (Fin m → ℝ) → (Fin n → ℝ) → EReal // ClosedConvexBifunction F }) (hProper : ProperConvexBifunction ↑F) (hData : (∃ (α : ℝ), (sublevelSetEReal (fun (uStar : Fin m → ℝ) => fenchelConjugate m (convexProgramAssociatedWith ↑F) (-uStar)) α).Nonempty ∧ Bornology.IsBounded (sublevelSetEReal (fun (uStar : Fin m → ℝ) => fenchelConjugate m (convexProgramAssociatedWith ↑F) (-uStar)) α) ∧ IsConsistentDualProgramOfConvexProgram ⟨↑F, ⋯⟩) ∨ (minimumSetEReal fun (uStar : Fin m → ℝ) => fenchelConjugate m (convexProgramAssociatedWith ↑F) (-uStar)).Nonempty ∧ Bornology.IsBounded (minimumSetEReal fun (uStar : Fin m → ℝ) => fenchelConjugate m (convexProgramAssociatedWith ↑F) (-uStar)) ∧ ∃ (uStar : Fin m → ℝ), adjointOfConvexBifunction ⟨↑F, ⋯⟩ 0 uStar = dualProgramOfConvexProgram ⟨↑F, ⋯⟩) : IsStrictlyConsistentConvexProgram ⟨↑F, ⋯⟩

Helper for Theorem 6.30.17: the two bounded dual branches share the same remaining transport problem from bounded Chapter 27 data for uStar ↦ fenchelConjugate m (convexProgramAssociatedWith F.1) (-uStar) to primal strict consistency.

theorem helperForTheorem_6_30_17_primalPolyhedralOrBoundedBranches_imply_normality {m n : ℕ} (F : { F : (Fin m → ℝ) → (Fin n → ℝ) → EReal // ClosedConvexBifunction F }) (hProper : ProperConvexBifunction ↑F) (hPrimalTerminal : PolyhedralConvexBifunction ↑F ∧ IsConsistentConvexProgram ⟨↑F, ⋯⟩ ∨ (∃ (α : ℝ), (primalSublevelSetOfConvexProgram ⟨↑F, ⋯⟩ α).Nonempty ∧ Bornology.IsBounded (primalSublevelSetOfConvexProgram ⟨↑F, ⋯⟩ α)) ∨ HasNonemptyBoundedPrimalOptimalSolutionSetOfConvexProgram ⟨↑F, ⋯⟩) : IsNormalConvexProgram ⟨↑F, ⋯⟩ ∧ IsNormalDualProgramOfConvexProgram ⟨↑F, ⋯⟩

Helper for Theorem 6.30.17: the remaining primal-side terminal branches are exactly the polyhedral primal branch (e) together with the bounded primal sublevel and bounded primal optimal-set branches (g) and (i).

theorem helperForTheorem_6_30_17_dualPolyhedralOrBoundedBranches_imply_normality {m n : ℕ} (F : { F : (Fin m → ℝ) → (Fin n → ℝ) → EReal // ClosedConvexBifunction F }) (hProper : ProperConvexBifunction ↑F) (hDualTerminal : PolyhedralConcaveBifunction (adjointOfConvexBifunction ⟨↑F, ⋯⟩) ∧ IsConsistentDualProgramOfConvexProgram ⟨↑F, ⋯⟩ ∨ (∃ (β : ℝ), (dualSuperlevelSetOfConvexProgram ⟨↑F, ⋯⟩ β).Nonempty ∧ Bornology.IsBounded (dualSuperlevelSetOfConvexProgram ⟨↑F, ⋯⟩ β)) ∨ HasNonemptyBoundedDualOptimalSolutionSetOfConvexProgram ⟨↑F, ⋯⟩) : IsNormalConvexProgram ⟨↑F, ⋯⟩ ∧ IsNormalDualProgramOfConvexProgram ⟨↑F, ⋯⟩

Helper for Theorem 6.30.17: the remaining dual-side terminal branches are exactly the polyhedral dual branch (f) together with the bounded dual superlevel and bounded dual optimal-set branches (h) and (j).