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.

References

• [Conway, John B., A course in functional analysis][conway1990]

Tags

dual, polar

@[reducible, inline]

abbrev NormedSpace.Dual (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (E : Type u_2) [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] : Type (max u_1 u_2)

The topological dual of a seminormed space E.

Equations

• NormedSpace.Dual 𝕜 E = (E →L[𝕜] 𝕜)

def NormedSpace.inclusionInDoubleDual (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (E : Type u_2) [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] : E →L[𝕜] Dual 𝕜 (Dual 𝕜 E)

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

Equations

• NormedSpace.inclusionInDoubleDual 𝕜 E = ContinuousLinearMap.apply 𝕜 𝕜

@[simp]

theorem NormedSpace.dual_def (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (E : Type u_2) [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] (x : E) (f : Dual 𝕜 E) : ((inclusionInDoubleDual 𝕜 E) x) f = f x

theorem NormedSpace.inclusionInDoubleDual_norm_eq (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (E : Type u_2) [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] : ‖inclusionInDoubleDual 𝕜 E‖ = ‖ContinuousLinearMap.id 𝕜 (Dual 𝕜 E)‖

theorem NormedSpace.inclusionInDoubleDual_norm_le (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (E : Type u_2) [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] : ‖inclusionInDoubleDual 𝕜 E‖ ≤ 1

theorem NormedSpace.double_dual_bound (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (E : Type u_2) [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] (x : E) : ‖(inclusionInDoubleDual 𝕜 E) x‖ ≤ ‖x‖

def NormedSpace.dualPairing (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (E : Type u_2) [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] : Dual 𝕜 E →ₗ[𝕜] E →ₗ[𝕜] 𝕜

The dual pairing as a bilinear form.

Equations

• NormedSpace.dualPairing 𝕜 E = ContinuousLinearMap.coeLM 𝕜

@[simp]

theorem NormedSpace.dualPairing_apply (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (E : Type u_2) [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {v : Dual 𝕜 E} {x : E} : ((dualPairing 𝕜 E) v) x = v x

theorem NormedSpace.dualPairing_separatingLeft (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (E : Type u_2) [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] : (dualPairing 𝕜 E).SeparatingLeft

theorem NormedSpace.norm_le_dual_bound (𝕜 : Type v) [RCLike 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (x : E) {M : ℝ} (hMp : 0 ≤ M) (hM : ∀ (f : Dual 𝕜 E), ‖f x‖ ≤ M * ‖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} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} (h : ∀ (f : Dual 𝕜 E), f x = 0) : x = 0

theorem NormedSpace.eq_zero_iff_forall_dual_eq_zero (𝕜 : Type v) [RCLike 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (x : E) : x = 0 ↔ ∀ (g : Dual 𝕜 E), g x = 0

theorem NormedSpace.eq_iff_forall_dual_eq (𝕜 : Type v) [RCLike 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x y : E} : x = y ↔ ∀ (g : Dual 𝕜 E), g x = g y

See also geometric_hahn_banach_point_point.

def NormedSpace.inclusionInDoubleDualLi (𝕜 : Type v) [RCLike 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] : E →ₗᵢ[𝕜] Dual 𝕜 (Dual 𝕜 E)

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

Equations

• NormedSpace.inclusionInDoubleDualLi 𝕜 = { toLinearMap := ↑(NormedSpace.inclusionInDoubleDual 𝕜 E), norm_map' := ⋯ }

def NormedSpace.polar (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] : Set E → Set (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

• NormedSpace.polar 𝕜 = (NormedSpace.dualPairing 𝕜 E).flip.polar

def NormedSpace.polarSubmodule (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {S : Type u_3} [SetLike S E] [SMulMemClass S 𝕜 E] (m : S) : Submodule 𝕜 (Dual 𝕜 E)

Given a subset s in a normed space E (over a field 𝕜) closed under scalar multiplication, the polar polarSubmodule 𝕜 s is the submodule of Dual 𝕜 E consisting of those functionals which evaluate to zero at all points z ∈ s.

Equations

• NormedSpace.polarSubmodule 𝕜 m = (NormedSpace.dualPairing 𝕜 E).flip.polarSubmodule m

theorem NormedSpace.polarSubmodule_eq_polar (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] (m : SubMulAction 𝕜 E) : ↑(polarSubmodule 𝕜 m) = polar 𝕜 ↑m

theorem NormedSpace.mem_polar_iff (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {x' : Dual 𝕜 E} (s : Set E) : x' ∈ polar 𝕜 s ↔ ∀ z ∈ s, ‖x' z‖ ≤ 1

theorem NormedSpace.polarSubmodule_eq_setOf (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {S : Type u_3} [SetLike S E] [SMulMemClass S 𝕜 E] (m : S) : ↑(polarSubmodule 𝕜 m) = {y : Dual 𝕜 E | ∀ x ∈ m, y x = 0}

theorem NormedSpace.mem_polarSubmodule (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {S : Type u_3} [SetLike S E] [SMulMemClass S 𝕜 E] (m : S) (y : Dual 𝕜 E) : y ∈ polarSubmodule 𝕜 m ↔ ∀ x ∈ m, y x = 0

@[simp]

theorem NormedSpace.zero_mem_polar (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] (s : Set E) : 0 ∈ polar 𝕜 s

theorem NormedSpace.polar_nonempty (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] (s : Set E) : (polar 𝕜 s).Nonempty

@[simp]

theorem NormedSpace.polar_univ (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] : polar 𝕜 Set.univ = {0}

theorem NormedSpace.isClosed_polar (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] (s : Set E) : IsClosed (polar 𝕜 s)

@[simp]

theorem NormedSpace.polar_closure (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] (s : Set E) : polar 𝕜 (closure s) = polar 𝕜 s

theorem NormedSpace.smul_mem_polar {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Set E} {x' : Dual 𝕜 E} {c : 𝕜} (hc : ∀ z ∈ s, ‖x' z‖ ≤ ‖c‖) : c⁻¹ • x' ∈ 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 NormedSpace.polar_ball_subset_closedBall_div {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {c : 𝕜} (hc : 1 < ‖c‖) {r : ℝ} (hr : 0 < r) : polar 𝕜 (Metric.ball 0 r) ⊆ Metric.closedBall 0 (‖c‖ / r)

theorem NormedSpace.closedBall_inv_subset_polar_closedBall (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {r : ℝ} : Metric.closedBall 0 r⁻¹ ⊆ polar 𝕜 (Metric.closedBall 0 r)

theorem NormedSpace.polar_closedBall {𝕜 : Type u_3} {E : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {r : ℝ} (hr : 0 < r) : polar 𝕜 (Metric.closedBall 0 r) = Metric.closedBall 0 r⁻¹

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

theorem NormedSpace.polar_ball {𝕜 : Type u_3} {E : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {r : ℝ} (hr : 0 < r) : polar 𝕜 (Metric.ball 0 r) = Metric.closedBall 0 r⁻¹

theorem NormedSpace.isBounded_polar_of_mem_nhds_zero (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Set E} (s_nhd : s ∈ nhds 0) : Bornology.IsBounded (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.

@[simp]

theorem NormedSpace.polar_empty (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] : polar 𝕜 ∅ = Set.univ

@[simp]

theorem NormedSpace.polar_singleton (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {a : E} : polar 𝕜 {a} = {x : Dual 𝕜 E | ‖x a‖ ≤ 1}

theorem NormedSpace.mem_polar_singleton (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {a : E} (y : Dual 𝕜 E) : y ∈ polar 𝕜 {a} ↔ ‖y a‖ ≤ 1

theorem NormedSpace.polar_zero (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] : polar 𝕜 {0} = Set.univ

theorem NormedSpace.sInter_polar_eq_closedBall {𝕜 : Type u_3} {E : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {r : ℝ} (hr : 0 < r) : ⋂₀ (polar 𝕜 '' {F : Set E | F.Finite ∧ F ⊆ Metric.closedBall 0 r⁻¹}) = Metric.closedBall 0 r

theorem LinearMap.polar_AbsConvex {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedField 𝕜] [NormedSpace ℝ 𝕜] [AddCommMonoid E] [AddCommMonoid F] [Module 𝕜 E] [Module 𝕜 F] {B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜} (s : Set E) [Module ℝ F] [IsScalarTower ℝ 𝕜 F] [IsScalarTower ℝ 𝕜 𝕜] : AbsConvex 𝕜 (B.polar s)