theorem strongDualSubdifferential_nonempty_at_interior_point {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (f : E → EReal) (hconvex : is_convex_function f) {x : E} (hx : x ∈ interior (effective_domain f)) : ∂ₛf(x).Nonempty

Helper for Theorem 3.5: interior points of effective_domain f have a nonempty strong-dual subdifferential.

theorem strongDualSubdifferential_subset_closedBall_of_lipschitzOnWith_closure {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : E → EReal) (h_ne_bot : ∀ y ∈ effective_domain f, f y ≠ ⊥) {U : Set E} (hU_open : IsOpen U) (hU_closure_subset : closure U ⊆ interior (effective_domain f)) {L : NNReal} (hLip : LipschitzOnWith L (fun (y : E) => (f y).toReal) (closure U)) ⦃x : E⦄ : x ∈ U → ∂ₛf(x) ⊆ Metric.closedBall 0 ↑L

Helper for Theorem 3.5: a Lipschitz bound on closure U bounds every subgradient over the open set U by the same dual closed ball.

theorem subdifferential_biUnion_nonempty_of_nonempty_subset_interior {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (f : E → EReal) (X : Set E) (hconvex : is_convex_function f) (hX_nonempty : X.Nonempty) (hX_subset : X ⊆ interior (effective_domain f)) : (⋃ x ∈ X, ∂ₛf(x)).Nonempty

Nonemptiness part of Theorem 3.5: if f is a convex extended-real-valued function and the source text assumes that X is a nonempty compact subset of interior (dom(f)), then the union ⋃ x ∈ X, ∂ₛ f(x) is nonempty. Compactness and any separate no-⊥ hypothesis are not used for this existence conclusion: Chapter 3 already provides subdifferential nonemptiness at interior points from convexity alone, so the public API keeps only the source-facing assumptions that change the statement.

theorem subdifferential_biUnion_isBounded_of_isCompact_subset_interior {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (f : E → EReal) (X : Set E) (h_ne_bot : ∀ y ∈ effective_domain f, f y ≠ ⊥) (hconvex : is_convex_function f) (hX_compact : IsCompact X) (hX_subset : X ⊆ interior (effective_domain f)) : Bornology.IsBounded (⋃ x ∈ X, ∂ₛf(x))

Theorem 3.5 (2): if f is a convex extended-real-valued function that never takes the value ⊥ on effective_domain f, and X is a compact subset of interior (dom(f)), then the union ⋃ x ∈ X, ∂ₛ f(x) is bounded in the dual norm. The boundedness conclusion does not use X.Nonempty, so the public API omits that redundant source-side binder. The source text packages this statement under the stronger properness and nonempty-compactness hypotheses; the boundedness argument used here depends only on the displayed Chapter 3 Lipschitz/boundedness assumptions.