noncomputable def helperForTheorem_38_5_threeVariableObjective {m n p : ℕ} (F : FiberwiseProperConvexBifunction m n) (G : FiberwiseProperConvexBifunction n p) (u : Fin m → ℝ) (x : Fin n → ℝ) (y : Fin p → ℝ) : EReal

Helper for Theorem 38.5: the textbook three-variable objective h(u, x, y) = F u x + G x y.

noncomputable def helperForTheorem_38_5_packedTripleObjective {m n p : ℕ} (F : FiberwiseProperConvexBifunction m n) (G : FiberwiseProperConvexBifunction n p) : (Fin (n + (m + p)) → ℝ) → EReal

Helper for Theorem 38.5: the same textbook objective packed onto ℝ^(n + (m + p)) so the middle block x can be eliminated by Theorem 5.7.

noncomputable def helperForTheorem_38_5_textbookPrimalMiddleFunction {m n : ℕ} (F : FiberwiseProperConvexBifunction m n) (uStar : Module.Dual ℝ (Fin m → ℝ)) : (Fin n → ℝ) → EReal

Helper for Theorem 38.5: the textbook function f(x) = inf_u {⟨u, u*⟩ - (F_* x)(u)}.

noncomputable def helperForTheorem_38_5_textbookDualMiddleFunction {n p : ℕ} (G : FiberwiseProperConvexBifunction n p) (yStar : Module.Dual ℝ (Fin p → ℝ)) : (Fin n → ℝ) → EReal

Helper for Theorem 38.5: the textbook function g(x) = sup_y {⟨y, y*⟩ - G x y}.

theorem helperForTheorem_38_5_dualLinearFunctional_properConvexFunctionOn_univ {m : ℕ} (uStar : Module.Dual ℝ (Fin m → ℝ)) : ProperConvexFunctionOn Set.univ fun (u : Fin m → ℝ) => ↑(uStar u)

Helper for Theorem 38.5: any real-valued linear functional, viewed as an EReal-valued function on ℝ^m, is proper convex on all of ℝ^m.

theorem helperForTheorem_38_5_textbookPrimalMiddleFunction_convexOn {m n : ℕ} (F : FiberwiseProperConvexBifunction m n) (uStar : Module.Dual ℝ (Fin m → ℝ)) (hF_properConvex : ProperConvexBifunction F.toFun) : ConvexFunctionOn Set.univ (helperForTheorem_38_5_textbookPrimalMiddleFunction F uStar)

Helper for Theorem 38.5: the textbook middle function x ↦ inf_u {⟨u, u*⟩ - (F_* x)(u)} is convex.

theorem helperForTheorem_38_5_textbookPrimalMiddleFunction_eq_iInf_inverse {m n : ℕ} (F : FiberwiseProperConvexBifunction m n) (uStar : Module.Dual ℝ (Fin m → ℝ)) (x : Fin n → ℝ) : helperForTheorem_38_5_textbookPrimalMiddleFunction F uStar x = ⨅ (u : Fin m → ℝ), ↑(uStar u) + -bifunctionInverse F.toFun x u

Helper for Theorem 38.5: rewrite the textbook f(x) through the inverse bifunction notation F_*.

theorem helperForTheorem_38_5_textbookPrimalMiddleFunction_negDual {m n : ℕ} (F : FiberwiseProperConvexBifunction m n) (uStar : Module.Dual ℝ (Fin m → ℝ)) (x : Fin n → ℝ) : helperForTheorem_38_5_textbookPrimalMiddleFunction F (-uStar) x = ⨅ (u : Fin m → ℝ), -↑(uStar u) + F.toFun u x

Helper for Theorem 38.5: the u-slice appearing in the fixed-x reduced problem is the primal middle function evaluated at -uStar.

theorem helperForTheorem_38_5_textbookDualMiddleFunction_eq_iSup {n p : ℕ} (G : FiberwiseProperConvexBifunction n p) (yStar : Module.Dual ℝ (Fin p → ℝ)) (x : Fin n → ℝ) : helperForTheorem_38_5_textbookDualMiddleFunction G yStar x = ⨆ (y : Fin p → ℝ), ↑(yStar y) - G.toFun x y

Helper for Theorem 38.5: rewrite the textbook g(x) in the explicit sup_y {⟨y, y*⟩ - G x y} form used in the original proof.

theorem helperForTheorem_38_5_neg_textbookDualMiddleFunction_negDual_eq_iInf {n p : ℕ} (G : FiberwiseProperConvexBifunction n p) (yStar : Module.Dual ℝ (Fin p → ℝ)) (x : Fin n → ℝ) : -helperForTheorem_38_5_textbookDualMiddleFunction G (-yStar) x = ⨅ (y : Fin p → ℝ), ↑(yStar y) + G.toFun x y

Helper for Theorem 38.5: negating the dual middle function at -yStar produces the y-side infimum inf_y {⟨y, y*⟩ + G x y} that occurs in the current sign convention for the adjoint.

noncomputable def helperForTheorem_38_5_middleReducedObjective {m n p : ℕ} (F : FiberwiseProperConvexBifunction m n) (G : FiberwiseProperConvexBifunction n p) (yStar : Module.Dual ℝ (Fin p → ℝ)) (uStar : Module.Dual ℝ (Fin m → ℝ)) : (Fin n → ℝ) → EReal

Helper for Theorem 38.5: the fixed-middle-variable reduced objective obtained after moving the outer minimization to the middle variable x.

noncomputable def helperForTheorem_38_5_secondShiftMiddleReducedObjective {m n p : ℕ} (F : FiberwiseProperConvexBifunction m n) (G : FiberwiseProperConvexBifunction n p) (yStar : Module.Dual ℝ (Fin p → ℝ)) (uStar : Module.Dual ℝ (Fin m → ℝ)) : (Fin n → ℝ) → (Fin n → ℝ) → EReal

Helper for Theorem 38.5: the original-text second-shift perturbation written as a partial infimum over the auxiliary primal/dual variables (u, y). This is the corrected object behind the guarded value function z ↦ inf_x (f x - g (x + z)).

theorem helperForTheorem_38_5_middleReducedObjective_eq_textbookPieces {m n p : ℕ} (F : FiberwiseProperConvexBifunction m n) (G : FiberwiseProperConvexBifunction n p) (yStar : Module.Dual ℝ (Fin p → ℝ)) (uStar : Module.Dual ℝ (Fin m → ℝ)) (x : Fin n → ℝ) (hPrimalFinite : ∃ (u : Fin m → ℝ), -↑(uStar u) + F.toFun u x < ⊤) (hDualFinite : ∃ (y : Fin p → ℝ), ↑(yStar y) + G.toFun x y < ⊤) : helperForTheorem_38_5_middleReducedObjective F G yStar uStar x = helperForTheorem_38_5_textbookPrimalMiddleFunction F (-uStar) x + -helperForTheorem_38_5_textbookDualMiddleFunction G (-yStar) x

Helper for Theorem 38.5: when the fixed-x primal and dual slices each admit one finite witness, the reduced middle-variable objective splits into the textbook f(x) - g(x) form.

theorem helperForTheorem_38_5_secondShiftMiddleReducedObjective_eq_textbookPieces {m n p : ℕ} (F : FiberwiseProperConvexBifunction m n) (G : FiberwiseProperConvexBifunction n p) (yStar : Module.Dual ℝ (Fin p → ℝ)) (uStar : Module.Dual ℝ (Fin m → ℝ)) (z x : Fin n → ℝ) (hPrimalFinite : ∃ (u : Fin m → ℝ), -↑(uStar u) + F.toFun u x < ⊤) (hDualFinite : ∃ (y : Fin p → ℝ), ↑(yStar y) + G.toFun (x + z) y < ⊤) : helperForTheorem_38_5_secondShiftMiddleReducedObjective F G yStar uStar z x = helperForTheorem_38_5_textbookPrimalMiddleFunction F (-uStar) x + -helperForTheorem_38_5_textbookDualMiddleFunction G (-yStar) (x + z)

Helper for Theorem 38.5: for fixed z, the corrected second-shift reduced objective splits as f(x) - g(x + z) once the primal slice at x and the dual slice at x + z both have a finite witness.

theorem helperForTheorem_38_5_neg_textbookDualMiddleFunction_negDual_convexOn {n p : ℕ} (G : FiberwiseProperConvexBifunction n p) (yStar : Module.Dual ℝ (Fin p → ℝ)) (hG_properConvex : ProperConvexBifunction G.toFun) : ConvexFunctionOn Set.univ fun (x : Fin n → ℝ) => -helperForTheorem_38_5_textbookDualMiddleFunction G (-yStar) x

Helper for Theorem 38.5: the convex function underlying the textbook g(x) = sup_y {⟨y, y*⟩ - G x y} is the negated slice at -yStar.

theorem helperForTheorem_38_5_adjoint_firstFactor_eq_neg_fenchelConjugate_textbookPrimal {m n : ℕ} (F : FiberwiseProperConvexBifunction m n) (xStar : Module.Dual ℝ (Fin n → ℝ)) (uStar : Module.Dual ℝ (Fin m → ℝ)) : bifunctionAdjoint F.toFun xStar uStar = -fenchelConjugate n (helperForTheorem_38_5_textbookPrimalMiddleFunction F (-uStar)) (-(dotProductEquiv ℝ (Fin n)).symm xStar)

Helper for Theorem 38.5: after identifying the middle dual variable with its Euclidean vector via dotProductEquiv, the left adjoint term F^*(x*, u*) is the negative Fenchel conjugate of the textbook primal middle function x ↦ inf_u {⟨u, -u*⟩ + F u x}.

theorem helperForTheorem_38_5_adjoint_secondFactor_eq_concaveFenchelConjugate_textbookDual {n p : ℕ} (G : FiberwiseProperConvexBifunction n p) (yStar : Module.Dual ℝ (Fin p → ℝ)) (xStar : Module.Dual ℝ (Fin n → ℝ)) : bifunctionAdjoint G.toFun yStar xStar = concaveFenchelConjugate (helperForTheorem_38_5_textbookDualMiddleFunction G (-yStar)) (-(dotProductEquiv ℝ (Fin n)).symm xStar)

Helper for Theorem 38.5: under the same Euclidean identification of the middle dual space, the right adjoint term G^*(y*, x*) is the concave Fenchel conjugate of the textbook dual middle function x ↦ sup_y {⟨y, -y*⟩ - G x y}.

theorem helperForTheorem_38_5_composeSupGeneric_eq_iSup_fenchelDualObjective {m n p : ℕ} (F : FiberwiseProperConvexBifunction m n) (G : FiberwiseProperConvexBifunction n p) (yStar : Module.Dual ℝ (Fin p → ℝ)) (uStar : Module.Dual ℝ (Fin m → ℝ)) : bifunctionComposeSupGeneric (bifunctionAdjoint F.toFun) (bifunctionAdjoint G.toFun) yStar uStar = ⨆ (xStar : Module.Dual ℝ (Fin n → ℝ)), fenchelDualObjective (helperForTheorem_38_5_textbookPrimalMiddleFunction F (-uStar)) (helperForTheorem_38_5_textbookDualMiddleFunction G (-yStar)) (-(dotProductEquiv ℝ (Fin n)).symm xStar)

Helper for Theorem 38.5: after rewriting both adjoint factors through the textbook middle functions, the supremum composition F^* G^* becomes the Fenchel dual supremum of that pair, still indexed by middle dual vectors via dotProductEquiv.

theorem helperForTheorem_38_5_textbookPrimalMiddleFunction_effectiveDomain {m n : ℕ} (F : FiberwiseProperConvexBifunction m n) (uStar : Module.Dual ℝ (Fin m → ℝ)) : effectiveDomain Set.univ (helperForTheorem_38_5_textbookPrimalMiddleFunction F uStar) = bifunctionDomBot (bifunctionInverse F.toFun)

Helper for Theorem 38.5: the textbook primal middle function has exactly the domain dom F_*, i.e. those x for which some u makes F u x different from ⊤.

theorem helperForTheorem_38_5_textbookDualMiddleFunction_concaveEffectiveDomain {n p : ℕ} (G : FiberwiseProperConvexBifunction n p) (yStar : Module.Dual ℝ (Fin p → ℝ)) : concaveEffectiveDomain (helperForTheorem_38_5_textbookDualMiddleFunction G yStar) = bifunctionDom G.toFun

Helper for Theorem 38.5: the textbook dual middle function has book concave effective domain exactly dom G. Equivalently, -g(x) is finite from above exactly when some y makes G x y different from ⊤.

theorem helperForTheorem_38_5_hri_implies_fenchelConditionA {m n p : ℕ} (F : FiberwiseProperConvexBifunction m n) (G : FiberwiseProperConvexBifunction n p) (yStar : Module.Dual ℝ (Fin p → ℝ)) (uStar : Module.Dual ℝ (Fin m → ℝ)) (hri : (intrinsicInterior ℝ (bifunctionDomBot (bifunctionInverse F.toFun)) ∩ intrinsicInterior ℝ (bifunctionDom G.toFun)).Nonempty) : FenchelConditionA (helperForTheorem_38_5_textbookPrimalMiddleFunction F (-uStar)) (helperForTheorem_38_5_textbookDualMiddleFunction G (-yStar))

Helper for Theorem 38.5: the qualification hypothesis stated with intrinsic interiors of dom F_* and dom G is exactly Fenchel's condition (a) for the textbook middle functions.

theorem helperForTheorem_38_5_middleReducedObjective_eq_commonBookEffectiveDomainDifference {m n p : ℕ} (F : FiberwiseProperConvexBifunction m n) (G : FiberwiseProperConvexBifunction n p) (yStar : Module.Dual ℝ (Fin p → ℝ)) (uStar : Module.Dual ℝ (Fin m → ℝ)) (x : Fin n → ℝ) : helperForTheorem_38_5_middleReducedObjective F G yStar uStar x = commonBookEffectiveDomainDifference (helperForTheorem_38_5_textbookPrimalMiddleFunction F (-uStar)) (helperForTheorem_38_5_textbookDualMiddleFunction G (-yStar)) x

Helper for Theorem 38.5: the reduced middle-variable objective is exactly the Chapter 31 primal objective commonBookEffectiveDomainDifference f g built from the textbook middle functions f(x) = inf_u {⟨u, -u*⟩ + F u x} and g(x) = sup_y {⟨y, -y*⟩ - G x y}.