theorem Set.not_mem_supportPoints_iff_normalCone_eq_singleton_zero_of_mem {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] {C : Set H} {x : H} (hx : x ∈ C) : x ∉ C.supportPoints ↔ C.normalCone x = {0}

At a point of C, not being a support point is equivalent to the normal cone being trivial.

theorem Set.not_mem_supportPoints_iff_tangentCone_eq_univ_of_convex {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {C : Set H} {x : H} (hC_convex : Convex ℝ C) (hx : x ∈ C) : x ∉ C.supportPoints ↔ C.tangentCone x = univ

For a convex set, a point of C is not a support point exactly when its tangent cone is all of H.

theorem Set.distanceToSet_zeroGateauxDerivative_tfae_not_mem_supportPoints_tangentCone_eq_univ {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {C : Set H} (hC_closed : IsClosed C) (hC_convex : Convex ℝ C) {x : H} (hx : x ∈ C) : [HasGateauxDerivativeAt (fun (y : H) => Metric.infDist y C) ((InnerProductSpace.toDual ℝ H) 0) x, x ∉ C.supportPoints, C.tangentCone x = univ].TFAE

Proposition 18.22: for a closed convex subset C of a real Hilbert space and x ∈ C, the following are equivalent: the distance function to C has Gâteaux derivative 0 at x, the point x is not a support point of C, and the tangent cone T[C] x is the whole space.

theorem Set.distanceToSet_hasGateauxDerivativeAt_zero_iff_not_mem_supportPoints {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {C : Set H} (hC_closed : IsClosed C) (hC_convex : Convex ℝ C) {x : H} (hx : x ∈ C) : HasGateauxDerivativeAt (fun (y : H) => Metric.infDist y C) ((InnerProductSpace.toDual ℝ H) 0) x ↔ x ∉ C.supportPoints

Proposition 18.22, clauses (i) and (ii): for a closed convex set, the distance function has Gâteaux derivative 0 at x ∈ C exactly when x is not a support point.

theorem Set.distanceToSet_hasGateauxDerivativeAt_zero_iff_tangentCone_eq_univ {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {C : Set H} (hC_closed : IsClosed C) (hC_convex : Convex ℝ C) {x : H} (hx : x ∈ C) : HasGateauxDerivativeAt (fun (y : H) => Metric.infDist y C) ((InnerProductSpace.toDual ℝ H) 0) x ↔ C.tangentCone x = univ

Proposition 18.22, clauses (i) and (iii): for a closed convex set, the distance function has Gâteaux derivative 0 at x ∈ C exactly when T[C] x = univ.