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 #

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) [nontrivially_normed_field 𝕜] (E : Type u_2) [seminormed_add_comm_group E] [normed_space 𝕜 E] :

inhabited (normed_space.dual 𝕜 E)

def normed_space.dual (𝕜 : Type u_1) [nontrivially_normed_field 𝕜] (E : Type u_2) [seminormed_add_comm_group E] [normed_space 𝕜 E] :

Type (max u_2 u_1)

The topological dual of a seminormed space E.

Equations

normed_space.dual 𝕜 E = (E →L[𝕜] 𝕜)

Instances for normed_space.dual

@[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] :

seminormed_add_comm_group (normed_space.dual 𝕜 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

normed_space.continuous_linear_map_class 𝕜 E = continuous_linear_map.continuous_semilinear_map_class

@[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

normed_space.dual.has_coe_to_fun 𝕜 E = continuous_linear_map.to_fun

@[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] :

normed_add_comm_group (normed_space.dual 𝕜 F)

Equations

normed_space.dual.normed_add_comm_group 𝕜 F = continuous_linear_map.to_normed_add_comm_group

@[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

normed_space.inclusion_in_double_dual 𝕜 E = continuous_linear_map.apply 𝕜 𝕜

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

⇑(⇑(normed_space.inclusion_in_double_dual 𝕜 E) x) f = ⇑f x

theorem normed_space.inclusion_in_double_dual_norm_eq (𝕜 : Type u_1) [nontrivially_normed_field 𝕜] (E : Type u_2) [seminormed_add_comm_group E] [normed_space 𝕜 E] :

∥normed_space.inclusion_in_double_dual 𝕜 E∥ = ∥continuous_linear_map.id 𝕜 (normed_space.dual 𝕜 E)∥

theorem normed_space.inclusion_in_double_dual_norm_le (𝕜 : Type u_1) [nontrivially_normed_field 𝕜] (E : Type u_2) [seminormed_add_comm_group E] [normed_space 𝕜 E] :

∥normed_space.inclusion_in_double_dual 𝕜 E∥ ≤ 1

theorem normed_space.double_dual_bound (𝕜 : Type u_1) [nontrivially_normed_field 𝕜] (E : Type u_2) [seminormed_add_comm_group E] [normed_space 𝕜 E] (x : E) :

∥⇑(normed_space.inclusion_in_double_dual 𝕜 E) x∥ ≤ ∥x∥

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

normed_space.dual_pairing 𝕜 E = continuous_linear_map.coe_lm 𝕜

@[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} :

⇑(⇑(normed_space.dual_pairing 𝕜 E) v) x = ⇑v x

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

(normed_space.dual_pairing 𝕜 E).separating_left

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

E →ₗᵢ[𝕜] normed_space.dual 𝕜 (normed_space.dual 𝕜 E)

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

Equations

normed_space.inclusion_in_double_dual_li 𝕜 = {to_linear_map := (normed_space.inclusion_in_double_dual 𝕜 E).to_linear_map, norm_map' := _}

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

normed_space.polar 𝕜 = (normed_space.dual_pairing 𝕜 E).flip.polar

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

normed_space.polar 𝕜 set.univ = {0}

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

is_closed (normed_space.polar 𝕜 s)

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

normed_space.polar 𝕜 (closure s) = normed_space.polar 𝕜 s

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

c⁻¹ • x' ∈ normed_space.polar 𝕜 s

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

normed_space.polar 𝕜 (metric.ball 0 r) ⊆ metric.closed_ball 0 (∥c∥ / r)

theorem normed_space.closed_ball_inv_subset_polar_closed_ball (𝕜 : Type u_1) [nontrivially_normed_field 𝕜] {E : Type u_2} [seminormed_add_comm_group E] [normed_space 𝕜 E] {r : ℝ} :

metric.closed_ball 0 r⁻¹ ⊆ normed_space.polar 𝕜 (metric.closed_ball 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) :

normed_space.polar 𝕜 (metric.closed_ball 0 r) = metric.closed_ball 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) :

metric.bounded (normed_space.polar 𝕜 s)

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.