The strong dual of a normed space

In this file we consider the strong dual StrongDual of a normed space, and the continuous linear map NormedSpace.inclusionInDoubleDual from a normed space into its double StrongDual.

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 →ₗᵢ[𝕜] (StrongDual 𝕜 (StrongDual 𝕜 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 StrongDual, considered as a bounded linear map and as a linear isometry, respectively.
• polar 𝕜 s is the subset of StrongDual 𝕜 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

strong dual, polar

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

The inclusion of a normed space in its double (topological) strong 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 : StrongDual 𝕜 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 𝕜 (StrongDual 𝕜 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‖

theorem NormedSpace.norm_le_dual_bound (𝕜 : Type v) [RCLike 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (x : E) {M : ℝ} (hMp : 0 ≤ M) (hM : ∀ (f : StrongDual 𝕜 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 : StrongDual 𝕜 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 : StrongDual 𝕜 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 : StrongDual 𝕜 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 →ₗᵢ[𝕜] StrongDual 𝕜 (StrongDual 𝕜 E)

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

Equations

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

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

@[simp]

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

theorem NormedSpace.smul_mem_polar {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Set E} {x' : StrongDual 𝕜 E} {c : 𝕜} (hc : ∀ z ∈ s, ‖x' z‖ ≤ ‖c‖) : c⁻¹ • x' ∈ StrongDual.polar 𝕜 s

If x' is a StrongDual 𝕜 E 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) : StrongDual.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⁻¹ ⊆ StrongDual.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) : StrongDual.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) : StrongDual.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_nhds : s ∈ nhds 0) : Bornology.IsBounded (StrongDual.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.

theorem NormedSpace.sInter_polar_eq_closedBall {𝕜 : Type u_3} {E : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {r : ℝ} (hr : 0 < r) : ⋂₀ (StrongDual.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)