# Documentation

Mathlib.Analysis.NormedSpace.Dual

# The topological dual of a normed space #

In this file we define the topological dual NormedSpace.Dual of a normed space, and the continuous linear map NormedSpace.inclusionInDoubleDual from a normed space into its double dual.

For base field 𝕜 = ℝ or 𝕜 = ℂ, this map is actually an isometric embedding; we provide a version NormedSpace.inclusionInDoubleDualLi of the map which is of type a bundled linear isometric embedding, E →ₗᵢ[𝕜] (Dual 𝕜 (Dual 𝕜 E)).

Since a lot of elementary properties don't require eq_of_dist_eq_zero we start setting up the theory for SeminormedAddCommGroup and we specialize to NormedAddCommGroup when needed.

## Main definitions #

• inclusionInDoubleDual and inclusionInDoubleDualLi are the inclusion of a normed space in its double dual, considered as a bounded linear map and as a linear isometry, respectively.
• polar 𝕜 s is the subset of Dual 𝕜 E consisting of those functionals x' for which ‖x' z‖ ≤ 1 for every z ∈ s.

## Tags #

dual

@[inline, reducible]
abbrev NormedSpace.Dual (𝕜 : Type u_1) (E : Type u_2) [] :
Type (max u_2 u_1)

The topological dual of a seminormed space E.

Instances For
instance NormedSpace.instSeminormedAddCommGroupDual (𝕜 : Type u_1) (E : Type u_2) [] :
def NormedSpace.inclusionInDoubleDual (𝕜 : Type u_1) (E : Type u_2) [] :
E →L[𝕜]

The inclusion of a normed space in its double (topological) dual, considered as a bounded linear map.

Instances For
@[simp]
theorem NormedSpace.dual_def (𝕜 : Type u_1) (E : Type u_2) [] (x : E) (f : ) :
↑() f = f x
theorem NormedSpace.inclusionInDoubleDual_norm_eq (𝕜 : Type u_1) (E : Type u_2) [] :
theorem NormedSpace.inclusionInDoubleDual_norm_le (𝕜 : Type u_1) (E : Type u_2) [] :
theorem NormedSpace.double_dual_bound (𝕜 : Type u_1) (E : Type u_2) [] (x : E) :
def NormedSpace.dualPairing (𝕜 : Type u_1) (E : Type u_2) [] :
→ₗ[𝕜] E →ₗ[𝕜] 𝕜

The dual pairing as a bilinear form.

Instances For
@[simp]
theorem NormedSpace.dualPairing_apply (𝕜 : Type u_1) (E : Type u_2) [] {v : } {x : E} :
↑(↑() v) x = v x
theorem NormedSpace.dualPairing_separatingLeft (𝕜 : Type u_1) (E : Type u_2) [] :
theorem NormedSpace.norm_le_dual_bound (𝕜 : Type v) [] {E : Type u} [] (x : E) {M : } (hMp : 0 M) (hM : ∀ (f : ), f x M * f) :

If one controls the norm of every f x, then one controls the norm of x. Compare ContinuousLinearMap.op_norm_le_bound.

theorem NormedSpace.eq_zero_of_forall_dual_eq_zero (𝕜 : Type v) [] {E : Type u} [] {x : E} (h : ∀ (f : ), f x = 0) :
x = 0
theorem NormedSpace.eq_zero_iff_forall_dual_eq_zero (𝕜 : Type v) [] {E : Type u} [] (x : E) :
x = 0 ∀ (g : ), g x = 0
theorem NormedSpace.eq_iff_forall_dual_eq (𝕜 : Type v) [] {E : Type u} [] {x : E} {y : E} :
x = y ∀ (g : ), g x = g y

See also geometric_hahn_banach_point_point.

def NormedSpace.inclusionInDoubleDualLi (𝕜 : Type v) [] {E : Type u} [] :

The inclusion of a normed space in its double dual is an isometry onto its image.

Instances For
def NormedSpace.polar (𝕜 : Type u_1) {E : Type u_2} [] :
Set ESet ()

Given a subset s in a normed space E (over a field 𝕜), the polar polar 𝕜 s is the subset of Dual 𝕜 E consisting of those functionals which evaluate to something of norm at most one at all points z ∈ s.

Instances For
theorem NormedSpace.mem_polar_iff (𝕜 : Type u_1) {E : Type u_2} [] {x' : } (s : Set E) :
x' ∀ (z : E), z sx' z 1
@[simp]
theorem NormedSpace.polar_univ (𝕜 : Type u_1) {E : Type u_2} [] :
NormedSpace.polar 𝕜 Set.univ = {0}
theorem NormedSpace.isClosed_polar (𝕜 : Type u_1) {E : Type u_2} [] (s : Set E) :
@[simp]
theorem NormedSpace.polar_closure (𝕜 : Type u_1) {E : Type u_2} [] (s : Set E) :
=
theorem NormedSpace.smul_mem_polar {𝕜 : Type u_1} {E : Type u_2} [] {s : Set E} {x' : } {c : 𝕜} (hc : ∀ (z : E), z sx' z c) :

If x' is a dual element such that the norms ‖x' z‖ are bounded for z ∈ s, then a small scalar multiple of x' is in polar 𝕜 s.

theorem NormedSpace.polar_ball_subset_closedBall_div {𝕜 : Type u_1} {E : Type u_2} [] {c : 𝕜} (hc : 1 < c) {r : } (hr : 0 < r) :
theorem NormedSpace.closedBall_inv_subset_polar_closedBall (𝕜 : Type u_1) {E : Type u_2} [] {r : } :
theorem NormedSpace.polar_closedBall {𝕜 : Type u_3} {E : Type u_4} [] [] {r : } (hr : 0 < r) :

The polar of closed ball in a normed space E is the closed ball of the dual with inverse radius.

theorem NormedSpace.isBounded_polar_of_mem_nhds_zero (𝕜 : Type u_1) {E : Type u_2} [] {s : Set E} (s_nhd : s nhds 0) :

Given a neighborhood s of the origin in a normed space E, the dual norms of all elements of the polar polar 𝕜 s are bounded by a constant.