Weak-star continuous functionals on a weak dual

Every weak-star continuous linear functional on WeakDual 𝕜 F is evaluation at a point of F. This is Mathlib's weak representation theorem LinearMap.dualEmbedding_surjective for the canonical pairing topDualPairing 𝕜 F, stated directly for the WeakDual type synonym, so that it applies to WeakDual 𝕜 F whatever instance path elaborated it. Hahn–Banach separation in a weak dual produces such functionals, and this lemma turns them into points of the predual.

Over 𝕜 = ℝ or ℂ, the dual WeakDual 𝕜 F is also a real vector space. A real multiple c • f is the multiple of f by the scalar (c : 𝕜), and acts pointwise as multiplication by (c : 𝕜). The instances WeakDual.instIsScalarTowerReal and WeakDual.instLocallyConvexSpaceReal record that this real structure is compatible with the 𝕜-structure and that the weak-star topology is real locally convex, as needed for real Hahn–Banach separation and the Krein–Milman theorem.

theorem WeakDual.exists_forall_apply_eq_apply {𝕜 : Type u_1} {F : Type u_2} [NontriviallyNormedField 𝕜] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] (l : StrongDual 𝕜 (WeakDual 𝕜 F)) : ∃ (x : F), ∀ (φ : WeakDual 𝕜 F), l φ = φ x

Every weak-star continuous linear functional on WeakDual 𝕜 F is evaluation at a point of F.

theorem WeakDual.real_smul_apply {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [AddCommMonoid F] [Module 𝕜 F] [TopologicalSpace F] (c : ℝ) (f : WeakDual 𝕜 F) (x : F) : (c • f) x = ↑c * f x

A real multiple of a functional in WeakDual 𝕜 F acts as multiplication by the corresponding scalar of 𝕜.

theorem WeakDual.real_smul_eq_coe_smul {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [AddCommMonoid F] [Module 𝕜 F] [TopologicalSpace F] (c : ℝ) (f : WeakDual 𝕜 F) : c • f = ↑c • f

A real multiple of a functional in WeakDual 𝕜 F is its multiple by the corresponding scalar of 𝕜.

instance WeakDual.instIsScalarTowerReal {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [AddCommMonoid F] [Module 𝕜 F] [TopologicalSpace F] : IsScalarTower ℝ 𝕜 (WeakDual 𝕜 F)

The real action on WeakDual 𝕜 F is compatible with the 𝕜-action.

instance WeakDual.instLocallyConvexSpaceReal {𝕜 : Type u_1} [RCLike 𝕜] {F : Type u_3} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] : LocallyConvexSpace ℝ (WeakDual 𝕜 F)

The weak-star topology on WeakDual 𝕜 F is real locally convex: it is defined by the seminorms of the canonical dual pairing.