The Bishop–Phelps theorem

Let C be a complete convex subset of a real or complex normed space E. A support functional of C is a nonzero continuous linear functional g whose real part attains its supremum on C; a point of C at which this happens is a support point. The Bishop–Phelps theorem says that there are many of both:

• if C is nonempty, every nonzero functional whose real part is bounded above on C is a norm limit of support functionals of C (Convex.mem_closure_setOf_ne_zero_isMaxOn_re_of_bddAbove); in particular, if C is moreover bounded and E is nonzero, the support functionals of C are norm dense in the dual (Convex.dense_setOf_ne_zero_isMaxOn_re);
• the support points of C are dense in its boundary (Convex.frontier_subset_closure_setOf_isMaxOn_re); conversely every support point lies on the boundary (StrongDual.mem_frontier_of_isMaxOn_re);
• taking for C the closed unit ball, the norm-attaining functionals are norm dense in the dual (TauCeti.dense_setOf_exists_norm_apply_eq_norm).

The support theorems assume only that C is complete; the norm-attainment theorem assumes that E is complete. Convexity is real convexity, also over ℂ. Cone convexity also holds on seminormed spaces, without a normed scalar action over 𝕜.

The proof follows Phelps. Ekeland's variational principle (LowerSemicontinuous.exists_add_mul_dist_le_and_lt_add_mul_dist), applied to minus the real part of a functional f on C, produces a point x ∈ C such that C meets the cone x + {w | k * ‖f‖ * ‖w‖ ≤ re (f w)} only at x. Separating C from the interior of this cone gives a support functional h at x whose real part is positive on the open cone (Convex.exists_isMaxOn_re_of_bddAbove), and the Bishop–Phelps lemma (StrongDual.exists_pos_norm_sub_ofReal_smul_le) shows that a positive multiple of h lies within k * ‖f‖ of f.

Main results

• StrongDual.exists_pos_norm_sub_ofReal_smul_le: the Bishop–Phelps lemma.
• StrongDual.convex_setOf_mul_norm_sub_lt_re: the open Bishop–Phelps cones are convex.
• Convex.exists_isMaxOn_re_of_bddAbove: support functionals at points reached through a cone.
• Convex.mem_closure_setOf_ne_zero_isMaxOn_re_of_bddAbove: support functionals of a nonempty complete convex set are dense among the nonzero functionals bounded above on it.
• Convex.dense_setOf_ne_zero_isMaxOn_re: support functionals of a bounded complete convex set are dense.
• Convex.frontier_subset_closure_setOf_isMaxOn_re: support points are dense in the boundary.
• TauCeti.dense_setOf_exists_norm_apply_eq_norm: norm-attaining functionals are dense.

References

• E. Bishop and R. R. Phelps, A proof that every Banach space is subreflexive, Bull. Amer. Math. Soc. 67 (1961), 97–98.
• R. R. Phelps, Convex Functions, Monotone Operators and Differentiability, 2nd ed., Lecture Notes in Mathematics 1364, Springer, 1993, Chapter 3.
• R. E. Megginson, An Introduction to Banach Space Theory, §2.11 and Theorem 2.11.14.

theorem StrongDual.convex_setOf_mul_norm_sub_lt_re {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [Module 𝕜 E] [NormedSpace ℝ E] [IsScalarTower ℝ 𝕜 E] (f : StrongDual 𝕜 E) {r : ℝ} (hr : 0 ≤ r) (x : E) : Convex ℝ {y : E | r * ‖y - x‖ < RCLike.re (f (y - x))}

For 0 ≤ r, the open cone {y | r * ‖y - x‖ < re (f (y - x))} with vertex x is convex.

theorem StrongDual.exists_pos_norm_sub_ofReal_smul_le {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (f h : StrongDual 𝕜 E) {k : ℝ} (hk₀ : 0 ≤ k) (hk₁ : k < 1) (hf : f ≠ 0) (hpos : ∀ (x : E), k * ‖f‖ * ‖x‖ < RCLike.re (f x) → 0 < RCLike.re (h x)) : ∃ (c : ℝ), 0 < c ∧ ‖f - ↑c • h‖ ≤ k * ‖f‖

The Bishop–Phelps lemma. Let 0 ≤ k < 1 and f ≠ 0. If the real part of h is positive on the open cone {x | k * ‖f‖ * ‖x‖ < re (f x)}, then some positive real multiple of h lies within k * ‖f‖ of f.

theorem StrongDual.mem_frontier_of_isMaxOn_re {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (g : StrongDual 𝕜 E) (hg : g ≠ 0) {C : Set E} {x : E} (hx : x ∈ C) (hmax : IsMaxOn (fun (y : E) => RCLike.re (g y)) C x) : x ∈ frontier C

A point at which the real part of a nonzero functional attains its maximum on C lies on the boundary of C.

theorem Convex.exists_isMaxOn_re_of_bddAbove {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace ℝ E] [IsScalarTower ℝ 𝕜 E] {C : Set E} (hconv : Convex ℝ C) (hC : IsComplete C) {f : StrongDual 𝕜 E} (hf : f ≠ 0) (hbdd : BddAbove ((fun (y : E) => RCLike.re (f y)) '' C)) {k : ℝ} (hk₀ : 0 < k) (hk₁ : k < 1) {z : E} (hz : z ∈ C) : ∃ x ∈ C, k * ‖f‖ * ‖x - z‖ ≤ RCLike.re (f (x - z)) ∧ ∃ (h : StrongDual 𝕜 E), h ≠ 0 ∧ IsMaxOn (fun (y : E) => RCLike.re (h y)) C x ∧ ∀ (w : E), k * ‖f‖ * ‖w‖ < RCLike.re (f w) → 0 < RCLike.re (h w)

Bishop–Phelps support lemma. Let C be a complete convex subset of a normed space, let f be a nonzero functional whose real part is bounded above on C, and let 0 < k < 1. From every z ∈ C one reaches a point x ∈ C with k * ‖f‖ * ‖x - z‖ ≤ re (f (x - z)) at which C has a support functional h, nonzero and with real part positive on the open cone {w | k * ‖f‖ * ‖w‖ < re (f w)}.

theorem Convex.mem_closure_setOf_ne_zero_isMaxOn_re_of_bddAbove {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace ℝ E] [IsScalarTower ℝ 𝕜 E] {C : Set E} (hconv : Convex ℝ C) (hC : IsComplete C) (hne : C.Nonempty) {f : StrongDual 𝕜 E} (hf : f ≠ 0) (hbdd : BddAbove ((fun (y : E) => RCLike.re (f y)) '' C)) : f ∈ closure {g : StrongDual 𝕜 E | g ≠ 0 ∧ ∃ x ∈ C, IsMaxOn (fun (y : E) => RCLike.re (g y)) C x}

The Bishop–Phelps theorem for support functionals, in Phelps' general form. Let C be a nonempty complete convex subset of a normed space. Every nonzero functional whose real part is bounded above on C is a norm limit of support functionals of C, namely of nonzero functionals whose real part attains its supremum on C. No boundedness of C is assumed: the support functionals of C are norm dense among the nonzero functionals whose real part is bounded above on C.

theorem Convex.dense_setOf_ne_zero_isMaxOn_re {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace ℝ E] [IsScalarTower ℝ 𝕜 E] {C : Set E} [Nontrivial E] (hconv : Convex ℝ C) (hC : IsComplete C) (hb : Bornology.IsBounded C) (hne : C.Nonempty) : Dense {g : StrongDual 𝕜 E | g ≠ 0 ∧ ∃ x ∈ C, IsMaxOn (fun (y : E) => RCLike.re (g y)) C x}

The Bishop–Phelps theorem for support functionals. The support functionals of a nonempty bounded complete convex subset C of a nonzero normed space, namely the nonzero functionals whose real part attains its supremum on C, are norm dense in the dual. This is the case of Convex.mem_closure_setOf_ne_zero_isMaxOn_re_of_bddAbove in which every functional is bounded on C.

theorem Convex.frontier_subset_closure_setOf_isMaxOn_re {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace ℝ E] [IsScalarTower ℝ 𝕜 E] {C : Set E} (hconv : Convex ℝ C) (hC : IsComplete C) : frontier C ⊆ closure {x : E | x ∈ C ∧ ∃ (g : StrongDual 𝕜 E), g ≠ 0 ∧ IsMaxOn (fun (y : E) => RCLike.re (g y)) C x}

The Bishop–Phelps theorem for support points. The support points of a complete convex subset C of a normed space, namely the points of C at which the real part of some nonzero functional attains its supremum on C, are dense in the boundary of C. They all lie on the boundary by StrongDual.mem_frontier_of_isMaxOn_re.

theorem TauCeti.dense_setOf_exists_norm_apply_eq_norm {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] : Dense {g : StrongDual 𝕜 E | ∃ (x : E), ‖x‖ ≤ 1 ∧ ‖g x‖ = ‖g‖}

The Bishop–Phelps theorem. The continuous linear functionals on a Banach space which attain their norm on the closed unit ball are norm dense in the dual.