theorem exists_closedProperConvex_subdifferential_superset_iff_isCyclicallyMonotone {n : ℕ} (ρ : (Fin n → ℝ) → Set (Fin n → ℝ)) : (∃ (f : (Fin n → ℝ) → EReal), ClosedConvexFunction f ∧ ProperConvexFunctionOn Set.univ f ∧ ∀ (x : Fin n → ℝ), ρ x ⊆ ⇑(dotProductEquiv ℝ (Fin n)) ⁻¹' subdifferentialAt f x) ↔ IsCyclicallyMonotone ρ

Theorem 5.24.11: a multivalued mapping ρ : ℝ^n ⇉ ℝ^n is cyclically monotone if and only if there exists a closed proper convex function f on ℝ^n whose Euclideanized subdifferential contains ρ pointwise; in Lean this containment is ρ x ⊆ (dotProductEquiv ℝ (Fin n)) ⁻¹' subdifferentialAt f x for every x.

theorem helperForTheorem_5_24_12_additive_constant_exists_at_common_graph_point {n : ℕ} (f g : (Fin n → ℝ) → EReal) (hproperF : ProperConvexFunctionOn Set.univ f) (hproperG : ProperConvexFunctionOn Set.univ g) {x xStar : Fin n → ℝ} (hxStarF : xStar ∈ ⇑(dotProductEquiv ℝ (Fin n)) ⁻¹' subdifferentialAt f x) (hxStarG : xStar ∈ ⇑(dotProductEquiv ℝ (Fin n)) ⁻¹' subdifferentialAt g x) : ∃ (α : ℝ), g x = f x + ↑α

Helper for Theorem 5.24.12: a common Euclideanized subgradient point already determines the additive gap between two proper convex functions.

theorem helperForTheorem_5_24_12_conjugateFiberSubset_of_primalFiberSubset {n : ℕ} (f g : (Fin n → ℝ) → EReal) (hclosedF : ClosedConvexFunction f) (hproperF : ProperConvexFunctionOn Set.univ f) (hclosedG : ClosedConvexFunction g) (hproperG : ProperConvexFunctionOn Set.univ g) (hsubset : ∀ (x : Fin n → ℝ), ⇑(dotProductEquiv ℝ (Fin n)) ⁻¹' subdifferentialAt f x ⊆ ⇑(dotProductEquiv ℝ (Fin n)) ⁻¹' subdifferentialAt g x) (xStar : Fin n → ℝ) : ⇑(dotProductEquiv ℝ (Fin n)) ⁻¹' subdifferentialAt (fenchelConjugate n f) xStar ⊆ ⇑(dotProductEquiv ℝ (Fin n)) ⁻¹' subdifferentialAt (fenchelConjugate n g) xStar

Helper for Theorem 5.24.12: primal Euclideanized fiber inclusion transports to the Fenchel conjugates by swapping the two Euclidean subgradient coordinates.

theorem helperForTheorem_5_24_12_subdifferential_eq_of_eq_add_constant {n : ℕ} {f g : (Fin n → ℝ) → EReal} {α : ℝ} (hEq : ∀ (x : Fin n → ℝ), g x = f x + ↑α) (x : Fin n → ℝ) : ⇑(dotProductEquiv ℝ (Fin n)) ⁻¹' subdifferentialAt f x = ⇑(dotProductEquiv ℝ (Fin n)) ⁻¹' subdifferentialAt g x

Helper for Theorem 5.24.12: adding a finite real constant does not change Euclideanized subdifferential fibers.

theorem helperForTheorem_5_24_12_secantQuotientFiberSubset_of_primalFiberSubset {n : ℕ} (f g : (Fin n → ℝ) → EReal) (hproperF : ProperConvexFunctionOn Set.univ f) (hproperG : ProperConvexFunctionOn Set.univ g) (hsubset : ∀ (x : Fin n → ℝ), ⇑(dotProductEquiv ℝ (Fin n)) ⁻¹' subdifferentialAt f x ⊆ ⇑(dotProductEquiv ℝ (Fin n)) ⁻¹' subdifferentialAt g x) {x u : Fin n → ℝ} {t : ℝ} (hxFiniteF : f x ≠ ⊤ ∧ f x ≠ ⊥) (hxFiniteG : g x ≠ ⊤ ∧ g x ≠ ⊥) (huFiniteF : f (x + t • u) ≠ ⊤ ∧ f (x + t • u) ≠ ⊥) (huFiniteG : g (x + t • u) ≠ ⊤ ∧ g (x + t • u) ≠ ⊥) (ht : 0 < t) : ⇑(dotProductEquiv ℝ (Fin n)) ⁻¹' subdifferentialAt (fun (v : Fin n → ℝ) => directionalDifferenceQuotientAt f x v t) u ⊆ ⇑(dotProductEquiv ℝ (Fin n)) ⁻¹' subdifferentialAt (fun (v : Fin n → ℝ) => directionalDifferenceQuotientAt g x v t) u

Helper for Theorem 5.24.12: primal Euclideanized fiber inclusion persists after passing to a fixed-step secant quotient based at a finite anchor point.

theorem helperForTheorem_5_24_12_intervalSetEq_implies_derivativeEndpointsEq {a1 b1 a2 b2 : EReal} (ha1_top : a1 ≠ ⊤) (ha1_bot : a1 ≠ ⊥) (hb1_top : b1 ≠ ⊤) (hb1_bot : b1 ≠ ⊥) (ha2_top : a2 ≠ ⊤) (ha2_bot : a2 ≠ ⊥) (hb2_top : b2 ≠ ⊤) (hb2_bot : b2 ≠ ⊥) (hNonempty : {x : ℝ | a1 ≤ ↑x ∧ ↑x ≤ b1}.Nonempty) (hEq : {x : ℝ | a1 ≤ ↑x ∧ ↑x ≤ b1} = {x : ℝ | a2 ≤ ↑x ∧ ↑x ≤ b2}) : a1 = a2 ∧ b1 = b2

Helper for Theorem 5.24.12: once two nonempty scalar interval fibers are written with finite endpoints, equality of the interval sets forces equality of the two endpoint pairs.

theorem helperForTheorem_5_24_12_intervalSubset_implies_derivativeBandBounds {a1 b1 a2 b2 : EReal} (ha1_top : a1 ≠ ⊤) (ha1_bot : a1 ≠ ⊥) (hb1_top : b1 ≠ ⊤) (hb1_bot : b1 ≠ ⊥) (_ha2_top : a2 ≠ ⊤) (_ha2_bot : a2 ≠ ⊥) (_hb2_top : b2 ≠ ⊤) (_hb2_bot : b2 ≠ ⊥) (hNonempty : {x : ℝ | a1 ≤ ↑x ∧ ↑x ≤ b1}.Nonempty) (hSubset : {x : ℝ | a1 ≤ ↑x ∧ ↑x ≤ b1} ⊆ {x : ℝ | a2 ≤ ↑x ∧ ↑x ≤ b2}) : a2 ≤ a1 ∧ b1 ≤ b2

Helper for Theorem 5.24.12: inclusion of two finite nonempty scalar interval fibers already forces the corresponding derivative-band bounds in the only direction available from the inclusion.

theorem helperForTheorem_5_24_12_scalarRestrictionDerivativeBandBounds_of_primalFiberSubset (F G : (Fin 1 → ℝ) → EReal) (hclosedF : ClosedConvexFunction F) (hproperF : ProperConvexFunctionOn Set.univ F) (hclosedG : ClosedConvexFunction G) (hproperG : ProperConvexFunctionOn Set.univ G) {t : ℝ} (htF : t ∈ interior (scalarEffectiveDomain F)) (htG : t ∈ interior (scalarEffectiveDomain G)) (hFiberSubset : {xStar : ℝ | (dotProductEquiv ℝ (Fin 1)) (scalarPoint xStar) ∈ subdifferentialAt F (scalarPoint t)} ⊆ {xStar : ℝ | (dotProductEquiv ℝ (Fin 1)) (scalarPoint xStar) ∈ subdifferentialAt G (scalarPoint t)}) : leftDerivativeExtension G t ≤ leftDerivativeExtension F t ∧ rightDerivativeExtension F t ≤ rightDerivativeExtension G t

Helper for Theorem 5.24.12: once scalar fiber inclusion is rewritten through Theorem 5.24.2, the only remaining information is the corresponding one-sided derivative-band bounds.

theorem helperForTheorem_5_24_12_derivativeBandBounds_on_Ioo_imply_scalarDerivativeExtensionsEq (F G : (Fin 1 → ℝ) → EReal) (hclosedF : ClosedConvexFunction F) (hproperF : ProperConvexFunctionOn Set.univ F) (hclosedG : ClosedConvexFunction G) (hproperG : ProperConvexFunctionOn Set.univ G) {a b : ℝ} (_hab : a < b) (hband : ∀ t ∈ Set.Ioo a b, leftDerivativeExtension G t ≤ leftDerivativeExtension F t ∧ rightDerivativeExtension F t ≤ rightDerivativeExtension G t) (x : ℝ) : x ∈ Set.Ioo a b → leftDerivativeExtension G x = leftDerivativeExtension F x ∧ rightDerivativeExtension F x = rightDerivativeExtension G x

Helper for Theorem 5.24.12: once the scalar derivative-band inequalities hold on every point of an open interval, the one-sided continuity of the derivative extensions upgrades them to pointwise equality of the left and right derivative extensions on that interval.

theorem helperForTheorem_5_24_12_scalarRestrictionDerivativeBands_eq_of_commonScalarFibers (F G : (Fin 1 → ℝ) → EReal) (hclosedF : ClosedConvexFunction F) (hproperF : ProperConvexFunctionOn Set.univ F) (hclosedG : ClosedConvexFunction G) (hproperG : ProperConvexFunctionOn Set.univ G) {t : ℝ} (htF : t ∈ interior (scalarEffectiveDomain F)) (htG : t ∈ interior (scalarEffectiveDomain G)) (hFiberEq : {xStar : ℝ | (dotProductEquiv ℝ (Fin 1)) (scalarPoint xStar) ∈ subdifferentialAt F (scalarPoint t)} = {xStar : ℝ | (dotProductEquiv ℝ (Fin 1)) (scalarPoint xStar) ∈ subdifferentialAt G (scalarPoint t)}) : leftDerivativeExtension F t = leftDerivativeExtension G t ∧ rightDerivativeExtension F t = rightDerivativeExtension G t

Helper for Theorem 5.24.12: if two one-dimensional scalar restrictions have the same scalar subdifferential fiber at an interior point, then their left and right derivative bands agree at that point.

theorem helperForTheorem_5_24_12_translatedDifference_subdifferential_eq_shifted {n : ℕ} (f : (Fin n → ℝ) → EReal) (x z : Fin n → ℝ) (hxFinite : f x ≠ ⊤ ∧ f x ≠ ⊥) : ⇑(dotProductEquiv ℝ (Fin n)) ⁻¹' subdifferentialAt (translatedDifferenceFunctionAt f x) z = ⇑(dotProductEquiv ℝ (Fin n)) ⁻¹' subdifferentialAt f (x + z)

Helper for Theorem 5.24.12: translating by a fixed primal base point rewrites the Euclideanized subdifferential fiber of the translated-difference function as the original fiber at the shifted point.

theorem helperForTheorem_5_24_12_translatedDifferenceFiberSubset_of_primalFiberSubset {n : ℕ} (f g : (Fin n → ℝ) → EReal) (x0 : Fin n → ℝ) (hx0FiniteF : f x0 ≠ ⊤ ∧ f x0 ≠ ⊥) (hx0FiniteG : g x0 ≠ ⊤ ∧ g x0 ≠ ⊥) (hsubset : ∀ (x : Fin n → ℝ), ⇑(dotProductEquiv ℝ (Fin n)) ⁻¹' subdifferentialAt f x ⊆ ⇑(dotProductEquiv ℝ (Fin n)) ⁻¹' subdifferentialAt g x) (z : Fin n → ℝ) : ⇑(dotProductEquiv ℝ (Fin n)) ⁻¹' subdifferentialAt (translatedDifferenceFunctionAt f x0) z ⊆ ⇑(dotProductEquiv ℝ (Fin n)) ⁻¹' subdifferentialAt (translatedDifferenceFunctionAt g x0) z

Helper for Theorem 5.24.12: pointwise Euclideanized primal-fiber inclusion is preserved after translating both functions by the same base point and subtracting the corresponding base value.

theorem helperForTheorem_5_24_12_translatedDifference_zero {n : ℕ} (f : (Fin n → ℝ) → EReal) (x : Fin n → ℝ) (hx : f x ≠ ⊤ ∧ f x ≠ ⊥) : translatedDifferenceFunctionAt f x 0 = 0

Helper for Theorem 5.24.12: the translated-difference function vanishes at the origin when the base value is finite.

theorem helperForTheorem_5_24_12_translatedDifference_properConvex {n : ℕ} (f : (Fin n → ℝ) → EReal) (hproper : ProperConvexFunctionOn Set.univ f) (x : Fin n → ℝ) (hx : f x ≠ ⊤ ∧ f x ≠ ⊥) : ProperConvexFunctionOn Set.univ (translatedDifferenceFunctionAt f x)

Helper for Theorem 5.24.12: translated differences inherit proper convexity from the original proper convex function.

theorem helperForTheorem_5_24_12_translatedDifference_closed {n : ℕ} (f : (Fin n → ℝ) → EReal) (hclosed : ClosedConvexFunction f) (hproper : ProperConvexFunctionOn Set.univ f) (x : Fin n → ℝ) (hx : f x ≠ ⊤ ∧ f x ≠ ⊥) : ClosedConvexFunction (translatedDifferenceFunctionAt f x)

Helper for Theorem 5.24.12: translated differences of closed proper convex functions remain closed.