noncomputable def firstVariableDirectionalDerivativeFunction {m n : ℕ} (K : (Fin m → ℝ) → (Fin n → ℝ) → EReal) (u : Fin m → ℝ) (v : Fin n → ℝ) : (Fin m → ℝ) → EReal

The first-variable directional derivative function attached to a saddle kernel at (u, v), defined by u' ↦ -K'(u, v; -u', 0) using the infimum of all admissible directional-derivative values.

noncomputable def saddleLowerSemicontinuousHull {α : Type u_1} [TopologicalSpace α] (f : α → EReal) : α → EReal

The lower semicontinuous hull of an extended-real-valued function, realized by the closure of its epigraph.

noncomputable def supportFunctionOfSet {m : ℕ} (S : Set (Fin m → ℝ)) : (Fin m → ℝ) → EReal

The support function of a set of vectors in ℝ^m, viewed as an extended-real-valued function on ℝ^m.

theorem helperForText_35_6_6_reflectedFirstSlice_convex {m n : ℕ} {K : (Fin m → ℝ) → (Fin n → ℝ) → EReal} (hSaddle : IsGloballyConcaveConvexERealKernel K) (v : Fin n → ℝ) : ConvexFunction fun (x : Fin m → ℝ) => -K (-x) v

Helper for Text 35.6.6: the reflected first slice x ↦ -K (-x) v is convex, because the saddle hypothesis already gives convexity of x ↦ -K x v and the involution x ↦ -x is linear.

theorem helperForText_35_6_6_reflectedFirstSlice_finiteAtBase {m n : ℕ} {K : (Fin m → ℝ) → (Fin n → ℝ) → EReal} {u : Fin m → ℝ} {v : Fin n → ℝ} (hFinite : K u v ≠ ⊤ ∧ K u v ≠ ⊥) : (fun (x : Fin m → ℝ) => -K (-x) v) (-u) ≠ ⊤ ∧ (fun (x : Fin m → ℝ) => -K (-x) v) (-u) ≠ ⊥

Helper for Text 35.6.6: recentering the first slice at -u does not change the finiteness of the base value, because the reflected slice still evaluates to -K u v.

theorem helperForText_35_6_6_recenteredFirstSlice_directionalDerivative {m n : ℕ} {K : (Fin m → ℝ) → (Fin n → ℝ) → EReal} (hSaddle : IsGloballyConcaveConvexERealKernel K) {u : Fin m → ℝ} {v : Fin n → ℝ} (hFinite : K u v ≠ ⊤ ∧ K u v ≠ ⊥) (u' : Fin m → ℝ) : firstVariableDirectionalDerivativeFunction K u v u' = upperDirectionalDerivativeAt (fun (x : Fin m → ℝ) => -K (-x) v) (-u) u'

Helper for Text 35.6.6: after recentering the first slice by x ↦ -x, the textbook first-variable directional derivative function is exactly the ordinary upper directional derivative of the convex slice x ↦ -K (-x) v at the base point -u.

theorem helperForText_35_6_6_firstVariableDirectionalDerivative_eq_upperDirectionalDerivative {m n : ℕ} {K : (Fin m → ℝ) → (Fin n → ℝ) → EReal} (hSaddle : IsGloballyConcaveConvexERealKernel K) {u : Fin m → ℝ} {v : Fin n → ℝ} (hFinite : K u v ≠ ⊤ ∧ K u v ≠ ⊥) : firstVariableDirectionalDerivativeFunction K u v = upperDirectionalDerivativeAt (fun (x : Fin m → ℝ) => -K (-x) v) (-u)

Helper for Text 35.6.6: the whole textbook first-variable directional-derivative function is exactly the Chapter 23 directional derivative of the reflected first slice at -u.

theorem helperForText_35_6_6_reflectedSliceSubgradient_iff_partialFirstMem {m n : ℕ} {K : (Fin m → ℝ) → (Fin n → ℝ) → EReal} {u : Fin m → ℝ} {v : Fin n → ℝ} {uStar : Fin m → ℝ} : (dotProductEquiv ℝ (Fin m)) uStar ∈ subdifferentialAt (fun (x : Fin m → ℝ) => -K (-x) v) (-u) ↔ uStar ∈ partialSubdifferentialInFirstVariable K u v

Helper for Text 35.6.6: membership in the Euclidean subdifferential of the reflected slice is exactly the textbook first-partial supporting inequality.

theorem helperForText_35_6_6_partialFirst_eq_sliceSubdifferential {m n : ℕ} {K : (Fin m → ℝ) → (Fin n → ℝ) → EReal} {u : Fin m → ℝ} {v : Fin n → ℝ} : ⇑(dotProductEquiv ℝ (Fin m)) ⁻¹' subdifferentialAt (fun (x : Fin m → ℝ) => -K (-x) v) (-u) = partialSubdifferentialInFirstVariable K u v

Helper for Text 35.6.6: the Euclidean subdifferential of the recentered convex slice x ↦ -K (-x) v at -u is exactly the first partial subdifferential ∂₁ K(u, v).

theorem helperForText_35_6_6_supportFunctionOfSet_eq_supportFunctionEReal {m : ℕ} (S : Set (Fin m → ℝ)) : supportFunctionEReal S = supportFunctionOfSet S

Helper for Text 35.6.6: after identifying the slice subdifferential with ∂₁ K(u, v), the Chapter 23 support value is exactly the textbook support function of the first partial subdifferential.

theorem helperForText_35_6_6_sliceSupport_eq_firstPartialSupport {m n : ℕ} {K : (Fin m → ℝ) → (Fin n → ℝ) → EReal} {u : Fin m → ℝ} {v : Fin n → ℝ} : subdifferentialSupportAt (fun (x : Fin m → ℝ) => -K (-x) v) (-u) = supportFunctionOfSet (partialSubdifferentialInFirstVariable K u v)

Helper for Text 35.6.6: after identifying the slice subdifferential with ∂₁ K(u, v), the Chapter 23 support value is exactly the textbook support function of the first partial subdifferential.

theorem helperForText_35_6_6_mem_closure_inter_open_iff {α : Type u_1} [TopologicalSpace α] {s t : Set α} {x : α} (hx : x ∈ t) (ht : IsOpen t) : x ∈ closure s ↔ x ∈ closure (s ∩ t)

Helper for Text 35.6.6: restricting a closure computation to an open neighborhood of the base point does not change membership, so localizing to the finite-height EReal range is legitimate.

theorem helperForText_35_6_6_realHeight_mem_saddleClosure_iff_realEpigraphClosure {m : ℕ} (φ : (Fin m → ℝ) → EReal) (x : Fin m → ℝ) (r : ℝ) : (x, ↑r) ∈ closure {p : (Fin m → ℝ) × EReal | φ p.1 ≤ p.2} ↔ (x, r) ∈ closure (epigraph Set.univ φ)

Helper for Text 35.6.6: a finite EReal height lies in the closure of the full EReal epigraph exactly when the corresponding real height lies in the closure of the ordinary real epigraph.

theorem helperForText_35_6_6_saddleClosure_upwardInSecondCoordinate {m : ℕ} {φ : (Fin m → ℝ) → EReal} {x : Fin m → ℝ} {μ ν : EReal} (hμν : μ ≤ ν) (hx : (x, μ) ∈ closure {p : (Fin m → ℝ) × EReal | φ p.1 ≤ p.2}) : (x, ν) ∈ closure {p : (Fin m → ℝ) × EReal | φ p.1 ≤ p.2}

Helper for Text 35.6.6: the closure of the full EReal epigraph remains upward closed in the second coordinate.

theorem helperForText_35_6_6_saddleLowerHull_eq_epigraphClosureInf {m : ℕ} (φ : (Fin m → ℝ) → EReal) : saddleLowerSemicontinuousHull φ = epigraphClosureInf φ

Helper for Text 35.6.6: the EReal epigraph hull used for saddle kernels is exactly the Chapter 2 vertical-slice infimum epigraphClosureInf.

theorem helperForText_35_6_6_epigraphClosureInf_eq_lowerSemicontinuousHull {m : ℕ} (φ : (Fin m → ℝ) → EReal) : epigraphClosureInf φ = lowerSemicontinuousHull φ

Helper for Text 35.6.6: the closure-by-epigraph construction epigraphClosureInf is exactly the ordinary lower semicontinuous hull.

theorem helperForText_35_6_6_epigraphClosureInf_eq_convexFunctionClosure_of_no_bot {m : ℕ} {D : (Fin m → ℝ) → EReal} (hnotbot : ∀ (y : Fin m → ℝ), D y ≠ ⊥) : epigraphClosureInf D = convexFunctionClosure D

Helper for Text 35.6.6: when the directional-derivative function never takes the value ⊥, its epigraph hull agrees with the Chapter 2 convex closure.

theorem helperForText_35_6_6_epigraphClosureInf_eq_bot_of_dense_effectiveDomain {m : ℕ} {D : (Fin m → ℝ) → EReal} (hImproper : ImproperConvexFunctionOn Set.univ D) (hBot : ∃ (y : Fin m → ℝ), D y = ⊥) (hDense : closure (effectiveDomain Set.univ D) = Set.univ) : epigraphClosureInf D = fun (x : Fin m → ℝ) => ⊥

Helper for Text 35.6.6: if an improper convex function attains ⊥ and its effective domain is dense, then the epigraph-closure hull is the constant ⊥ function.

theorem helperForText_35_6_6_denseEffectiveDomain_of_dense_reflectedSliceDomain {m : ℕ} {g : (Fin m → ℝ) → EReal} {x : Fin m → ℝ} (hg : ConvexFunction g) (hx : g x ≠ ⊤ ∧ g x ≠ ⊥) (hDense : closure (effectiveDomain Set.univ g) = Set.univ) : closure (effectiveDomain Set.univ (upperDirectionalDerivativeAt g x)) = Set.univ

Helper for Text 35.6.6: once the reflected convex slice g has dense effective domain, the relative-interior transport from Theorem 23.3 forces the effective domain of its directional derivative y ↦ g'(x; y) to be dense as well.

theorem helperForText_35_6_6_epigraphClosureInf_eq_bot_of_empty_sliceSubdifferential_of_dense_reflectedSliceDomain {m : ℕ} {g : (Fin m → ℝ) → EReal} {x : Fin m → ℝ} (hg : ConvexFunction g) (hx : g x ≠ ⊤ ∧ g x ≠ ⊥) (hsubEmpty : subdifferentialAt g x = ∅) (hDense : closure (effectiveDomain Set.univ g) = Set.univ) : epigraphClosureInf (upperDirectionalDerivativeAt g x) = fun (x : Fin m → ℝ) => ⊥

Helper for Text 35.6.6: once the reflected slice g has dense effective domain, the empty subdifferential branch collapses epigraphClosureInf (g'(x; ·)) to the constant ⊥ function.

theorem helperForText_35_6_6_epigraphClosureInf_eq_sliceSupport_of_nonempty_sliceSubdifferential {m : ℕ} {g : (Fin m → ℝ) → EReal} {x : Fin m → ℝ} (hg : ConvexFunction g) (hx : g x ≠ ⊤ ∧ g x ≠ ⊥) (hsub : (subdifferentialAt g x).Nonempty) : epigraphClosureInf (upperDirectionalDerivativeAt g x) = subdifferentialSupportAt g x

Helper for Text 35.6.6: if the reflected slice subdifferential is nonempty, then the Chapter 2 epigraph hull of the slice directional derivative already matches the Chapter 23 support formula.

theorem helperForText_35_6_6_sliceSupport_eq_bot_of_empty_sliceSubdifferential {m : ℕ} {g : (Fin m → ℝ) → EReal} {x : Fin m → ℝ} (hsubEmpty : subdifferentialAt g x = ∅) : subdifferentialSupportAt g x = fun (x : Fin m → ℝ) => ⊥

Helper for Text 35.6.6: if the reflected slice subdifferential is empty, then the Chapter 23 support function is the constant ⊥ function.

theorem helperForText_35_6_6_partialFirst_nonempty_iff_sliceSubdifferential_nonempty {m n : ℕ} {K : (Fin m → ℝ) → (Fin n → ℝ) → EReal} {u : Fin m → ℝ} {v : Fin n → ℝ} : (partialSubdifferentialInFirstVariable K u v).Nonempty ↔ (subdifferentialAt (fun (x : Fin m → ℝ) => -K (-x) v) (-u)).Nonempty

Helper for Text 35.6.6: nonemptiness of the textbook first partial subdifferential is equivalent to nonemptiness of the Euclidean subdifferential of the reflected slice.

theorem helperForText_35_6_6_firstPartialSupport_eq_bot_of_empty_partialFirst {m n : ℕ} {K : (Fin m → ℝ) → (Fin n → ℝ) → EReal} {u : Fin m → ℝ} {v : Fin n → ℝ} (hpartialEmpty : partialSubdifferentialInFirstVariable K u v = ∅) : supportFunctionOfSet (partialSubdifferentialInFirstVariable K u v) = fun (x : Fin m → ℝ) => ⊥

Helper for Text 35.6.6: if ∂₁ K(u, v) is empty, then its textbook support function is the constant ⊥ function.

theorem helperForText_35_6_6_eq_firstPartialSupport_iff_eq_bot_of_empty_partialFirst {m n : ℕ} {K : (Fin m → ℝ) → (Fin n → ℝ) → EReal} {u : Fin m → ℝ} {v : Fin n → ℝ} (φ : (Fin m → ℝ) → EReal) (hpartialEmpty : partialSubdifferentialInFirstVariable K u v = ∅) : φ = supportFunctionOfSet (partialSubdifferentialInFirstVariable K u v) ↔ φ = fun (x : Fin m → ℝ) => ⊥

Helper for Text 35.6.6: on the empty first-partial branch, identifying any candidate hull with the textbook support function is equivalent to showing that the candidate hull is constantly ⊥.

theorem helperForText_35_6_6_convexFunctionClosure_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: Theorem 23.2 identifies the convex closure of the textbook first-variable directional derivative with the support function of ∂₁ K(u, v). This is the mathematically correct closure statement available even before comparing with the stronger lower-semicontinuous hull used later in the textbook phrasing.

theorem helperForText_35_6_6_convexFunctionClosure_eq_bot_of_empty_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 ≠ ⊥) (hpartialEmpty : partialSubdifferentialInFirstVariable K u v = ∅) : convexFunctionClosure (firstVariableDirectionalDerivativeFunction K u v) = fun (x : Fin m → ℝ) => ⊥

Helper for Text 35.6.6: when ∂₁ K(u, v) is empty, the correct Chapter 23 conclusion is that the convex closure of the textbook directional-derivative function is constantly ⊥. This does not by itself imply the stronger epigraphClosureInf endpoint used in the remaining blocked branch.