Real parts of continuous linear functionals on balls

For a continuous linear functional f on a seminormed space over RCLike scalars and a radius 0 ≤ r, every upper bound of re ∘ f on closedBall x r is at least re (f x) + r * ‖f‖. Hahn–Banach separation arguments use this to turn a separating real-part bound on a ball into a bound on the norm of the separating functional. Conversely, for 0 ≤ r < ‖f‖ the real part of f exceeds r * ‖x‖ at some point x.

Main results

• StrongDual.re_apply_add_mul_norm_le: a bound for the real part of a functional on a closed ball of nonnegative radius bounds its value at the centre plus the radius times its norm.
• StrongDual.exists_mul_norm_lt_re_apply: for 0 ≤ r < ‖f‖, the real part of f exceeds r * ‖x‖ at some point x.

theorem StrongDual.re_apply_add_mul_norm_le {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {f : StrongDual 𝕜 E} {x : E} {r u : ℝ} (hr : 0 ≤ r) (h : ∀ y ∈ Metric.closedBall x r, RCLike.re (f y) ≤ u) : RCLike.re (f x) + r * ‖f‖ ≤ u

If the real part of a continuous linear functional f is at most u on the closed ball of radius r ≥ 0 about x, then re (f x) + r * ‖f‖ ≤ u.

theorem StrongDual.exists_mul_norm_lt_re_apply {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] (f : StrongDual 𝕜 E) {r : ℝ} (hr₀ : 0 ≤ r) (hr : r < ‖f‖) : ∃ (x : E), r * ‖x‖ < RCLike.re (f x)

If 0 ≤ r < ‖f‖, then the real part of f exceeds r * ‖x‖ at some point x.