def extendedRealHypograph {n : ℕ} (g : (Fin n → ℝ) → EReal) : Set ((Fin n → ℝ) × ℝ)

The hypograph of an extended-real-valued function on ℝ^n, viewed as a subset of ℝ^n × ℝ.

def extendedRealEffectiveDomain {n : ℕ} (g : (Fin n → ℝ) → EReal) : Set (Fin n → ℝ)

The effective domain of an extended-real-valued function on ℝ^n, i.e. the points where the value is strictly greater than -∞.

def extendedRealHypographAndEffectiveDomain {n : ℕ} (g : (Fin n → ℝ) → EReal) : Set ((Fin n → ℝ) × ℝ) × Set (Fin n → ℝ)

Definition 6.30.1: for g : ℝ^n → [-∞, +∞], the hypograph is {(x, μ) ∈ ℝ^n × ℝ | μ ≤ g(x)} and the effective domain is dom g = {x ∈ ℝ^n | g x > -∞}.

noncomputable def convexClosure {n : ℕ} (f : (Fin n → ℝ) → EReal) : (Fin n → ℝ) → EReal

The convex closure of an extended-real-valued function on ℝ^n. This reuses the canonical repository-wide closure convexFunctionClosure, so the Chapter 6 bifunction closure agrees with the same cl used earlier in the book.

noncomputable def concaveClosure {n : ℕ} (g : (Fin n → ℝ) → EReal) : (Fin n → ℝ) → EReal

Definition 6.30.3: for a concave function g : ℝ^n → [-∞, +∞], its closure cl g is the negative of the canonical convex closure of -g.

theorem concaveClosure_eq_neg_convexClosure_neg {n : ℕ} (g : (Fin n → ℝ) → EReal) : concaveClosure g = fun (x : Fin n → ℝ) => -convexClosure (fun (z : Fin n → ℝ) => -g z) x

Negating converts affine majorants of g into affine minorants of -g, so the concave closure is the negative of the convex closure of the negated function.

def ConcaveFunction {n : ℕ} (g : (Fin n → ℝ) → EReal) : Prop

An extended-real-valued function on ℝ^n is concave when its negative is convex.

def ClosedConcaveFunction {n : ℕ} (g : (Fin n → ℝ) → EReal) : Prop

An extended-real-valued function on ℝ^n is closed and concave when its negative is a closed convex function.

def ProperConvexBifunction {m n : ℕ} (F : (Fin m → ℝ) → (Fin n → ℝ) → EReal) : Prop

A convex bifunction is proper when its graph function on ℝ^(m + n) is proper convex.

def ProperConcaveBifunction {m n : ℕ} (G : (Fin m → ℝ) → (Fin n → ℝ) → EReal) : Prop

A concave bifunction is proper when its graph function on ℝ^(m + n) is proper concave.

def ClosedConvexBifunction {m n : ℕ} (F : (Fin m → ℝ) → (Fin n → ℝ) → EReal) : Prop

A convex bifunction is closed when its graph function is closed convex on ℝ^(m + n).

def ClosedConcaveBifunction {m n : ℕ} (G : (Fin m → ℝ) → (Fin n → ℝ) → EReal) : Prop

A concave bifunction is closed when its graph function is closed concave on ℝ^(m + n).

def PolyhedralConvexBifunction {m n : ℕ} (F : (Fin m → ℝ) → (Fin n → ℝ) → EReal) : Prop

A convex bifunction is polyhedral when its graph function is polyhedral convex.

def PolyhedralConcaveBifunction {m n : ℕ} (G : (Fin m → ℝ) → (Fin n → ℝ) → EReal) : Prop

A concave bifunction is polyhedral when the negative of its graph function is polyhedral convex.

noncomputable def convexBifunctionClosure {m n : ℕ} (F : (Fin m → ℝ) → (Fin n → ℝ) → EReal) : (Fin m → ℝ) → (Fin n → ℝ) → EReal

The closure of a convex bifunction is the bifunction induced by the convex closure of its graph function.

noncomputable def concaveBifunctionClosure {m n : ℕ} (G : (Fin m → ℝ) → (Fin n → ℝ) → EReal) : (Fin m → ℝ) → (Fin n → ℝ) → EReal

The closure of a concave bifunction is the bifunction induced by the concave closure of its graph function.

theorem adjointOfConcaveBifunction_closedConvex {m n : ℕ} (G : { G : (Fin m → ℝ) → (Fin n → ℝ) → EReal // ConcaveBifunction G }) : ClosedConvexBifunction (adjointOfConcaveBifunction G)

The adjoint of a concave bifunction is a closed convex bifunction on the reversed product.

noncomputable def adjointOfConvexBifunctionAsConcave {m n : ℕ} (F : { F : (Fin m → ℝ) → (Fin n → ℝ) → EReal // ConvexBifunction F }) : { G : (Fin n → ℝ) → (Fin m → ℝ) → EReal // ConcaveBifunction G }

The convex adjoint, packaged as a concave bifunction on the reversed variables.

noncomputable def adjointOfConcaveBifunctionAsConvex {m n : ℕ} (G : { G : (Fin m → ℝ) → (Fin n → ℝ) → EReal // ConcaveBifunction G }) : { F : (Fin n → ℝ) → (Fin m → ℝ) → EReal // ConvexBifunction F }

The concave adjoint, packaged as a convex bifunction on the reversed variables.

noncomputable def biadjointOfConvexBifunction {m n : ℕ} (F : { F : (Fin m → ℝ) → (Fin n → ℝ) → EReal // ConvexBifunction F }) : (Fin m → ℝ) → (Fin n → ℝ) → EReal

The biconjugate of a convex bifunction, obtained by taking the concave adjoint of its adjoint.

noncomputable def biadjointOfConcaveBifunction {m n : ℕ} (G : { G : (Fin m → ℝ) → (Fin n → ℝ) → EReal // ConcaveBifunction G }) : (Fin m → ℝ) → (Fin n → ℝ) → EReal

The biconjugate of a concave bifunction, obtained by taking the convex adjoint of its adjoint.

theorem helperForTheorem_6_30_11_adjointOfConcave_graph_eq_fenchelConjugate_precomp {m n : ℕ} (G : { G : (Fin m → ℝ) → (Fin n → ℝ) → EReal // ConcaveBifunction G }) (z : Fin (n + m) → ℝ) : bifunctionGraphFunction (adjointOfConcaveBifunction G) z = fenchelConjugate (m + n) (fun (w : Fin (m + n) → ℝ) => -bifunctionGraphFunction (↑G) w) (-helperForTheorem_6_30_10_coordinateLinearMap z)

Helper for Theorem 6.30.11: the graph of the adjoint of a concave bifunction is the Fenchel conjugate of the negated graph function after the coordinate shuffle (x*, u*) ↦ (u*, -x*).

theorem helperForTheorem_6_30_11_coordinateLinearMap_surjective {m n : ℕ} : Function.Surjective ⇑helperForTheorem_6_30_10_coordinateLinearMap

Helper for Theorem 6.30.11: the coordinate shuffle from Theorem 6.30.10 is surjective.

theorem helperForTheorem_6_30_11_negCoordinateLinearMap_surjective {m n : ℕ} : Function.Surjective ⇑(-helperForTheorem_6_30_10_coordinateLinearMap)

Helper for Theorem 6.30.11: negating the coordinate shuffle still gives a surjective linear map.

theorem helperForTheorem_6_30_11_coordinateLinearMap_comp_neg_reverse {m n : ℕ} (z : Fin (m + n) → ℝ) : helperForTheorem_6_30_10_coordinateLinearMap (-helperForTheorem_6_30_10_coordinateLinearMap z) = z

Helper for Theorem 6.30.11: the two coordinate shuffles cancel after inserting the intermediate minus sign required by the adjoint formulas.

theorem helperForTheorem_6_30_11_fenchelConjugate_precomp_coordinateLinearMap {m n : ℕ} (f : (Fin (m + n) → ℝ) → EReal) (z : Fin (m + n) → ℝ) : fenchelConjugate (n + m) (fun (w : Fin (n + m) → ℝ) => f (helperForTheorem_6_30_10_coordinateLinearMap w)) (-helperForTheorem_6_30_10_coordinateLinearMap z) = fenchelConjugate (m + n) f z

Helper for Theorem 6.30.11: Fenchel conjugation through the coordinate shuffle is equivalent to evaluating the conjugate at the correspondingly shuffled dual point.

theorem helperForTheorem_6_30_11_neg_coordinateLinearMap_comp_reverse {m n : ℕ} (z : Fin (m + n) → ℝ) : -helperForTheorem_6_30_10_coordinateLinearMap (helperForTheorem_6_30_10_coordinateLinearMap z) = z

Helper for Theorem 6.30.11: negating after the reverse coordinate shuffle recovers the original point.

theorem helperForTheorem_6_30_11_neg_fenchelConjugate_precomp_coordinateLinearMap {m n : ℕ} (f : (Fin (m + n) → ℝ) → EReal) (z : Fin (m + n) → ℝ) : fenchelConjugate (n + m) (fun (w : Fin (n + m) → ℝ) => f (-helperForTheorem_6_30_10_coordinateLinearMap w)) (helperForTheorem_6_30_10_coordinateLinearMap z) = fenchelConjugate (m + n) f z

Helper for Theorem 6.30.11: the opposite sign convention for the coordinate shuffle also transports Fenchel conjugation back to the original dual point.

theorem helperForTheorem_6_30_11_properConvexFunctionOn_univ_of_properConvexERealFunction {n : ℕ} (f : (Fin n → ℝ) → EReal) (hf : ProperConvexERealFunction f) : ProperConvexFunctionOn Set.univ f

Helper for Theorem 6.30.11: a proper convex EReal-valued function on ℝ^n induces a proper convex function on Set.univ, so the Fenchel-conjugate API applies directly.

theorem helperForTheorem_6_30_11_properConvexFunctionOn_of_precomp_linearMap_surjective {n m : ℕ} (A : (Fin n → ℝ) →ₗ[ℝ] Fin m → ℝ) (hA : Function.Surjective ⇑A) {f : (Fin m → ℝ) → EReal} (hf : ProperConvexFunctionOn Set.univ fun (x : Fin n → ℝ) => f (A x)) : ProperConvexFunctionOn Set.univ f

Helper for Theorem 6.30.11: if a surjective linear precomposition is proper on univ, then the original function is proper on univ as well.

theorem helperForTheorem_6_30_11_convex_branch_except_closed_fixed_point {m n : ℕ} (F : (Fin m → ℝ) → (Fin n → ℝ) → EReal) (hF : ConvexBifunction F) : ClosedConcaveBifunction (adjointOfConvexBifunction ⟨F, hF⟩) ∧ (ProperConcaveBifunction (adjointOfConvexBifunction ⟨F, hF⟩) ↔ ProperConvexBifunction F) ∧ (ClosedConvexBifunction F ∧ ProperConvexBifunction F → ClosedConcaveBifunction (adjointOfConvexBifunction ⟨F, hF⟩) ∧ ProperConcaveBifunction (adjointOfConvexBifunction ⟨F, hF⟩)) ∧ (PolyhedralConvexBifunction F → PolyhedralConcaveBifunction (adjointOfConvexBifunction ⟨F, hF⟩))

Helper for Theorem 6.30.11: aside from the closed fixed-point clause, the convex branch of the theorem follows from Theorem 6.30.10 together with standard Fenchel-conjugate transport results for properness and polyhedrality.

theorem helperForTheorem_6_30_11_concave_branch_except_closed_fixed_point {m n : ℕ} (G : (Fin m → ℝ) → (Fin n → ℝ) → EReal) (hG : ConcaveBifunction G) : ClosedConvexBifunction (adjointOfConcaveBifunction ⟨G, hG⟩) ∧ (ProperConvexBifunction (adjointOfConcaveBifunction ⟨G, hG⟩) ↔ ProperConcaveBifunction G) ∧ (ClosedConcaveBifunction G ∧ ProperConcaveBifunction G → ClosedConvexBifunction (adjointOfConcaveBifunction ⟨G, hG⟩) ∧ ProperConvexBifunction (adjointOfConcaveBifunction ⟨G, hG⟩)) ∧ (PolyhedralConcaveBifunction G → PolyhedralConvexBifunction (adjointOfConcaveBifunction ⟨G, hG⟩))

Helper for Theorem 6.30.11: aside from the closed fixed-point clause, the concave branch of the theorem follows from the corresponding graph rewrite and the same Fenchel transport results.

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

Helper for Theorem 6.30.11: the convex biadjoint is the closure of the original convex bifunction.

theorem helperForTheorem_6_30_11_biadjointOfConcave_graph_eq_concaveBifunctionClosure_via_coordinate_shuffle {m n : ℕ} (G : (Fin m → ℝ) → (Fin n → ℝ) → EReal) (hG : ConcaveBifunction G) : biadjointOfConcaveBifunction ⟨G, hG⟩ = concaveBifunctionClosure G

Helper for Theorem 6.30.11: the concave biadjoint is the closure of the original concave bifunction.

Route correction for Theorem 6.30.11:

The original proof cites Theorem 12.2 at the level of the graph function. The local transport lemmas below reduce the remaining work to a graph-level fixed-point theorem for convexFunctionClosure and concaveClosure.

Under the current repository semantics, that route breaks in the closed improper branch: convexFunctionClosure_eq_of_closedConvexFunction still requires the extra hypothesis ∀ x, f x ≠ ⊥, while convexFunctionClosure_eq_bot_of_exists_bot collapses any function with one ⊥ value to the constant ⊥ closure. Therefore the two fixed-point lemmas below remain the exact upstream blocker for the theorem as currently formalized.

theorem helperForTheorem_6_30_11_convexBifunctionClosure_eq_self_of_closed_of_graph_ne_bot {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 is fixed by the canonical graph closure. This is the graph-level lift of the Chapter 2 fixed-point theorem for closed convex functions.

theorem helperForTheorem_6_30_11_convexBifunctionClosure_eq_self_of_closed_proper {m n : ℕ} {F : (Fin m → ℝ) → (Fin n → ℝ) → EReal} (hClosed : ClosedConvexBifunction F) (hProper : ProperConvexBifunction F) : convexBifunctionClosure F = F

Helper for Theorem 6.30.11: the closed proper convex branch is already covered by the graph-level fixed-point theorem, because properness rules out ⊥ on the graph.

theorem helperForTheorem_6_30_11_concaveBifunctionClosure_eq_self_of_closed_of_neg_graph_ne_bot {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.

theorem helperForTheorem_6_30_11_concaveBifunctionClosure_eq_self_of_closed_proper {m n : ℕ} {G : (Fin m → ℝ) → (Fin n → ℝ) → EReal} (hClosed : ClosedConcaveBifunction G) (hProper : ProperConcaveBifunction G) : concaveBifunctionClosure G = G

Helper for Theorem 6.30.11: the closed proper concave branch is already covered by the graph-level fixed-point theorem after negating the graph, because properness rules out ⊥ there.

theorem helperForTheorem_6_30_11_convexBifunctionClosure_eq_self_of_eq_const_top {m n : ℕ} {F : (Fin m → ℝ) → (Fin n → ℝ) → EReal} (hTop : F = fun (x : Fin m → ℝ) (x_1 : Fin n → ℝ) => ⊤) : convexBifunctionClosure F = F

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

theorem helperForTheorem_6_30_11_convexBifunctionClosure_eq_self_of_eq_const_bot {m n : ℕ} {F : (Fin m → ℝ) → (Fin n → ℝ) → EReal} (hBot : F = fun (x : Fin m → ℝ) (x_1 : Fin n → ℝ) => ⊥) : convexBifunctionClosure F = F

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