def ERealFunction.ContinuousAtOnEffectiveDomain {H : Type u} [NormedAddCommGroup H] (f : H → ↑(Set.Ioi ⊥)) (x : H) : Prop

A point is a continuity point of f when the finite-valued restriction of f to its effective domain is continuous there.

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

A continuity point on the effective domain belongs to the effective domain.

theorem ERealFunction.ContinuousAtOnEffectiveDomain.continuousWithinAt {H : Type u} [NormedAddCommGroup H] {f : H → ↑(Set.Ioi ⊥)} {x : H} (hx : ContinuousAtOnEffectiveDomain f x) : ContinuousWithinAt (fun (y : H) => (↑(f y)).toReal) (effectiveDomain f) x

A continuity point on the effective domain is continuous for the finite-valued restriction of f to its effective domain.

theorem ERealFunction.subdifferential_eq_empty_or_unbounded_of_mem_frontier_effectiveDomain {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (f : H → ↑(Set.Ioi ⊥)) (hconv : ConvexOn f (effectiveDomain f)) {x : H} (hx : x ∈ effectiveDomain f) (hinter : (interior (effectiveDomain f)).Nonempty) (hfrontier : x ∈ frontier (effectiveDomain f)) : subdifferential f x = ∅ ∨ ¬Bornology.IsBounded (subdifferential f x)

Proposition 16.17 (1): clause (i). If the effective domain has nonempty interior and x lies on its boundary, then the subdifferential at x is either empty or unbounded.

theorem ERealFunction.subdifferential_nonempty_and_weaklyCompact_of_continuousAtOnEffectiveDomain {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (f : H → ↑(Set.Ioi ⊥)) (hconv : ConvexOn f (effectiveDomain f)) {x : H} (hxcont : ContinuousAtOnEffectiveDomain f x) : (subdifferential f x).Nonempty ∧ IsCompact (⇑(toWeakSpace ℝ H) '' subdifferential f x)

Proposition 16.17 (2): clause (ii). At a continuity point of the finite-valued restriction of f to its effective domain, the subdifferential is nonempty and weakly compact.

theorem ERealFunction.subdifferential_ball_union_bounded_of_continuousAtOnEffectiveDomain {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (f : H → ↑(Set.Ioi ⊥)) (hconv : ConvexOn f (effectiveDomain f)) {x : H} (hxcont : ContinuousAtOnEffectiveDomain f x) : ∃ (ρ : ℝ), 0 < ρ ∧ Bornology.IsBounded (⋃ y ∈ Metric.ball x ρ, subdifferential f y)

Proposition 16.17 (3): clause (iii). At a continuity point of the finite-valued restriction of f to its effective domain, there is a positive radius for which the union of the nearby subdifferentials is bounded.

theorem ERealFunction.interior_effectiveDomain_subset_subdifferentiabilityDomain_of_exists_continuityPoint {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (f : H → ↑(Set.Ioi ⊥)) (hconv : ConvexOn f (effectiveDomain f)) (hcont : ∃ (x : H), ContinuousAtOnEffectiveDomain f x) : interior (effectiveDomain f) ⊆ {x : H | SubdifferentiableAt f x}

Proposition 16.17 (4): clause (iv). If the effective-domain continuity set is nonempty, then every interior point of the effective domain is a subdifferentiability point.