# 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

source
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 𝕜 𝕜

Instances For

source
@[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
source
theorem NormedSpace.inclusionInDoubleDual_norm_eq (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (E : Type u_2) [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] :
‖inclusionInDoubleDual 𝕜 E‖ = ‖ContinuousLinearMap.id 𝕜 (StrongDual 𝕜 E)‖
source
theorem NormedSpace.inclusionInDoubleDual_norm_le (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (E : Type u_2) [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] :
‖inclusionInDoubleDual 𝕜 E‖ ≤ 1
source
theorem NormedSpace.double_dual_bound (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (E : Type u_2) [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] (x : E) :
‖(inclusionInDoubleDual 𝕜 E) x‖ ≤ ‖x‖
source
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`.

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

source
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' := ⋯ }

Instances For

source
theorem NormedSpace.isClosed_polar (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] (s : Set E) :
IsClosed (StrongDual.polar 𝕜 s)
source
@[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
source
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`.

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

source
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⁻¹
source
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.

source
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
source
theorem LinearMap.polar_AbsConvex {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommMonoid E] [AddCommMonoid F] [Module 𝕜 E] [Module 𝕜 F] {B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜} (s : Set E) :
AbsConvex 𝕜 (B.polar s)