The duality set of a vector in a normed space

For a vector x of a normed space E over 𝕜 = ℝ or ℂ, the (normalized) duality set

J(x) = {x' ∈ E' | x' x = ‖x‖² ∧ ‖x'‖ = ‖x‖}

collects the continuous linear functionals that realize the norm of x in the sharpest possible way. The set-valued map x ↦ J(x) is the duality map of E. On a Hilbert space J(x) is the singleton {⟪x, ·⟫}, and in general it is the tool through which inner-product arguments (⟪A x, x⟫ ≤ 0, say) are transported to Banach spaces; the main consumer is the duality-map characterization of dissipative operators in semigroup theory.

The Hahn--Banach theorem makes every J(x) nonempty (dualitySet_nonempty), and the norm condition can be weakened to an inequality (mem_dualitySet_iff_norm_le), which is how members are usually produced: rescale a norming functional of norm at most one (smul_mem_dualitySet).

References

• K.-J. Engel and R. Nagel, One-Parameter Semigroups for Linear Evolution Equations, Definition II.3.13 (the duality set).
• A. Pazy, Semigroups of Linear Operators and Applications to Partial Differential Equations, Chapter 1, Section 4 (the duality set F(x)).

def TauCeti.dualitySet (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (x : E) : Set (StrongDual 𝕜 E)

The (normalized) duality set J(x) of a vector x in a normed space: the continuous linear functionals x' with x' x = ‖x‖² and ‖x'‖ = ‖x‖.

Equations

• TauCeti.dualitySet 𝕜 x = {f : StrongDual 𝕜 E | f x = ↑‖x‖ ^ 2 ∧ ‖f‖ = ‖x‖}

@[simp]

theorem TauCeti.mem_dualitySet_iff {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {f : StrongDual 𝕜 E} : f ∈ dualitySet 𝕜 x ↔ f x = ↑‖x‖ ^ 2 ∧ ‖f‖ = ‖x‖

Membership in the duality set unfolds to its two defining conditions.

theorem TauCeti.mem_dualitySet_iff_norm_le {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {f : StrongDual 𝕜 E} : f ∈ dualitySet 𝕜 x ↔ f x = ↑‖x‖ ^ 2 ∧ ‖f‖ ≤ ‖x‖

In the definition of the duality set the norm condition may be weakened to ‖x'‖ ≤ ‖x‖: the reverse inequality is forced by x' x = ‖x‖².

theorem TauCeti.smul_mem_dualitySet {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {g : StrongDual 𝕜 E} (hg : ‖g‖ ≤ 1) (hgx : g x = ↑‖x‖) : ↑‖x‖ • g ∈ dualitySet 𝕜 x

Rescaling a norming functional: if ‖g‖ ≤ 1 and g x = ‖x‖, then ‖x‖ • g lies in the duality set of x.

theorem TauCeti.star_smul_mem_dualitySet {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {f : StrongDual 𝕜 E} (hf : f ∈ dualitySet 𝕜 x) (c : 𝕜) : star c • f ∈ dualitySet 𝕜 (c • x)

Multiplying a vector by a scalar multiplies its norming functional by the conjugate scalar.

theorem TauCeti.dualitySet_nonempty (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (x : E) : (dualitySet 𝕜 x).Nonempty

The duality set is nonempty, by the Hahn--Banach theorem.

@[simp]

theorem TauCeti.dualitySet_zero {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] : dualitySet 𝕜 0 = {0}

The duality set of the zero vector consists of the zero functional alone.

@[simp]

theorem TauCeti.dualitySet_smul {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (c : 𝕜) (x : E) : dualitySet 𝕜 (c • x) = star c • dualitySet 𝕜 x

The duality set is conjugate-homogeneous under scalar multiplication.

@[simp]

theorem TauCeti.dualitySet_neg {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (x : E) : dualitySet 𝕜 (-x) = -1 • dualitySet 𝕜 x

Negating a vector negates its duality set.