theorem ERealFunction.subdifferential_domain_subset_effectiveDomain {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (f : H → ↑(Set.Ioi ⊥)) (hdom : (effectiveDomain f).Nonempty) : (subdifferential f).dom ⊆ effectiveDomain f

Proposition 16.4 (1): if f has a nonempty effective domain, then every point at which the subdifferential is nonempty lies in the effective domain. For ]-∞,+∞]-valued functions, this is the remaining properness content after excluding -∞ by the codomain.

theorem ERealFunction.SubdifferentiableAt.mem_effectiveDomain {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] {f : H → ↑(Set.Ioi ⊥)} (hdom : (effectiveDomain f).Nonempty) {x : H} (hx : SubdifferentiableAt f x) : x ∈ effectiveDomain f

Pointwise form of Proposition 16.4 (1): subdifferentiability forces effective-domain membership.

theorem ERealFunction.subdifferential_eq_iInter_affine_halfspaces {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (f : H → ↑(Set.Ioi ⊥)) (x : H) (hx : x ∈ effectiveDomain f) : subdifferential f x = ⋂ y ∈ effectiveDomain f, {u : H | inner ℝ (y - x) u ≤ (↑(f y)).toReal - (↑(f x)).toReal}

Proposition 16.4 (2): at a point of the effective domain, the subdifferential is the intersection of the affine half-spaces cut out by the subgradient inequalities over the effective domain.

theorem ERealFunction.isClosed_subdifferential {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (f : H → ↑(Set.Ioi ⊥)) (x : H) : IsClosed (subdifferential f x)

Proposition 16.4 (3): the subdifferential is closed at every point.

theorem ERealFunction.convex_subdifferential {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (f : H → ↑(Set.Ioi ⊥)) (x : H) : Convex ℝ (subdifferential f x)

Proposition 16.4 (4): the subdifferential is convex at every point.

theorem ERealFunction.SubdifferentiableAt.lowerSemicontinuousAt {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] {f : H → ↑(Set.Ioi ⊥)} {x : H} (hxsub : SubdifferentiableAt f x) : LowerSemicontinuousAt (Function.asEReal f) x

Proposition 16.4 (5): if the subdifferential of f at x is nonempty, then f is lower semicontinuous at x.

theorem ERealFunction.SubdifferentiableAt.weaklyLowerSemicontinuousAt {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] {f : H → ↑(Set.Ioi ⊥)} {x : H} (hxsub : SubdifferentiableAt f x) : WeaklyLowerSemicontinuousAt (Function.asEReal f) x

Proposition 16.4 (6): if the subdifferential of f at x is nonempty, then f is weakly lower semicontinuous at x.