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

Definition 36.4.5: Let F be a convex bifunction from ℝ^m to ℝ^n. The Lagrangian of the associated convex program is the function L : ℝ^m × ℝ^n → [-∞, +∞] defined by L(u*, x) := inf_{u ∈ ℝ^m} (⟨u*, u⟩ + (F u) x).

noncomputable def infPairing {m : ℕ} (uStar : Fin m → ℝ) (g : (Fin m → ℝ) → EReal) : EReal

The infimal pairing ⟪uStar, g⟫ := inf_u (⟨uStar, u⟩ - g u) used in the book for an extended-real function g : ℝ^m → [-∞, +∞].

def IsConcaveInFirst {m n : ℕ} (L : (Fin m → ℝ) → (Fin n → ℝ) → EReal) : Prop

Concavity in the first argument uStar (pointwise in x) for an extended-real bifunction L(uStar, x).

def IsConvexInSecond {m n : ℕ} (L : (Fin m → ℝ) → (Fin n → ℝ) → EReal) : Prop

Convexity in the second argument x (pointwise in uStar) for an extended-real bifunction L(uStar, x).

theorem helperForProposition_36_4_6_finDot_smul_add_left {m : ℕ} (uStar₁ uStar₂ u : Fin m → ℝ) (a b : ℝ) : finDot (a • uStar₁ + b • uStar₂) u = a * finDot uStar₁ u + b * finDot uStar₂ u

Helper for Proposition 36.4.6: finDot is linear in its first argument.

theorem helperForProposition_36_4_6_finDot_smul_add_right {m : ℕ} (uStar u₁ u₂ : Fin m → ℝ) (a b : ℝ) : finDot uStar (a • u₁ + b • u₂) = a * finDot uStar u₁ + b * finDot uStar u₂

Helper for Proposition 36.4.6: finDot is linear in its second argument.

theorem helperForProposition_36_4_6_finDot_eq_dotProduct {m : ℕ} (uStar u : Fin m → ℝ) : finDot uStar u = uStar ⬝ᵥ u

Helper for Proposition 36.4.6: the local finDot notation agrees with the standard dotProduct.

theorem helperForProposition_36_4_6_infPairing_eq_concaveConjugate {m : ℕ} (uStar : Fin m → ℝ) (g : (Fin m → ℝ) → EReal) : infPairing uStar g = concaveConjugate g uStar

Helper for Proposition 36.4.6: the local infimal pairing is exactly the chapter's concave conjugate.

def helperForProposition_36_4_6_negateScalarSecond {m : ℕ} : (Fin m → ℝ) × ℝ → (Fin m → ℝ) × ℝ

Helper for Proposition 36.4.6: negate the scalar coordinate while keeping the vector coordinate fixed.

theorem helperForProposition_36_4_6_negateScalarSecond_isLinear {m : ℕ} : IsLinearMap ℝ helperForProposition_36_4_6_negateScalarSecond

Helper for Proposition 36.4.6: negating the scalar coordinate is linear on (ℝ^m) × ℝ.

theorem helperForProposition_36_4_6_infPairing_hypograph_preimage_negEpigraph {m : ℕ} (g : (Fin m → ℝ) → EReal) : {p : (Fin m → ℝ) × ℝ | ↑p.2 ≤ infPairing p.1 g} = helperForProposition_36_4_6_negateScalarSecond ⁻¹' epigraph Set.univ fun (uStar : Fin m → ℝ) => -infPairing uStar g

Helper for Proposition 36.4.6: the hypograph of infPairing is the preimage of the epigraph of its negation under scalar negation.

theorem helperForProposition_36_4_6_infPairing_isConcave {m : ℕ} (g : (Fin m → ℝ) → EReal) : Convex ℝ {p : (Fin m → ℝ) × ℝ | ↑p.2 ≤ infPairing p.1 g}

Helper for Proposition 36.4.6: for every function g, the map uStar ↦ infPairing uStar g is concave.

theorem helperForProposition_36_4_6_graphFunction_isConvexFunction {m n : ℕ} (F : { F : (Fin m → ℝ) → (Fin n → ℝ) → EReal // IsEpigraphConvexBifunction F }) : ConvexFunction (graphFunctionOfBifunction ↑F)

Helper for Proposition 36.4.6: the graph function of a section-local convex bifunction is a convex function on the product space.

theorem helperForProposition_36_4_6_tiltedGraph_isConvexFunction {m n : ℕ} (F : { F : (Fin m → ℝ) → (Fin n → ℝ) → EReal // IsEpigraphConvexBifunction F }) (uStar : Fin m → ℝ) : ConvexFunction fun (z : Fin (m + n) → ℝ) => ↑(finDot uStar (projXLinearMap z)) + graphFunctionOfBifunction (↑F) z

Helper for Proposition 36.4.6: the tilted graph function used for the fixed-uStar sections is convex.

theorem helperForProposition_36_4_6_secondSection_eq_projectionInf {m n : ℕ} (F : { F : (Fin m → ℝ) → (Fin n → ℝ) → EReal // IsEpigraphConvexBifunction F }) (uStar : Fin m → ℝ) : (fun (x : Fin n → ℝ) => bifunctionLagrangian F uStar x) = imageUnderLinearMap projLamLinearMap fun (z : Fin (m + n) → ℝ) => ↑(finDot uStar (projXLinearMap z)) + graphFunctionOfBifunction (↑F) z

Helper for Proposition 36.4.6: for fixed uStar, the x-section of the Lagrangian is the fiber infimum of the tilted graph under projection to the x-coordinates.

theorem bifunctionLagrangian_eq_infPairing_inverse_and_concave_convex {m n : ℕ} (F : { F : (Fin m → ℝ) → (Fin n → ℝ) → EReal // IsEpigraphConvexBifunction F }) : (∀ (uStar : Fin m → ℝ) (x : Fin n → ℝ), bifunctionLagrangian F uStar x = ⨅ (u : Fin m → ℝ), ↑(finDot uStar u) + -bifunctionInverse (↑F) x u) ∧ (∀ (uStar : Fin m → ℝ) (x : Fin n → ℝ), bifunctionLagrangian F uStar x = infPairing uStar (bifunctionInverse (↑F) x)) ∧ IsConcaveInFirst (bifunctionLagrangian F) ∧ IsConvexInSecond (bifunctionLagrangian F)

Proposition 36.4.6: Let F be a convex bifunction from ℝ^m to ℝ^n with inverse F_*, and let L be defined by Definition 36.4.5. Then

L(uStar, x) = inf_u (⟨uStar, u⟩ - (F_* x)(u)) = ⟪uStar, F_* x⟫.

In particular, L is concave in uStar and convex in x.

def IsUpperClosedInFirst {m n : ℕ} (L : (Fin m → ℝ) → (Fin n → ℝ) → EReal) : Prop

Upper closedness in the first argument uStar (pointwise in x) for an extended-real function L(uStar, x): for each x, the hypograph {(uStar,t) | t ≤ L(uStar,x)} is closed.

def IsLowerClosedInSecond {m n : ℕ} (L : (Fin m → ℝ) → (Fin n → ℝ) → EReal) : Prop

Lower closedness in the second argument x (pointwise in uStar) for an extended-real function L(uStar, x): for each uStar, the epigraph {(x,t) | L(uStar,x) ≤ t} is closed.

def IsUpperClosedConcaveConvex {m n : ℕ} (L : (Fin m → ℝ) → (Fin n → ℝ) → EReal) : Prop

A bundled predicate expressing that L(uStar, x) is upper closed concave-convex on ℝ^m × ℝ^n: it is upper closed and concave in uStar, and lower closed and convex in x.

theorem helperForTheorem_36_5_lagrangian_has_concaveConvex_orientation {m n : ℕ} (F : { F : (Fin m → ℝ) → (Fin n → ℝ) → EReal // IsEpigraphConvexBifunction F }) : IsConcaveInFirst (bifunctionLagrangian F) ∧ IsConvexInSecond (bifunctionLagrangian F)

Helper for Theorem 36.5: a Lagrangian already has the concave-convex orientation from Proposition 36.4.6.

theorem helperForTheorem_36_5_infPairing_isFunctionConcaveClosed {m : ℕ} (g : (Fin m → ℝ) → EReal) : IsFunctionConcaveClosed fun (uStar : Fin m → ℝ) => infPairing uStar g

Helper for Theorem 36.5: every one-variable infimal pairing section is concave-closed.

theorem helperForTheorem_36_5_upperClosedSlices_to_functionClosedData {m n : ℕ} {L : (Fin m → ℝ) → (Fin n → ℝ) → EReal} (hL : IsUpperClosedConcaveConvex L) : (∀ (x : Fin n → ℝ), IsFunctionConcaveClosed fun (uStar : Fin m → ℝ) => L uStar x) ∧ ∀ (uStar : Fin m → ℝ), IsFunctionConvexClosed fun (x : Fin n → ℝ) => L uStar x

Helper for Theorem 36.5: upper/lower closedness of an upper closed concave-convex bifunction already gives the Section 33 one-variable closedness data on every slice.

theorem helperForTheorem_36_5_sliceClosedConcave_of_upperClosedConcave {m n : ℕ} {L : (Fin m → ℝ) → (Fin n → ℝ) → EReal} (hUpper : IsUpperClosedInFirst L) (hConc : IsConcaveInFirst L) (x : Fin n → ℝ) : ClosedConcaveFunction fun (uStar : Fin m → ℝ) => L uStar x

Helper for Theorem 36.5: upper closedness together with first-variable concavity upgrades each fixed-x slice to a closed concave function in the Chapter 6 sense.

theorem helperForTheorem_36_5_reconstructedBifunction_isEpigraphConvex {m n : ℕ} {L : (Fin m → ℝ) → (Fin n → ℝ) → EReal} (hConv : IsConvexInSecond L) : IsEpigraphConvexBifunction fun (u : Fin m → ℝ) (x : Fin n → ℝ) => ⨆ (uStar : Fin m → ℝ), L uStar x + -↑(finDot uStar u)

Helper for Theorem 36.5: the conjugate reconstruction F(u, x) = sup_{u*} (L(u*, x) - ⟨u*, u⟩) is convex in the epigraph sense whenever the second sections of L are convex.

theorem helperForTheorem_36_5_reconstructedBifunction_epigraph_eq_iInter_preimages {m n : ℕ} {L : (Fin m → ℝ) → (Fin n → ℝ) → EReal} : (bifunctionEpigraph fun (u : Fin m → ℝ) (x : Fin n → ℝ) => ⨆ (uStar : Fin m → ℝ), L uStar x + -↑(finDot uStar u)) = ⋂ (uStar : Fin m → ℝ), (fun (p : ((Fin m → ℝ) × (Fin n → ℝ)) × ℝ) => (p.1.2, p.2 + finDot uStar p.1.1)) ⁻¹' {q : (Fin n → ℝ) × ℝ | L uStar q.1 ≤ ↑q.2}

Helper for Theorem 36.5: the epigraph of the reconstructed conjugate bifunction is the intersection of the closed fixed-uStar slice epigraphs after shifting the height coordinate by ⟨uStar, u⟩.

theorem helperForTheorem_36_5_reconstructedBifunction_isEpigraphClosed {m n : ℕ} {L : (Fin m → ℝ) → (Fin n → ℝ) → EReal} (hLower : IsLowerClosedInSecond L) : IsEpigraphClosedConvexBifunction fun (u : Fin m → ℝ) (x : Fin n → ℝ) => ⨆ (uStar : Fin m → ℝ), L uStar x + -↑(finDot uStar u)

Helper for Theorem 36.5: the same conjugate reconstruction has closed epigraph whenever the second sections of L are lower closed.

theorem helperForTheorem_36_5_reconstructedBifunction_closed_convex {m n : ℕ} {L : (Fin m → ℝ) → (Fin n → ℝ) → EReal} (hLower : IsLowerClosedInSecond L) (hConv : IsConvexInSecond L) : (IsEpigraphConvexBifunction fun (u : Fin m → ℝ) (x : Fin n → ℝ) => ⨆ (uStar : Fin m → ℝ), L uStar x + -↑(finDot uStar u)) ∧ IsEpigraphClosedConvexBifunction fun (u : Fin m → ℝ) (x : Fin n → ℝ) => ⨆ (uStar : Fin m → ℝ), L uStar x + -↑(finDot uStar u)

Helper for Theorem 36.5: combining the previous two facts packages the reconstructed conjugate bifunction as a closed convex bifunction.

theorem helperForTheorem_36_5_reconstructedBifunction_recovers_L {m n : ℕ} {L : (Fin m → ℝ) → (Fin n → ℝ) → EReal} (hClosedSlices : ∀ (x : Fin n → ℝ), ClosedConcaveFunction fun (uStar : Fin m → ℝ) => L uStar x) (hProperSlices : ∀ (x : Fin n → ℝ), ProperConcaveERealFunction fun (uStar : Fin m → ℝ) => L uStar x) (hFconv : IsEpigraphConvexBifunction fun (u : Fin m → ℝ) (x : Fin n → ℝ) => ⨆ (uStar : Fin m → ℝ), L uStar x + -↑(finDot uStar u)) (uStar : Fin m → ℝ) (x : Fin n → ℝ) : bifunctionLagrangian ⟨fun (u : Fin m → ℝ) (x : Fin n → ℝ) => ⨆ (vStar : Fin m → ℝ), L vStar x + -↑(finDot vStar u), hFconv⟩ uStar x = L uStar x

Helper for Theorem 36.5: once each fixed-x slice of L is closed concave, the Lagrangian of the reconstructed bifunction recovers L pointwise by the concave biconjugation theorem.