mathlib documentation

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 #

Tags #

dual

@[protected, instance]
def normed_space.dual.inhabited (๐•œ : Type u_1) [nontrivially_normed_field ๐•œ] (E : Type u_2) [seminormed_add_comm_group E] [normed_space ๐•œ E] :
@[protected, instance]
noncomputable def normed_space.dual.seminormed_add_comm_group (๐•œ : Type u_1) [nontrivially_normed_field ๐•œ] (E : Type u_2) [seminormed_add_comm_group E] [normed_space ๐•œ E] :
@[protected, instance]
def normed_space.dual.normed_space (๐•œ : Type u_1) [nontrivially_normed_field ๐•œ] (E : Type u_2) [seminormed_add_comm_group E] [normed_space ๐•œ E] :
normed_space ๐•œ (normed_space.dual ๐•œ E)
@[protected, instance]
def normed_space.continuous_linear_map_class (๐•œ : Type u_1) [nontrivially_normed_field ๐•œ] (E : Type u_2) [seminormed_add_comm_group E] [normed_space ๐•œ E] :
continuous_linear_map_class (normed_space.dual ๐•œ E) ๐•œ E ๐•œ
Equations
@[protected, instance]
def normed_space.dual.has_coe_to_fun (๐•œ : Type u_1) [nontrivially_normed_field ๐•œ] (E : Type u_2) [seminormed_add_comm_group E] [normed_space ๐•œ E] :
has_coe_to_fun (normed_space.dual ๐•œ E) (ฮป (_x : normed_space.dual ๐•œ E), E โ†’ ๐•œ)
Equations
@[protected, instance]
noncomputable def normed_space.dual.normed_add_comm_group (๐•œ : Type u_1) [nontrivially_normed_field ๐•œ] (F : Type u_3) [normed_add_comm_group F] [normed_space ๐•œ F] :
Equations
@[protected, instance]
def normed_space.dual.finite_dimensional (๐•œ : Type u_1) [nontrivially_normed_field ๐•œ] (E : Type u_2) [seminormed_add_comm_group E] [normed_space ๐•œ E] [finite_dimensional ๐•œ E] :
finite_dimensional ๐•œ (normed_space.dual ๐•œ E)
noncomputable def normed_space.inclusion_in_double_dual (๐•œ : Type u_1) [nontrivially_normed_field ๐•œ] (E : Type u_2) [seminormed_add_comm_group E] [normed_space ๐•œ E] :
E โ†’L[๐•œ] normed_space.dual ๐•œ (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) [nontrivially_normed_field ๐•œ] (E : Type u_2) [seminormed_add_comm_group E] [normed_space ๐•œ E] (x : E) (f : normed_space.dual ๐•œ E) :
def normed_space.dual_pairing (๐•œ : Type u_1) [nontrivially_normed_field ๐•œ] (E : Type u_2) [seminormed_add_comm_group E] [normed_space ๐•œ E] :
normed_space.dual ๐•œ E โ†’โ‚—[๐•œ] E โ†’โ‚—[๐•œ] ๐•œ

The dual pairing as a bilinear form.

Equations
@[simp]
theorem normed_space.dual_pairing_apply (๐•œ : Type u_1) [nontrivially_normed_field ๐•œ] (E : Type u_2) [seminormed_add_comm_group E] [normed_space ๐•œ E] {v : normed_space.dual ๐•œ E} {x : E} :
theorem normed_space.dual_pairing_separating_left (๐•œ : Type u_1) [nontrivially_normed_field ๐•œ] (E : Type u_2) [seminormed_add_comm_group E] [normed_space ๐•œ E] :
theorem normed_space.norm_le_dual_bound (๐•œ : Type v) [is_R_or_C ๐•œ] {E : Type u} [normed_add_comm_group E] [normed_space ๐•œ E] (x : E) {M : โ„} (hMp : 0 โ‰ค M) (hM : โˆ€ (f : normed_space.dual ๐•œ 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_add_comm_group E] [normed_space ๐•œ E] {x : E} (h : โˆ€ (f : normed_space.dual ๐•œ 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_add_comm_group E] [normed_space ๐•œ E] (x : E) :
x = 0 โ†” โˆ€ (g : normed_space.dual ๐•œ E), โ‡‘g x = 0
theorem normed_space.eq_iff_forall_dual_eq (๐•œ : Type v) [is_R_or_C ๐•œ] {E : Type u} [normed_add_comm_group E] [normed_space ๐•œ E] {x y : E} :
x = y โ†” โˆ€ (g : normed_space.dual ๐•œ 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_add_comm_group E] [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) [nontrivially_normed_field ๐•œ] {E : Type u_2} [seminormed_add_comm_group E] [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) [nontrivially_normed_field ๐•œ] {E : Type u_2} [seminormed_add_comm_group E] [normed_space ๐•œ E] {x' : normed_space.dual ๐•œ E} (s : set E) :
x' โˆˆ normed_space.polar ๐•œ s โ†” โˆ€ (z : E), z โˆˆ s โ†’ โˆฅโ‡‘x' zโˆฅ โ‰ค 1
@[simp]
theorem normed_space.polar_univ (๐•œ : Type u_1) [nontrivially_normed_field ๐•œ] {E : Type u_2} [seminormed_add_comm_group E] [normed_space ๐•œ E] :
theorem normed_space.is_closed_polar (๐•œ : Type u_1) [nontrivially_normed_field ๐•œ] {E : Type u_2} [seminormed_add_comm_group E] [normed_space ๐•œ E] (s : set E) :
@[simp]
theorem normed_space.polar_closure (๐•œ : Type u_1) [nontrivially_normed_field ๐•œ] {E : Type u_2} [seminormed_add_comm_group E] [normed_space ๐•œ E] (s : set E) :
theorem normed_space.smul_mem_polar {๐•œ : Type u_1} [nontrivially_normed_field ๐•œ] {E : Type u_2} [seminormed_add_comm_group E] [normed_space ๐•œ E] {s : set E} {x' : normed_space.dual ๐•œ 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} [nontrivially_normed_field ๐•œ] {E : Type u_2} [seminormed_add_comm_group E] [normed_space ๐•œ E] {c : ๐•œ} (hc : 1 < โˆฅcโˆฅ) {r : โ„} (hr : 0 < r) :
theorem normed_space.polar_closed_ball {๐•œ : Type u_1} {E : Type u_2} [is_R_or_C ๐•œ] [normed_add_comm_group E] [normed_space ๐•œ E] {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 normed_space.bounded_polar_of_mem_nhds_zero (๐•œ : Type u_1) [nontrivially_normed_field ๐•œ] {E : Type u_2} [seminormed_add_comm_group E] [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.