noncomputable def rightHalfLineSquareRootGap (ξ₁ : ℝ) : EReal

The one-variable function g(ξ₁) = 1 - √ξ₁ on the nonnegative half-line and +∞ on the negative half-line.

noncomputable def nonconvexSubdifferentiabilityExampleFunction (ξ : Fin 2 → ℝ) : EReal

The ℝ² example f(ξ₁, ξ₂) = max {g(ξ₁), |ξ₂|} used to show that the set of subdifferentiability points of a proper convex function need not be convex.

def closedRightHalfPlane : Set (Fin 2 → ℝ)

The closed right half-plane in ℝ².

def openVerticalUnitSegment : Set (Fin 2 → ℝ)

The relative interior of the vertical line segment joining (0, 1) and (0, -1).

theorem helperForExample_23_4_2_rightHalfLineSquareRootGap_branch_convex : ConvexOn ℝ (Set.Ici 0) fun (t : ℝ) => 1 - √t

The g-branch is convex on the nonnegative half-line.

theorem helperForExample_23_4_2_rightHalfLineSquareRootGap_convex : ConvexFunctionOn Set.univ fun (ξ : Fin 2 → ℝ) => rightHalfLineSquareRootGap (ξ 0)

The epigraph of the right-half-line square-root gap function is convex.

theorem helperForExample_23_4_2_absBranch_convex : ConvexFunctionOn Set.univ fun (ξ : Fin 2 → ℝ) => ↑|ξ 1|

The epigraph of the absolute-value branch is convex.

theorem helperForExample_23_4_2_properConvex : ProperConvexFunctionOn Set.univ nonconvexSubdifferentiabilityExampleFunction

The full max example is a proper convex function.

theorem helperForExample_23_4_2_effectiveDomain : effectiveDomain Set.univ nonconvexSubdifferentiabilityExampleFunction = closedRightHalfPlane

The effective domain of the example is exactly the closed right half-plane.

theorem helperForExample_23_4_2_mem_interior_closedRightHalfPlane {ξ : Fin 2 → ℝ} (hξ : 0 < ξ 0) : ξ ∈ interior closedRightHalfPlane

Points with positive first coordinate lie in the interior of the closed right half-plane.

theorem helperForExample_23_4_2_subdifferential_empty_on_openVerticalUnitSegment {ξ : Fin 2 → ℝ} (hξ0 : ξ 0 = 0) (hξ1 : |ξ 1| < 1) : subdifferentialAt nonconvexSubdifferentiabilityExampleFunction ξ = ∅

Boundary points (0,t) with |t| < 1 have empty subdifferential.

theorem helperForExample_23_4_2_subgradient_of_boundary_ge_one {ξ : Fin 2 → ℝ} (hξ0 : ξ 0 = 0) (hξ1 : 1 ≤ ξ 1) : (dotProductEquiv ℝ (Fin 2)) (Pi.single 1 1) ∈ subdifferentialAt nonconvexSubdifferentiabilityExampleFunction ξ

Boundary points (0,t) with t ≥ 1 admit the upward vertical subgradient.

theorem helperForExample_23_4_2_subgradient_of_boundary_le_neg_one {ξ : Fin 2 → ℝ} (hξ0 : ξ 0 = 0) (hξ1 : ξ 1 ≤ -1) : (dotProductEquiv ℝ (Fin 2)) (Pi.single 1 (-1)) ∈ subdifferentialAt nonconvexSubdifferentiabilityExampleFunction ξ

Boundary points (0,t) with t ≤ -1 admit the downward vertical subgradient.

theorem subdifferentiableSet_nonconvex_for_halfPlaneSquareRootMaxExample : ProperConvexFunctionOn Set.univ nonconvexSubdifferentiabilityExampleFunction ∧ effectiveDomain Set.univ nonconvexSubdifferentiabilityExampleFunction = closedRightHalfPlane ∧ {ξ : Fin 2 → ℝ | (subdifferentialAt nonconvexSubdifferentiabilityExampleFunction ξ).Nonempty} = closedRightHalfPlane \ openVerticalUnitSegment ∧ ¬Convex ℝ {ξ : Fin 2 → ℝ | (subdifferentialAt nonconvexSubdifferentiabilityExampleFunction ξ).Nonempty}

Example 23.4.2 (Nonconvexity of Subdifferentiability Set): For the function f(ξ₁, ξ₂) = max {g(ξ₁), |ξ₂|} with g(ξ₁) = 1 - √ξ₁ for ξ₁ ≥ 0 and g(ξ₁) = +∞ for ξ₁ < 0, the effective domain is the closed right half-plane, the set of points where f is subdifferentiable is the closed right half-plane with the open vertical segment {(0, t) | |t| < 1} removed, and hence this subdifferentiability set is not convex.

def RangeMeetsRelativeInteriorEffectiveDomain {n m : ℕ} (A : (Fin n → ℝ) →ₗ[ℝ] Fin m → ℝ) (h : (Fin m → ℝ) → EReal) : Prop

Qualification by an intersection of the range of A with the relative interior of the effective domain of h.

def RangeMeetsEffectiveDomainInOnePoint {n m : ℕ} (A : (Fin n → ℝ) →ₗ[ℝ] Fin m → ℝ) (h : (Fin m → ℝ) → EReal) : Prop

Qualification by a singleton intersection of the range of A with the effective domain of h.

def IsSubdifferentialSumDecompositionAt {m n : ℕ} (f : Fin m → (Fin n → ℝ) → EReal) (x : Fin n → ℝ) (xStar : Module.Dual ℝ (Fin n → ℝ)) : Prop

A dual vector xStar decomposes at x as a sum of subgradients of f₁, …, fₘ when there is a family parts i ∈ ∂ fᵢ(x) whose sum is xStar.

def SubdifferentialSumQualification {m n : ℕ} (f : Fin m → (Fin n → ℝ) → EReal) (Ipoly : Set (Fin m)) : Prop

The qualification condition for the subdifferential sum rule: either all relative interiors of the effective domains meet, or a distinguished polyhedral subfamily has a common point in its effective domains while the remaining summands still meet in relative interior.

theorem helperForTheorem_23_8_sum_dual_apply_sub_eq_ereal_sum {m n : ℕ} (parts : Fin m → Module.Dual ℝ (Fin n → ℝ)) (x z : Fin n → ℝ) : ∑ i : Fin m, ↑((parts i) (z - x)) = ↑((∑ i : Fin m, parts i) (z - x))

Helper for Theorem 23.8: evaluating the sum of a family of dual vectors on z - x is the same as summing the individual evaluations.

theorem helperForTheorem_23_8_subgradient_of_sum_of_decomposition {m n : ℕ} (f : Fin m → (Fin n → ℝ) → EReal) (x : Fin n → ℝ) (xStar : Module.Dual ℝ (Fin n → ℝ)) : IsSubdifferentialSumDecompositionAt f x xStar → xStar ∈ subdifferentialAt (fun (y : Fin n → ℝ) => ∑ i : Fin m, f i y) x

Helper for Theorem 23.8: every explicit decomposition of xStar into summand subgradients produces a subgradient of the pointwise sum.

theorem subgradient_sum_mem_subdifferential_sum {m n : ℕ} (f : Fin m → (Fin n → ℝ) → EReal) (x : Fin n → ℝ) (parts : Fin m → Module.Dual ℝ (Fin n → ℝ)) (hparts : ∀ (i : Fin m), parts i ∈ subdifferentialAt (f i) x) : ∑ i : Fin m, parts i ∈ subdifferentialAt (fun (y : Fin n → ℝ) => ∑ i : Fin m, f i y) x

Theorem 23.8(1), inclusion direction in notation form: every finite sum of summand subgradients belongs to the subdifferential of the summed function.

theorem subdifferential_sum_subset_subdifferential_sum {m n : ℕ} (f : Fin m → (Fin n → ℝ) → EReal) (x : Fin n → ℝ) : ∑ i : Fin m, subdifferentialAt (f i) x ⊆ subdifferentialAt (fun (y : Fin n → ℝ) => ∑ i : Fin m, f i y) x

Theorem 23.8(1), inclusion direction in set form: the Minkowski sum of the summand subdifferentials is contained in the subdifferential of the summed function.

theorem helperForTheorem_23_8_sum_proper_of_qualification {m n : ℕ} (f : Fin m → (Fin n → ℝ) → EReal) (hproper : ∀ (i : Fin m), ProperConvexFunctionOn Set.univ (f i)) (Ipoly : Set (Fin m)) (hqual : SubdifferentialSumQualification f Ipoly) : ProperConvexFunctionOn Set.univ fun (y : Fin n → ℝ) => ∑ i : Fin m, f i y

Helper for Theorem 23.8: the qualification hypothesis supplies a point where the full sum is finite, so the summed function is again proper convex.

theorem helperForTheorem_23_8_fullFenchelYoung_of_sumSubgradient {m n : ℕ} (f : Fin m → (Fin n → ℝ) → EReal) (hsumProper : ProperConvexFunctionOn Set.univ fun (y : Fin n → ℝ) => ∑ i : Fin m, f i y) (x : Fin n → ℝ) (xStar : Module.Dual ℝ (Fin n → ℝ)) (hxStar : xStar ∈ subdifferentialAt (fun (y : Fin n → ℝ) => ∑ i : Fin m, f i y) x) : FenchelYoungEqualityAt (fun (y : Fin n → ℝ) => ∑ i : Fin m, f i y) x ((dotProductEquiv ℝ (Fin n)).symm xStar)

Helper for Theorem 23.8: a subgradient of the full sum yields the corresponding Fenchel-Young equality for that full sum.

theorem helperForTheorem_23_8_dualDecomposition_of_summandFenchelYoung {m n : ℕ} (f : Fin m → (Fin n → ℝ) → EReal) (hproper : ∀ (i : Fin m), ProperConvexFunctionOn Set.univ (f i)) (x xStar : Fin n → ℝ) (parts : Fin m → Fin n → ℝ) (hsum : ∑ i : Fin m, parts i = xStar) (hfy : ∀ (i : Fin m), FenchelYoungEqualityAt (f i) x (parts i)) : IsSubdifferentialSumDecompositionAt f x ((dotProductEquiv ℝ (Fin n)) xStar)

Helper for Theorem 23.8: once each Euclidean summand satisfies Fenchel-Young equality and the summands add up to xStar, the corresponding dual vectors give the required decomposition.

theorem helperForTheorem_23_8_fullConjugate_ne_top_of_fullFenchelYoung {m n : ℕ} (f : Fin m → (Fin n → ℝ) → EReal) (hsumProper : ProperConvexFunctionOn Set.univ fun (y : Fin n → ℝ) => ∑ i : Fin m, f i y) (x xStarE : Fin n → ℝ) (hfullFY : FenchelYoungEqualityAt (fun (y : Fin n → ℝ) => ∑ i : Fin m, f i y) x xStarE) : fenchelConjugate n (fun (y : Fin n → ℝ) => ∑ i : Fin m, f i y) xStarE ≠ ⊤

Helper for Theorem 23.8: a full Fenchel-Young equality for the summed function forces the full conjugate value to be finite.

theorem helperForTheorem_23_8_attainedFenchelSplit_of_allRiQualification {m n : ℕ} (f : Fin m → (Fin n → ℝ) → EReal) (hmPos : 0 < m) (hproper : ∀ (i : Fin m), ProperConvexFunctionOn Set.univ (f i)) (hsumProper : ProperConvexFunctionOn Set.univ fun (y : Fin n → ℝ) => ∑ i : Fin m, f i y) (x xStarE : Fin n → ℝ) (hallri : ∃ (z : Fin n → ℝ), ∀ (i : Fin m), z ∈ euclideanRelativeInterior_fin n (effectiveDomain Set.univ (f i))) (hfullFY : FenchelYoungEqualityAt (fun (y : Fin n → ℝ) => ∑ i : Fin m, f i y) x xStarE) : ∃ (parts : Fin m → Fin n → ℝ), ∑ i : Fin m, parts i = xStarE ∧ fenchelConjugate n (fun (y : Fin n → ℝ) => ∑ i : Fin m, f i y) xStarE = ∑ i : Fin m, fenchelConjugate n (f i) (parts i)

Helper for Theorem 23.8: an all-relative-interior qualification gives an attained Fenchel-conjugate split for the full family.

theorem helperForTheorem_23_8_polyFilter_conjugate_attained_by_subtypeFamily {m n : ℕ} (f : Fin m → (Fin n → ℝ) → EReal) (Ipoly : Set (Fin m)) [DecidablePred fun (i : Fin m) => i ∈ Ipoly] (hIpolyNonempty : Ipoly ≠ ∅) (hpoly : ∀ (i : Fin m), i ∈ Ipoly ↔ IsPolyhedralConvexFunction n (f i)) (hproper : ∀ (i : Fin m), ProperConvexFunctionOn Set.univ (f i)) (hdomPoly : ∃ (z : Fin n → ℝ), ∀ i ∈ Ipoly, z ∈ effectiveDomain Set.univ (f i)) (xHead : Fin n → ℝ) : ∃ (headFamily : { i : Fin m // i ∈ Ipoly } → Fin n → ℝ), ∑ i : { i : Fin m // i ∈ Ipoly }, headFamily i = xHead ∧ fenchelConjugate n (fun (y : Fin n → ℝ) => ∑ i : Fin m with i ∈ Ipoly, f i y) xHead = ∑ i : { i : Fin m // i ∈ Ipoly }, fenchelConjugate n (f ↑i) (headFamily i)

Helper for Theorem 23.8: the polyhedral filtered block over Ipoly attains its conjugate value by a decomposition over the corresponding subtype.

theorem helperForTheorem_23_8_nonpolyFilter_conjugate_attained_by_subtypeFamily {m n : ℕ} (f : Fin m → (Fin n → ℝ) → EReal) (Ipoly : Set (Fin m)) [DecidablePred fun (i : Fin m) => i ∈ Ipoly] (hnonpolyNonempty : {i : Fin m | i ∉ Ipoly} ≠ ∅) (hproper : ∀ (i : Fin m), ProperConvexFunctionOn Set.univ (f i)) (hriNonpoly : ∃ (z : Fin n → ℝ), ∀ i ∉ Ipoly, z ∈ euclideanRelativeInterior_fin n (effectiveDomain Set.univ (f i))) (xTail : Fin n → ℝ) : ∃ (tailFamily : { i : Fin m // i ∉ Ipoly } → Fin n → ℝ), ∑ i : { i : Fin m // i ∉ Ipoly }, tailFamily i = xTail ∧ fenchelConjugate n (fun (y : Fin n → ℝ) => ∑ i : Fin m with i ∉ Ipoly, f i y) xTail = ∑ i : { i : Fin m // i ∉ Ipoly }, fenchelConjugate n (f ↑i) (tailFamily i)

Helper for Theorem 23.8: the nonpolyhedral filtered block over Ipolyᶜ attains its conjugate value by a decomposition over the complement subtype, provided that block is nonempty.

theorem helperForTheorem_23_8_sum_piecewise_membership {m : ℕ} {α : Type u_1} [AddCommMonoid α] (Ipoly : Set (Fin m)) [DecidablePred fun (i : Fin m) => i ∈ Ipoly] (headVal : { i : Fin m // i ∈ Ipoly } → α) (tailVal : { i : Fin m // i ∉ Ipoly } → α) : (∑ i : Fin m, if hi : i ∈ Ipoly then headVal ⟨i, hi⟩ else tailVal ⟨i, hi⟩) = ∑ i : { i : Fin m // i ∈ Ipoly }, headVal i + ∑ i : { i : Fin m // i ∉ Ipoly }, tailVal i

Helper for Theorem 23.8: summing a piecewise family over Ipoly and its complement splits into the corresponding subtype sums.

theorem helperForTheorem_23_8_attainedFenchelSplit_of_mixedQualification_via_filteredBinaryBridge {m n : ℕ} (f : Fin m → (Fin n → ℝ) → EReal) (hmPos : 0 < m) (hproper : ∀ (i : Fin m), ProperConvexFunctionOn Set.univ (f i)) (hsumProper : ProperConvexFunctionOn Set.univ fun (y : Fin n → ℝ) => ∑ i : Fin m, f i y) (Ipoly : Set (Fin m)) [DecidablePred fun (i : Fin m) => i ∈ Ipoly] (hpoly : ∀ (i : Fin m), i ∈ Ipoly ↔ IsPolyhedralConvexFunction n (f i)) (hmixed : ∃ (z : Fin n → ℝ), (∀ i ∈ Ipoly, z ∈ effectiveDomain Set.univ (f i)) ∧ ∀ i ∉ Ipoly, z ∈ euclideanRelativeInterior_fin n (effectiveDomain Set.univ (f i))) (x xStarE : Fin n → ℝ) (hfullFY : FenchelYoungEqualityAt (fun (y : Fin n → ℝ) => ∑ i : Fin m, f i y) x xStarE) : ∃ (parts : Fin m → Fin n → ℝ), ∑ i : Fin m, parts i = xStarE ∧ fenchelConjugate n (fun (y : Fin n → ℝ) => ∑ i : Fin m, f i y) xStarE = ∑ i : Fin m, fenchelConjugate n (f i) (parts i)

Helper for Theorem 23.8: the mixed qualification yields an attained conjugate split after first separating the polyhedral and nonpolyhedral filtered blocks.