The double dual of a normed space

In this file we define the inclusion of a normed space into its double strong dual, prove that it is an isometry (for 𝕜 = ℝ or 𝕜 = ℂ), and use the corresponding weak-topology embedding together with Banach–Alaoglu to transfer compactness from the weak-star bidual back to the weak topology.

Main definitions

• NormedSpace.inclusionInDoubleDual is the inclusion of a normed space in its double StrongDual, considered as a bounded linear map.
• NormedSpace.inclusionInDoubleDualLi is the same map as a linear isometry (for 𝕜 = ℝ or 𝕜 = ℂ).
• NormedSpace.inclusionInDoubleDualWeak is the map from the weak space into the weak-star bidual, as a continuous linear map.
• NormedSpace.isEmbedding_inclusionInDoubleDualWeak shows that inclusionInDoubleDualWeak is a topological embedding.
• NormedSpace.isCompact_closure_of_isBounded transfers compactness from the weak-star topology on the bidual back to the weak topology on X.

References

• Conway, John B., A course in functional analysis

Tags

double dual, inclusion, isometry, embedding, weak-star topology

noncomputable 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‖

noncomputable def NormedSpace.inclusionInDoubleDualLi (𝕜 : Type v) [RCLike 𝕜] {E : Type u} [SeminormedAddCommGroup 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.norm_le_dual_bound (𝕜 : Type v) [RCLike 𝕜] {E : Type u} [SeminormedAddCommGroup 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.

noncomputable def NormedSpace.inclusionInDoubleDualWeak (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (X : Type u_2) [SeminormedAddCommGroup X] [NormedSpace 𝕜 X] : WeakSpace 𝕜 X →L[𝕜] WeakDual 𝕜 (StrongDual 𝕜 X)

The map from a normed space with the weak topology into the weak-star bidual, as a continuous linear map. Built using LinearEquiv.arrowCongr to properly bundle the topology changes via toWeakSpace and StrongDual.toWeakDual.

Equations

• NormedSpace.inclusionInDoubleDualWeak 𝕜 X = { toLinearMap := ((toWeakSpace 𝕜 X).arrowCongr StrongDual.toWeakDual) ↑(NormedSpace.inclusionInDoubleDual 𝕜 X), cont := ⋯ }

@[simp]

theorem NormedSpace.inclusionInDoubleDualWeak_apply_apply (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (X : Type u_2) [SeminormedAddCommGroup X] [NormedSpace 𝕜 X] (a✝ : WeakSpace 𝕜 X) (x : X →L[𝕜] 𝕜) : ((inclusionInDoubleDualWeak 𝕜 X) a✝) x = x ((toWeakSpace 𝕜 X).symm a✝)

theorem NormedSpace.inclusionInDoubleDualWeak_apply (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (X : Type u_2) [SeminormedAddCommGroup X] [NormedSpace 𝕜 X] (a✝ : WeakSpace 𝕜 X) : (inclusionInDoubleDualWeak 𝕜 X) a✝ = StrongDual.toWeakDual ((inclusionInDoubleDual 𝕜 X) ((toWeakSpace 𝕜 X).symm a✝))

@[simp]

theorem NormedSpace.toLinearMap_inclusionInDoubleDualWeak (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (X : Type u_2) [SeminormedAddCommGroup X] [NormedSpace 𝕜 X] : ↑(inclusionInDoubleDualWeak 𝕜 X) = ((toWeakSpace 𝕜 X).arrowCongr StrongDual.toWeakDual) ↑(inclusionInDoubleDual 𝕜 X)

theorem NormedSpace.isEmbedding_inclusionInDoubleDualWeak (𝕜 : Type u_3) [RCLike 𝕜] (X : Type u_4) [NormedAddCommGroup X] [NormedSpace 𝕜 X] : Topology.IsEmbedding ⇑(inclusionInDoubleDualWeak 𝕜 X)

inclusionInDoubleDualWeak is a topological embedding from the weak topology to the weak-star topology.

theorem NormedSpace.isCompact_closure_of_isBounded (𝕜 : Type u_3) [RCLike 𝕜] (X : Type u_4) [NormedAddCommGroup X] [NormedSpace 𝕜 X] (S : Set (WeakSpace 𝕜 X)) (hb : Bornology.IsBounded (⇑(toWeakSpace 𝕜 X) ⁻¹' S)) (hrange : closure (⇑(inclusionInDoubleDualWeak 𝕜 X) '' S) ⊆ Set.range ⇑(inclusionInDoubleDualWeak 𝕜 X)) : IsCompact (closure S)

If S is bounded set in WeakSpace X and the weak-star closure of its image under the embedding into the weak-star double dual lies in the range of that embedding, then closure S is compact in the weak topology.

This combines Banach–Alaoglu (compactness of bounded weak-star–closed sets) with the topological embedding inclusionInDoubleDualWeak_isEmbedding to transfer compactness back to the weak topology on X.