# mathlibdocumentation

analysis.normed_space.dual

# The topological dual of a normed space #

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

For base field ๐ = โ or ๐ = โ, this map is actually an isometric embedding; we provide a version normed_space.inclusion_in_double_dual_li 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 seminormed_add_comm_group and we specialize to normed_add_comm_group when needed.

## Main definitions #

• inclusion_in_double_dual and inclusion_in_double_dual_li 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

@[protected, instance]
def normed_space.dual.inhabited (๐ : Type u_1) (E : Type u_2) [normed_space ๐ E] :
def normed_space.dual (๐ : Type u_1) (E : Type u_2) [normed_space ๐ E] :
Type (max u_2 u_1)

The topological dual of a seminormed space E.

Equations
Instances for normed_space.dual
@[protected, instance]
noncomputable def normed_space.dual.seminormed_add_comm_group (๐ : Type u_1) (E : Type u_2) [normed_space ๐ E] :
@[protected, instance]
def normed_space.dual.normed_space (๐ : Type u_1) (E : Type u_2) [normed_space ๐ E] :
normed_space ๐ (normed_space.dual ๐ E)
@[protected, instance]
def normed_space.continuous_linear_map_class (๐ : Type u_1) (E : Type u_2) [normed_space ๐ E] :
๐ E ๐
Equations
@[protected, instance]
def normed_space.dual.has_coe_to_fun (๐ : Type u_1) (E : Type u_2) [normed_space ๐ E] :
has_coe_to_fun (normed_space.dual ๐ E) (ฮป (_x : E), E โ ๐)
Equations
@[protected, instance]
noncomputable def normed_space.dual.normed_add_comm_group (๐ : Type u_1) (F : Type u_3) [normed_space ๐ F] :
Equations
@[protected, instance]
def normed_space.dual.finite_dimensional (๐ : Type u_1) (E : Type u_2) [normed_space ๐ E] [ E] :
(normed_space.dual ๐ E)
noncomputable def normed_space.inclusion_in_double_dual (๐ : Type u_1) (E : Type u_2) [normed_space ๐ E] :
E โL[๐] (normed_space.dual ๐ E)

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

Equations
• = ๐
@[simp]
theorem normed_space.dual_def (๐ : Type u_1) (E : Type u_2) [normed_space ๐ E] (x : E) (f : E) :
theorem normed_space.inclusion_in_double_dual_norm_eq (๐ : Type u_1) (E : Type u_2) [normed_space ๐ E] :
theorem normed_space.inclusion_in_double_dual_norm_le (๐ : Type u_1) (E : Type u_2) [normed_space ๐ E] :
theorem normed_space.double_dual_bound (๐ : Type u_1) (E : Type u_2) [normed_space ๐ E] (x : E) :
def normed_space.dual_pairing (๐ : Type u_1) (E : Type u_2) [normed_space ๐ E] :
E โโ[๐] E โโ[๐] ๐

The dual pairing as a bilinear form.

Equations
@[simp]
theorem normed_space.dual_pairing_apply (๐ : Type u_1) (E : Type u_2) [normed_space ๐ E] {v : E} {x : E} :
theorem normed_space.dual_pairing_separating_left (๐ : Type u_1) (E : Type u_2) [normed_space ๐ E] :
theorem normed_space.norm_le_dual_bound (๐ : Type v) [is_R_or_C ๐] {E : Type u} [normed_space ๐ E] (x : E) {M : โ} (hMp : 0 โค M) (hM : โ (f : E), โฅโf xโฅ โค M * โฅfโฅ) :

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

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

See also geometric_hahn_banach_point_point.

noncomputable def normed_space.inclusion_in_double_dual_li (๐ : Type v) [is_R_or_C ๐] {E : Type u} [normed_space ๐ E] :

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

Equations
def normed_space.polar (๐ : Type u_1) {E : Type u_2} [normed_space ๐ E] :
set E โ set (normed_space.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
theorem normed_space.mem_polar_iff (๐ : Type u_1) {E : Type u_2} [normed_space ๐ E] {x' : E} (s : set E) :
x' โ s โ โ (z : E), z โ s โ โฅโx' zโฅ โค 1
@[simp]
theorem normed_space.polar_univ (๐ : Type u_1) {E : Type u_2} [normed_space ๐ E] :
= {0}
theorem normed_space.is_closed_polar (๐ : Type u_1) {E : Type u_2} [normed_space ๐ E] (s : set E) :
@[simp]
theorem normed_space.polar_closure (๐ : Type u_1) {E : Type u_2} [normed_space ๐ E] (s : set E) :
(closure s) = s
theorem normed_space.smul_mem_polar {๐ : Type u_1} {E : Type u_2} [normed_space ๐ E] {s : set E} {x' : E} {c : ๐} (hc : โ (z : E), z โ s โ โฅโx' 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 normed_space.polar_ball_subset_closed_ball_div {๐ : Type u_1} {E : Type u_2} [normed_space ๐ E] {c : ๐} (hc : 1 < โฅcโฅ) {r : โ} (hr : 0 < r) :
theorem normed_space.closed_ball_inv_subset_polar_closed_ball (๐ : Type u_1) {E : Type u_2} [normed_space ๐ E] {r : โ} :
theorem normed_space.polar_closed_ball {๐ : Type u_1} {E : Type u_2} [is_R_or_C ๐] [normed_space ๐ E] {r : โ} (hr : 0 < r) :
r) =

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

theorem normed_space.bounded_polar_of_mem_nhds_zero (๐ : Type u_1) {E : Type u_2} [normed_space ๐ 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.