mathlib3 documentation

analysis.normed_space.dual

The topological dual of a normed space #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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]
@[protected, instance]

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) :

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.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

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
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.

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.