# 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

@[reducible, inline]
abbrev NormedSpace.Dual (๐ : Type u_1) [] (E : Type u_2) [NormedSpace ๐ E] :
Type (max u_1 u_2)

The topological dual of a seminormed space E.

Equations
Instances For
instance NormedSpace.instDual (๐ : Type u_1) [] (E : Type u_2) [NormedSpace ๐ E] :
NormedSpace ๐ (NormedSpace.Dual ๐ E)
Equations
instance NormedSpace.instSeminormedAddCommGroupDual (๐ : Type u_1) [] (E : Type u_2) [NormedSpace ๐ E] :
Equations
• = inferInstance
def NormedSpace.inclusionInDoubleDual (๐ : Type u_1) [] (E : Type u_2) [NormedSpace ๐ E] :
E โL[๐] NormedSpace.Dual ๐ (NormedSpace.Dual ๐ E)

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

Equations
Instances For
@[simp]
theorem NormedSpace.dual_def (๐ : Type u_1) [] (E : Type u_2) [NormedSpace ๐ E] (x : E) (f : NormedSpace.Dual ๐ E) :
( x) f = f x
theorem NormedSpace.inclusionInDoubleDual_norm_eq (๐ : Type u_1) [] (E : Type u_2) [NormedSpace ๐ E] :
theorem NormedSpace.inclusionInDoubleDual_norm_le (๐ : Type u_1) [] (E : Type u_2) [NormedSpace ๐ E] :
theorem NormedSpace.double_dual_bound (๐ : Type u_1) [] (E : Type u_2) [NormedSpace ๐ E] (x : E) :
def NormedSpace.dualPairing (๐ : Type u_1) [] (E : Type u_2) [NormedSpace ๐ E] :
NormedSpace.Dual ๐ E โโ[๐] E โโ[๐] ๐

The dual pairing as a bilinear form.

Equations
Instances For
@[simp]
theorem NormedSpace.dualPairing_apply (๐ : Type u_1) [] (E : Type u_2) [NormedSpace ๐ E] {v : NormedSpace.Dual ๐ E} {x : E} :
((NormedSpace.dualPairing ๐ E) v) x = v x
theorem NormedSpace.dualPairing_separatingLeft (๐ : Type u_1) [] (E : Type u_2) [NormedSpace ๐ E] :
(NormedSpace.dualPairing ๐ E).SeparatingLeft
theorem NormedSpace.norm_le_dual_bound (๐ : Type v) [RCLike ๐] {E : Type u} [NormedSpace ๐ E] (x : E) {M : โ} (hMp : 0 โค M) (hM : โ (f : NormedSpace.Dual ๐ E), โf xโ โค M * ) :

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

theorem NormedSpace.eq_zero_of_forall_dual_eq_zero (๐ : Type v) [RCLike ๐] {E : Type u} [NormedSpace ๐ E] {x : E} (h : โ (f : NormedSpace.Dual ๐ E), f x = 0) :
x = 0
theorem NormedSpace.eq_zero_iff_forall_dual_eq_zero (๐ : Type v) [RCLike ๐] {E : Type u} [NormedSpace ๐ E] (x : E) :
x = 0 โ โ (g : NormedSpace.Dual ๐ E), g x = 0
theorem NormedSpace.eq_iff_forall_dual_eq (๐ : Type v) [RCLike ๐] {E : Type u} [NormedSpace ๐ E] {x : E} {y : E} :
x = y โ โ (g : NormedSpace.Dual ๐ E), g x = g y

See also geometric_hahn_banach_point_point.

def NormedSpace.inclusionInDoubleDualLi (๐ : Type v) [RCLike ๐] {E : Type u} [NormedSpace ๐ E] :

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

Equations
• = let __src := ; { toLinearMap := โ__src, norm_map' := โฏ }
Instances For
def NormedSpace.polar (๐ : Type u_1) [] {E : Type u_2} [NormedSpace ๐ E] :
Set E โ Set (NormedSpace.Dual ๐ E)

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.

Equations
Instances For
theorem NormedSpace.mem_polar_iff (๐ : Type u_1) [] {E : Type u_2} [NormedSpace ๐ E] {x' : NormedSpace.Dual ๐ E} (s : Set E) :
x' โ NormedSpace.polar ๐ s โ โ z โ s, โx' zโ โค 1
@[simp]
theorem NormedSpace.polar_univ (๐ : Type u_1) [] {E : Type u_2} [NormedSpace ๐ E] :
NormedSpace.polar ๐ Set.univ = {0}
theorem NormedSpace.isClosed_polar (๐ : Type u_1) [] {E : Type u_2} [NormedSpace ๐ E] (s : Set E) :
@[simp]
theorem NormedSpace.polar_closure (๐ : Type u_1) [] {E : Type u_2} [NormedSpace ๐ E] (s : Set E) :
NormedSpace.polar ๐ (closure s) = NormedSpace.polar ๐ s
theorem NormedSpace.smul_mem_polar {๐ : Type u_1} [] {E : Type u_2} [NormedSpace ๐ E] {s : Set E} {x' : NormedSpace.Dual ๐ E} {c : ๐} (hc : โ z โ s, โx' zโ โค ) :

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} [NormedSpace ๐ E] {c : ๐} (hc : 1 < ) {r : โ} (hr : 0 < r) :
theorem NormedSpace.closedBall_inv_subset_polar_closedBall (๐ : Type u_1) [] {E : Type u_2} [NormedSpace ๐ E] {r : โ} :
theorem NormedSpace.polar_closedBall {๐ : Type u_3} {E : Type u_4} [RCLike ๐] [NormedSpace ๐ E] {r : โ} (hr : 0 < r) :
NormedSpace.polar ๐ =

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} [NormedSpace ๐ E] {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.