Commit 2026-03-27 16:33 173d8345

feat(Analysis/Normed): weak-topology embedding into weak-star bidual and compactenss transfer theorem (#35559) This PR refactors the double dual material and adds new results connecting the weak topology on a normed space to the weak-star topology on its bidual.

Changes

New file: Analysis.Normed.Module.DoubleDual

Extracts the canonical embedding inclusionInDoubleDual and the bidual isometry inclusionInDoubleDualLi from Analysis.Normed.Module.Dual into a dedicated file, and adds:

• inclusionInDoubleDualWeak: the canonical map from WeakSpace 𝕜 X into WeakDual 𝕜 (StrongDual 𝕜 X).
• inclusionInDoubleDualWeak_isEmbedding: this map is a topological embedding.
• inclusionInDoubleDualWeak_homeomorph: the map as a homeomorphism onto its range.
• isCompact_closure_of_isBounded: bounded sets whose bidual image has weak-star closure in range have weakly compact closure, via Banach–Alaoglu.

Modified: Analysis.Normed.Module.Dual

The double dual inclusion material is moved out; polar set results remain. References to inclusionInDoubleDual in polar_closure are replaced by ContinuousLinearMap.apply to avoid a dependency on the new file.