theorem subdifferential_domain_nonempty_of_convex_of_effective_domain_nonempty {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (f : E → EReal) (hconv : is_convex_function f) (hdom : (effective_domain f).Nonempty) : (subdifferential_domain f).Nonempty

Owner-level bridge: a convex extended-real-valued function with nonempty effective domain has nonempty subdifferential domain.

theorem subdifferential_domain_nonempty_of_proper_convex {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (f : E → EReal) (hf : IsProperExtendedRealFunction f) (hconv : is_convex_function f) : (subdifferential_domain f).Nonempty

Proposition 3.7.1: any proper convex extended-real-valued function has a point where the subdifferential is nonempty. Equivalently, dom(∂ f) is nonempty.

theorem exists_subdifferentiable_point_in_effective_domain_of_convex_of_effective_domain_nonempty {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (f : E → EReal) (hconv : is_convex_function f) (hdom : (effective_domain f).Nonempty) : ∃ x ∈ effective_domain f, ∂f(x).Nonempty

Owner-level companion: a convex extended-real-valued function with nonempty effective domain has a point of its effective domain where the subdifferential is nonempty.

theorem exists_subdifferentiable_point_in_effective_domain_of_proper_convex {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (f : E → EReal) (hf : IsProperExtendedRealFunction f) (hconv : is_convex_function f) : ∃ x ∈ effective_domain f, ∂f(x).Nonempty

Source-facing corollary: any proper convex extended-real-valued function has a point of its effective domain where the subdifferential is nonempty.