theorem helperForTheorem_6_30_11_improperConvexGraph_of_closed_not_proper {m n : ℕ} {F : (Fin m → ℝ) → (Fin n → ℝ) → EReal} (hClosed : ClosedConvexBifunction F) (hNotProper : ¬ProperConvexBifunction F) : ImproperConvexFunctionOn Set.univ (bifunctionGraphFunction F)

Helper for Theorem 6.30.11: once a closed convex bifunction fails properness, its graph function is an improper convex function on univ.

theorem helperForTheorem_6_30_11_concaveBifunctionClosure_eq_self_of_eq_const_top {m n : ℕ} {G : (Fin m → ℝ) → (Fin n → ℝ) → EReal} (hTop : G = fun (x : Fin m → ℝ) (x_1 : Fin n → ℝ) => ⊤) : concaveBifunctionClosure G = G

Helper for Theorem 6.30.11: the concave bifunction closure fixes the constant ⊤ bifunction.

theorem helperForTheorem_6_30_11_concaveBifunctionClosure_eq_self_of_eq_const_bot {m n : ℕ} {G : (Fin m → ℝ) → (Fin n → ℝ) → EReal} (hBot : G = fun (x : Fin m → ℝ) (x_1 : Fin n → ℝ) => ⊥) : concaveBifunctionClosure G = G

Helper for Theorem 6.30.11: the concave bifunction closure fixes the constant ⊥ bifunction.

theorem helperForTheorem_6_30_11_improperNegGraph_of_closed_not_proper {m n : ℕ} {G : (Fin m → ℝ) → (Fin n → ℝ) → EReal} (hClosed : ClosedConcaveBifunction G) (hNotProper : ¬ProperConcaveBifunction G) : ImproperConvexFunctionOn Set.univ fun (z : Fin (m + n) → ℝ) => -bifunctionGraphFunction G z

Helper for Theorem 6.30.11: once a closed concave bifunction fails properness, the negated graph function is an improper convex function on univ.

theorem helperForTheorem_6_30_11_convexGraph_values_top_or_bot_of_closed_not_proper {m n : ℕ} {F : (Fin m → ℝ) → (Fin n → ℝ) → EReal} (hClosed : ClosedConvexBifunction F) (hNotProper : ¬ProperConvexBifunction F) (z : Fin (m + n) → ℝ) : bifunctionGraphFunction F z = ⊤ ∨ bifunctionGraphFunction F z = ⊥

Helper for Theorem 6.30.11: a closed improper convex bifunction graph can only take the values ⊤ and ⊥.

theorem helperForTheorem_6_30_11_negConcaveGraph_values_top_or_bot_of_closed_not_proper {m n : ℕ} {G : (Fin m → ℝ) → (Fin n → ℝ) → EReal} (hClosed : ClosedConcaveBifunction G) (hNotProper : ¬ProperConcaveBifunction G) (z : Fin (m + n) → ℝ) : -bifunctionGraphFunction G z = ⊤ ∨ -bifunctionGraphFunction G z = ⊥

Helper for Theorem 6.30.11: once a closed concave bifunction is improper, its negated graph also takes only the values ⊤ and ⊥.

theorem helperForTheorem_6_30_11_improper_convex_fixed_point_eq_const_top_or_bot {m n : ℕ} {F : (Fin m → ℝ) → (Fin n → ℝ) → EReal} (hImproper : ImproperConvexFunctionOn Set.univ (bifunctionGraphFunction F)) (hFixed : convexBifunctionClosure F = F) : (F = fun (x : Fin m → ℝ) (x_1 : Fin n → ℝ) => ⊤) ∨ F = fun (x : Fin m → ℝ) (x_1 : Fin n → ℝ) => ⊥

Helper for Theorem 6.30.11: if an improper convex bifunction graph is fixed by the current Chapter 2 closure, then the bifunction must already be constant ⊤ or constant ⊥.

theorem helperForTheorem_6_30_11_improper_concave_fixed_point_eq_const_top_or_bot {m n : ℕ} {G : (Fin m → ℝ) → (Fin n → ℝ) → EReal} (hImproper : ImproperConvexFunctionOn Set.univ fun (z : Fin (m + n) → ℝ) => -bifunctionGraphFunction G z) (hFixed : concaveBifunctionClosure G = G) : (G = fun (x : Fin m → ℝ) (x_1 : Fin n → ℝ) => ⊤) ∨ G = fun (x : Fin m → ℝ) (x_1 : Fin n → ℝ) => ⊥

Helper for Theorem 6.30.11: if the negated graph of an improper concave bifunction is fixed by the current Chapter 2 closure, then the bifunction must already be constant ⊤ or constant ⊥.

theorem helperForTheorem_6_30_11_convexBifunctionClosure_ne_self_of_closed_not_proper_nonconstant {m n : ℕ} {F : (Fin m → ℝ) → (Fin n → ℝ) → EReal} (hClosed : ClosedConvexBifunction F) (hNotProper : ¬ProperConvexBifunction F) (hNotTop : F ≠ fun (x : Fin m → ℝ) (x_1 : Fin n → ℝ) => ⊤) (hNotBot : F ≠ fun (x : Fin m → ℝ) (x_1 : Fin n → ℝ) => ⊥) : convexBifunctionClosure F ≠ F

Helper for Theorem 6.30.11: in the closed improper nonconstant convex branch, the current Chapter 2 closure semantics force the failure of the desired fixed-point identity.

theorem helperForTheorem_6_30_11_concaveBifunctionClosure_ne_self_of_closed_not_proper_nonconstant {m n : ℕ} {G : (Fin m → ℝ) → (Fin n → ℝ) → EReal} (hClosed : ClosedConcaveBifunction G) (hNotProper : ¬ProperConcaveBifunction G) (hNotTop : G ≠ fun (x : Fin m → ℝ) (x_1 : Fin n → ℝ) => ⊤) (hNotBot : G ≠ fun (x : Fin m → ℝ) (x_1 : Fin n → ℝ) => ⊥) : concaveBifunctionClosure G ≠ G

Helper for Theorem 6.30.11: in the closed improper nonconstant concave branch, the current Chapter 2 closure semantics force the failure of the desired fixed-point identity after negating the graph.

theorem helperForTheorem_6_30_11_convexBifunctionClosure_eq_self_of_closed {m n : ℕ} {F : (Fin m → ℝ) → (Fin n → ℝ) → EReal} (hClosed : ClosedConvexBifunction F) (hGraphNeBot : ∀ (z : Fin (m + n) → ℝ), bifunctionGraphFunction F z ≠ ⊥) : convexBifunctionClosure F = F

Helper for Theorem 6.30.11: a closed convex bifunction whose graph never attains ⊥ is fixed by the canonical graph closure. This is the graph-level lift of the Chapter 2 fixed-point theorem in the non-⊥ branch supported by the current closure API.

theorem helperForTheorem_6_30_11_concaveBifunctionClosure_eq_self_of_closed {m n : ℕ} {G : (Fin m → ℝ) → (Fin n → ℝ) → EReal} (hClosed : ClosedConcaveBifunction G) (hNegGraphNeBot : ∀ (z : Fin (m + n) → ℝ), -bifunctionGraphFunction G z ≠ ⊥) : concaveBifunctionClosure G = G

Helper for Theorem 6.30.11: a closed concave bifunction whose negated graph never attains ⊥ is fixed by the canonical concave graph closure. This is the concave counterpart of the supported non-⊥ convex fixed-point theorem after negating the graph.

theorem helperForTheorem_6_30_11_convex_biadjoint_eq_self_of_closure_eq_self {m n : ℕ} {F : (Fin m → ℝ) → (Fin n → ℝ) → EReal} (hF : ConvexBifunction F) (hClosureFixed : convexBifunctionClosure F = F) : biadjointOfConvexBifunction ⟨F, hF⟩ = F

Helper for Theorem 6.30.11: in the convex branch, once the closure identity cl F = F is supplied, the biconjugation formula immediately collapses to the fixed-point statement F^{**} = F.

theorem helperForTheorem_6_30_11_concave_biadjoint_eq_self_of_closure_eq_self {m n : ℕ} {F : (Fin m → ℝ) → (Fin n → ℝ) → EReal} (hF : ConcaveBifunction F) (hClosureFixed : concaveBifunctionClosure F = F) : biadjointOfConcaveBifunction ⟨F, hF⟩ = F

Helper for Theorem 6.30.11: in the concave branch, the fixed-point clause follows by rewriting the biadjoint as the canonical concave closure and then using cl F = F.

theorem adjoint_bifunction_closure_properness_biconjugation_and_polyhedrality {m n : ℕ} (F : (Fin m → ℝ) → (Fin n → ℝ) → EReal) : (∀ (hF : ConvexBifunction F), ClosedConcaveBifunction (adjointOfConvexBifunction ⟨F, hF⟩) ∧ (ProperConcaveBifunction (adjointOfConvexBifunction ⟨F, hF⟩) ↔ ProperConvexBifunction F) ∧ biadjointOfConvexBifunction ⟨F, hF⟩ = convexBifunctionClosure F ∧ (convexBifunctionClosure F = F → biadjointOfConvexBifunction ⟨F, hF⟩ = F) ∧ (ClosedConvexBifunction F ∧ ProperConvexBifunction F → ClosedConcaveBifunction (adjointOfConvexBifunction ⟨F, hF⟩) ∧ ProperConcaveBifunction (adjointOfConvexBifunction ⟨F, hF⟩)) ∧ (PolyhedralConvexBifunction F → PolyhedralConcaveBifunction (adjointOfConvexBifunction ⟨F, hF⟩))) ∧ ∀ (hF : ConcaveBifunction F), ClosedConvexBifunction (adjointOfConcaveBifunction ⟨F, hF⟩) ∧ (ProperConvexBifunction (adjointOfConcaveBifunction ⟨F, hF⟩) ↔ ProperConcaveBifunction F) ∧ biadjointOfConcaveBifunction ⟨F, hF⟩ = concaveBifunctionClosure F ∧ (concaveBifunctionClosure F = F → biadjointOfConcaveBifunction ⟨F, hF⟩ = F) ∧ (ClosedConcaveBifunction F ∧ ProperConcaveBifunction F → ClosedConvexBifunction (adjointOfConcaveBifunction ⟨F, hF⟩) ∧ ProperConvexBifunction (adjointOfConcaveBifunction ⟨F, hF⟩)) ∧ (PolyhedralConcaveBifunction F → PolyhedralConvexBifunction (adjointOfConcaveBifunction ⟨F, hF⟩))

Theorem 6.30.11: for a convex or concave bifunction F : ℝ^m → ℝ^n, its adjoint is a closed bifunction of the opposite type from ℝ^n to ℝ^m, it is proper exactly when F is proper, and the biadjoint agrees with the appropriate closure of F. The textbook closed-case conclusion is formalized here through the explicit fixed-point identity cl F = F, i.e. through the closure operator appearing in the preceding biconjugation statement itself. Closed proper convex and closed proper concave bifunctions still correspond through adjunction, and polyhedrality is preserved by adjoints.