noncomputable def helperForTheorem_37_4_affineTiltKernel {m n : ℕ} (K : SaddleFunction m n) (uStar : Fin m → ℝ) (vStar : Fin n → ℝ) : SaddleFunction m n

Helper for Theorem 37.4: this is the affine tilt K - ⟨\cdot,u^*⟩ - ⟨\cdot,v^*⟩ whose saddle points characterize productSubdifferentialAt K u v.

theorem helperForTheorem_37_4_coe_firstPartialIncrement_eq_finDot_sub {m : ℕ} (u u' uStar : Fin m → ℝ) : ↑(∑ i : Fin m, uStar i * (u' i - u i)) = ↑(finDot u' uStar - finDot u uStar)

Helper for Theorem 37.4: the first-variable partial increment is the difference of the two corresponding dot products.

theorem helperForTheorem_37_4_coe_secondPartialIncrement_eq_finDot_sub {n : ℕ} (v v' vStar : Fin n → ℝ) : ↑(∑ i : Fin n, vStar i * (v' i - v i)) = ↑(finDot v' vStar - finDot v vStar)

Helper for Theorem 37.4: the second-variable partial increment is the difference of the two corresponding dot products.

theorem helperForTheorem_37_4_mem_euclideanRelativeInterior_fin_of_mem_intrinsicInterior {k : ℕ} {C : Set (Fin k → ℝ)} {x : Fin k → ℝ} (hx : x ∈ intrinsicInterior ℝ C) : x ∈ euclideanRelativeInterior_fin k C

Helper for Theorem 37.4: on Fin k → ℝ, intrinsic-interior points are also points of the transported Euclidean relative interior.

theorem helperForTheorem_37_4_sumERealProducts_eq_coe_sum {k : ℕ} (a x y : Fin k → ℝ) : ∑ i : Fin k, ↑(a i) * ↑(x i - y i) = ↑(∑ i : Fin k, a i * (x i - y i))

Helper for Theorem 37.4: the EReal sum of coordinatewise affine products is the coercion of the corresponding real sum.

theorem helperForTheorem_37_4_sumERealProducts_subtractedCoordinates_eq_coe_sum {k : ℕ} (a x y : Fin k → ℝ) : ∑ i : Fin k, ↑(a i) * (↑(x i) - ↑(y i)) = ↑(∑ i : Fin k, a i * (x i - y i))

Helper for Theorem 37.4: the coordinatewise EReal products that occur after unfolding the partial subdifferentials sum to the same coerced real affine increment.

theorem helperForTheorem_37_4_mem_productSubdifferential_iff_saddlePoint_affineTilt {m n : ℕ} (K : SaddleFunction m n) (u : Fin m → ℝ) (v : Fin n → ℝ) (uStar : Fin m → ℝ) (vStar : Fin n → ℝ) : (uStar, vStar) ∈ productSubdifferentialAt K u v ↔ IsSaddlePoint (helperForTheorem_37_4_affineTiltKernel K uStar vStar) u v

Helper for Theorem 37.4: membership in the product subdifferential is exactly the saddle-point condition for the affine tilt by (uStar, vStar).

theorem helperForTheorem_37_4_nonempty_productSubdifferential_of_mem_saddleKernelDomain {m n : ℕ} (K : SaddleFunction m n) (hKclosed : IsClosedSaddleFunction K) (hKproper : IsProperSaddleFunction K) (hGlobal : Section34Theorem34_2GlobalQualification m n) {u : Fin m → ℝ} {v : Fin n → ℝ} (huv : (u, v) ∈ saddleKernelDomain K) : (productSubdifferentialAt K u v).Nonempty

Helper for Theorem 37.4: a closed proper saddle-function has nonempty product subdifferential at every point of ri (dom K).

theorem helperForTheorem_37_4_mem_saddleEffectiveDomain_of_nonempty_productSubdifferential {m n : ℕ} (K : SaddleFunction m n) (hKproper : IsProperSaddleFunction K) {u : Fin m → ℝ} {v : Fin n → ℝ} (hSub : (productSubdifferentialAt K u v).Nonempty) : (u, v) ∈ saddleEffectiveDomain K

Helper for Theorem 37.4: for a proper saddle-function, any nonempty product subdifferential can only occur on dom K = dom₁ K × dom₂ K.

theorem section37_theorem37_4 {m n : ℕ} (K : SaddleFunction m n) (hKclosed : IsClosedSaddleFunction K) (hKproper : IsProperSaddleFunction K) (hGlobal : Section34Theorem34_2GlobalQualification m n) : (∀ (u : Fin m → ℝ) (v : Fin n → ℝ) (uStar : Fin m → ℝ) (vStar : Fin n → ℝ), (uStar, vStar) ∈ productSubdifferentialAt K u v ↔ IsSaddlePoint (helperForTheorem_37_4_affineTiltKernel K uStar vStar) u v) ∧ saddleKernelDomain K ⊆ {p : (Fin m → ℝ) × (Fin n → ℝ) | (productSubdifferentialAt K p.1 p.2).Nonempty} ∧ {p : (Fin m → ℝ) × (Fin n → ℝ) | (productSubdifferentialAt K p.1 p.2).Nonempty} ⊆ saddleEffectiveDomain K

Theorem 37.4: a pair (uStar, vStar) lies in ∂K(u, v) exactly when the affine tilt K - ⟨\cdot,u^*⟩ - ⟨\cdot,v^*⟩ has (u, v) as a saddle point; for closed proper K one has ri (dom K) ⊆ dom ∂K ⊆ dom K.

theorem helperForCorollary_37_4_1_equivalentSaddleFunctions_symm {m n : ℕ} {K L : SaddleFunction m n} (hKL : EquivalentSaddleFunctions K L) : EquivalentSaddleFunctions L K

Helper for Corollary 37.4.1: equivalence of saddle-functions is symmetric.

theorem helperForCorollary_37_4_1_mem_originalSaddleDom_of_isSaddlePoint_affineTilt {m n : ℕ} {K L : SaddleFunction m n} (hKL : EquivalentSaddleFunctions K L) {u : Fin m → ℝ} {v : Fin n → ℝ} {uStar : Fin m → ℝ} {vStar : Fin n → ℝ} (hSaddle : IsSaddlePoint (helperForTheorem_37_4_affineTiltKernel K uStar vStar) u v) : u ∈ saddleDom1 K ∧ v ∈ saddleDom2 K

Helper for Corollary 37.4.1: a saddle point of the affine tilt can occur only at a point of the original common saddle domain.

theorem helperForCorollary_37_4_1_affineTilt_eq_on_row_of_mem_saddleDom2 {m n : ℕ} {K L : SaddleFunction m n} {uStar : Fin m → ℝ} {vStar : Fin n → ℝ} (hKL : EquivalentSaddleFunctions K L) {v : Fin n → ℝ} (hv : v ∈ saddleDom2 K) (u : Fin m → ℝ) : helperForTheorem_37_4_affineTiltKernel K uStar vStar u v = helperForTheorem_37_4_affineTiltKernel L uStar vStar u v

Helper for Corollary 37.4.1: once the second coordinate lies in the common saddle domain, the affine tilts of equivalent saddle-functions agree on the whole corresponding row.

theorem helperForCorollary_37_4_1_affineTilt_eq_on_col_of_mem_saddleDom1 {m n : ℕ} {K L : SaddleFunction m n} {uStar : Fin m → ℝ} {vStar : Fin n → ℝ} (hKL : EquivalentSaddleFunctions K L) {u : Fin m → ℝ} (hu : u ∈ saddleDom1 K) (v : Fin n → ℝ) : helperForTheorem_37_4_affineTiltKernel K uStar vStar u v = helperForTheorem_37_4_affineTiltKernel L uStar vStar u v

Helper for Corollary 37.4.1: once the first coordinate lies in the common saddle domain, the affine tilts of equivalent saddle-functions agree on the whole corresponding column.

theorem helperForCorollary_37_4_1_saddlePoint_affineTilt_transport {m n : ℕ} {K L : SaddleFunction m n} (hKL : EquivalentSaddleFunctions K L) {u : Fin m → ℝ} {v : Fin n → ℝ} {uStar : Fin m → ℝ} {vStar : Fin n → ℝ} (hSaddle : IsSaddlePoint (helperForTheorem_37_4_affineTiltKernel K uStar vStar) u v) : IsSaddlePoint (helperForTheorem_37_4_affineTiltKernel L uStar vStar) u v

Helper for Corollary 37.4.1: if one affine tilt has a saddle point at (u,v), the corresponding affine tilt of an equivalent saddle-function has the same saddle point.

theorem helperForCorollary_37_4_1_saddlePoint_affineTilt_iff_of_equivalentSaddleFunctions {m n : ℕ} {K L : SaddleFunction m n} (hKL : EquivalentSaddleFunctions K L) (u : Fin m → ℝ) (v : Fin n → ℝ) (uStar : Fin m → ℝ) (vStar : Fin n → ℝ) : IsSaddlePoint (helperForTheorem_37_4_affineTiltKernel K uStar vStar) u v ↔ IsSaddlePoint (helperForTheorem_37_4_affineTiltKernel L uStar vStar) u v

Helper for Corollary 37.4.1: the affine-tilt saddle-point predicate is identical for equivalent saddle-functions.

theorem helperForCorollary_37_4_1_productSubdifferential_eq_of_equivalentSaddleFunctions {m n : ℕ} {K L : SaddleFunction m n} (hKL : EquivalentSaddleFunctions K L) (u : Fin m → ℝ) (v : Fin n → ℝ) : productSubdifferentialAt K u v = productSubdifferentialAt L u v

Helper for Corollary 37.4.1: equivalent saddle-functions have the same product subdifferential at every point.

theorem helperForCorollary_37_4_1_value_eq_on_productSubdifferentialDomain {m n : ℕ} {K L : SaddleFunction m n} (hKL : EquivalentSaddleFunctions K L) (u : Fin m → ℝ) (v : Fin n → ℝ) : (productSubdifferentialAt K u v).Nonempty → K u v = L u v

Helper for Corollary 37.4.1: on every point where the product subdifferential is nonempty, equivalent saddle-functions already agree in value.

theorem corollary37_4_1_equivalentSaddleFunctions_have_same_productSubdifferential {m n : ℕ} {K L : SaddleFunction m n} (hKL : EquivalentSaddleFunctions K L) : (∀ (u : Fin m → ℝ) (v : Fin n → ℝ), productSubdifferentialAt K u v = productSubdifferentialAt L u v) ∧ {p : (Fin m → ℝ) × (Fin n → ℝ) | (productSubdifferentialAt K p.1 p.2).Nonempty} = {p : (Fin m → ℝ) × (Fin n → ℝ) | (productSubdifferentialAt L p.1 p.2).Nonempty} ∧ ∀ (u : Fin m → ℝ) (v : Fin n → ℝ), (productSubdifferentialAt K u v).Nonempty → K u v = L u v

Corollary 37.4.1: equivalent saddle-functions have the same product subdifferential, and their values agree on the common domain where this product subdifferential is nonempty.

def helperForCorollary_37_5_1_productSubdifferentialGraph {m n : ℕ} (K : SaddleFunction m n) : Set (((Fin m → ℝ) × (Fin n → ℝ)) × (Fin m → ℝ) × (Fin n → ℝ))

Helper for Corollary 37.5.1: the graph of the product subdifferential of K, written in the four-block coordinates (u, v, uStar, vStar).

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

Helper for Corollary 37.5.1: the textbook map sending a graph point (u, v, uStar, vStar) to (u - uStar, v + vStar).

theorem helperForCorollary_37_5_1_appendHomeomorph_bookMap_eq_packedAddition {m n : ℕ} (u : Fin m → ℝ) (v : Fin n → ℝ) (uStar : Fin m → ℝ) (vStar : Fin n → ℝ) : (Fin.appendHomeomorph m n) (helperForCorollary_37_5_1_bookMap ((u, v), uStar, vStar)) = Fin.append u v + Fin.append (-uStar) vStar

Helper for Corollary 37.5.1: after packing the primal variables with Fin.append, the textbook map becomes the packed addition map with the first dual block sign-twisted.

theorem helperForCorollary_37_5_1_bookMap_eq_appendHomeomorph_symm_packedAddition {m n : ℕ} (u : Fin m → ℝ) (v : Fin n → ℝ) (uStar : Fin m → ℝ) (vStar : Fin n → ℝ) : helperForCorollary_37_5_1_bookMap ((u, v), uStar, vStar) = (Fin.appendHomeomorph m n).symm (Fin.append u v + Fin.append (-uStar) vStar)

Helper for Corollary 37.5.1: unpacking the packed addition map recovers exactly the textbook map (u - uStar, v + vStar).

def helperForCorollary_37_5_1_packGraphCoordinates {m n : ℕ} : ((Fin m → ℝ) × (Fin n → ℝ)) × (Fin m → ℝ) × (Fin n → ℝ) → (Fin (m + n) → ℝ) × (Fin (m + n) → ℝ)

Helper for Corollary 37.5.1: package the four-block graph coordinates (u, v, uStar, vStar) into the corrected packed coordinates ((u, vStar), (-uStar, v)).

def helperForCorollary_37_5_1_packedSubdifferentialGraph {m n : ℕ} (F : (Fin m → ℝ) → (Fin n → ℝ) → EReal) : Set ((Fin (m + n) → ℝ) × (Fin (m + n) → ℝ))

Helper for Corollary 37.5.1: this is the ordinary subdifferential graph of the packed graph function attached to a convex bifunction.

theorem helperForCorollary_37_5_1_packGraphCoordinates_continuous {m n : ℕ} : Continuous helperForCorollary_37_5_1_packGraphCoordinates

Helper for Corollary 37.5.1: the packed coordinate swap/sign map is continuous, so closedness can be transported by preimages once the graph-bridge is known.

theorem helperForCorollary_37_5_1_graphFunction_properConvex {m n : ℕ} {F : (Fin m → ℝ) → (Fin n → ℝ) → EReal} (hF : IsClosedConvexBifunction F) (hFproper : IsProperConvexBifunction F) : ProperConvexFunctionOn Set.univ (graphFunctionOfBifunction F)

Helper for Corollary 37.5.1: a closed proper convex bifunction gives a closed proper packed convex graph function on ℝ^(m+n).

def Section37ClosedRepresentativeQualification {m n : ℕ} (K : SaddleFunction m n) (hKclosed : IsClosedSaddleFunction K) : Prop

Explicit infinite-value qualification needed by the canonical Section 34 witness route used to recover a graph-closed convex representative.

theorem helperForCorollary_37_5_1_closedProperRepresentativeWithClosedWitness {m n : ℕ} (K : SaddleFunction m n) (hKclosed : IsClosedSaddleFunction K) (hKproper : IsProperSaddleFunction K) (hRepresentative : Section37ClosedRepresentativeQualification K hKclosed) (hGlobal : Section34Theorem34_2GlobalQualification m n) : ∃ (F : (Fin m → ℝ) → (Fin n → ℝ) → EReal) (hF : IsClosedConvexBifunction F), ClosedConvexBifunction F ∧ IsProperConvexBifunction F ∧ K ∈ EquivalenceClassGeneratedByConvexBifunction ⟨F, hF⟩

Helper for Corollary 37.5.1: a closed proper saddle-function admits a representative that is closed in the Chapter 6 graph-function sense as well as proper in the Section 34 image-closed sense.

theorem helperForCorollary_37_5_1_graphFunction_closedProperConvex {m n : ℕ} {F : (Fin m → ℝ) → (Fin n → ℝ) → EReal} (hF : IsClosedConvexBifunction F) (hClosed : ClosedConvexBifunction F) (hFproper : IsProperConvexBifunction F) : ClosedConvexFunction (graphFunctionOfBifunction F) ∧ ProperConvexFunctionOn Set.univ (graphFunctionOfBifunction F)

Helper for Corollary 37.5.1: a closed proper convex bifunction gives a closed proper packed convex graph function on ℝ^(m+n).

theorem helperForCorollary_37_5_1_generatedClass_gives_saddleEquivalent {m n : ℕ} (K : SaddleFunction m n) {F : (Fin m → ℝ) → (Fin n → ℝ) → EReal} (hF : IsClosedConvexBifunction F) (hKGenerated : K ∈ EquivalenceClassGeneratedByConvexBifunction ⟨F, hF⟩) : saddleEquivalent K (convexBifunctionPairing F)

Helper for Corollary 37.5.1: generated-class membership is exactly saddle-equivalence with the canonical pairing kernel of the representing convex bifunction.

theorem helperForCorollary_37_5_1_packGraphCoordinates_homeomorph {m n : ℕ} : ∃ (e : ((Fin m → ℝ) × (Fin n → ℝ)) × (Fin m → ℝ) × (Fin n → ℝ) ≃ₜ (Fin (m + n) → ℝ) × (Fin (m + n) → ℝ)), ∀ (p : ((Fin m → ℝ) × (Fin n → ℝ)) × (Fin m → ℝ) × (Fin n → ℝ)), e p = helperForCorollary_37_5_1_packGraphCoordinates p

Helper for Corollary 37.5.1: the corrected packing map is an ambient homeomorphism before restricting to either graph.

theorem helperForCorollary_37_5_1_packedDotIncrement_eq_splitAffineTerm {m n : ℕ} (u : Fin m → ℝ) (v : Fin n → ℝ) (uStar : Fin m → ℝ) (vStar : Fin n → ℝ) (u' : Fin m → ℝ) (x' : Fin n → ℝ) : ↑(((dotProductEquiv ℝ (Fin (m + n))) (Fin.append (-uStar) v)) (Fin.append u' x' - Fin.append u vStar)) = ↑(x' ⬝ᵥ v) - ↑(vStar ⬝ᵥ v) - (↑(u' ⬝ᵥ uStar) - ↑(u ⬝ᵥ uStar))

Helper for Corollary 37.5.1: the packed dual pairing with ((u', x') - (u, vStar), (-uStar, v)) is exactly the split affine term ⟪x', v⟫ - ⟪vStar, v⟫ - (⟪u', uStar⟫ - ⟪u, uStar⟫).