theorem helperForText_35_6_6_saddleLowerHull_eq_firstPartialSupport_of_nonempty_partialFirst {m n : ℕ} {K : (Fin m → ℝ) → (Fin n → ℝ) → EReal} (hSaddle : IsGloballyConcaveConvexERealKernel K) {u : Fin m → ℝ} {v : Fin n → ℝ} (hFinite : K u v ≠ ⊤ ∧ K u v ≠ ⊥) (hpartial : (partialSubdifferentialInFirstVariable K u v).Nonempty) : saddleLowerSemicontinuousHull (firstVariableDirectionalDerivativeFunction K u v) = supportFunctionOfSet (partialSubdifferentialInFirstVariable K u v)

Helper for Text 35.6.6: the textbook hull/support identity is correct on the honest branch where the first partial subdifferential is nonempty.

theorem helperForText_35_6_6_saddleLowerHull_eq_firstPartialSupport {m n : ℕ} {K : (Fin m → ℝ) → (Fin n → ℝ) → EReal} (hSaddle : IsGloballyConcaveConvexERealKernel K) {u : Fin m → ℝ} {v : Fin n → ℝ} (hFinite : K u v ≠ ⊤ ∧ K u v ≠ ⊥) : convexFunctionClosure (firstVariableDirectionalDerivativeFunction K u v) = supportFunctionOfSet (partialSubdifferentialInFirstVariable K u v)

Helper for Text 35.6.6: the mathematically correct Chapter 23 closure statement identifies the convex closure of the first directional-derivative slice with the support function of ∂₁ K(u,v).

theorem section35_text35_6_6 {m n : ℕ} {K : (Fin m → ℝ) → (Fin n → ℝ) → EReal} (hSaddle : IsGloballyConcaveConvexERealKernel K) {u : Fin m → ℝ} {v : Fin n → ℝ} (hFinite : K u v ≠ ⊤ ∧ K u v ≠ ⊥) : ConvexFunction (firstVariableDirectionalDerivativeFunction K u v) ∧ ∀ (u' : Fin m → ℝ), convexFunctionClosure (firstVariableDirectionalDerivativeFunction K u v) u' = supportFunctionOfSet (partialSubdifferentialInFirstVariable K u v) u'

Text 35.6.6: let K be a saddle function on ℝ^m × ℝ^n, and let (u, v) be a point with finite value K u v. Define φ(u') = -K'(u, v; -u', 0). Then φ is a convex function on ℝ^m, and the convex closure of φ coincides with the support function of the closed convex set ∂₁ K(u, v).