Weak dual topology

This file defines the weak topology given two vector spaces E and F over a commutative semiring 𝕜 and a bilinear form B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜. The weak topology on E is the coarsest topology such that for all y : F every map fun x => B x y is continuous.

In the case that F = E →L[𝕜] 𝕜 and B being the canonical pairing, we obtain the weak-* topology, WeakDual 𝕜 E := (E →L[𝕜] 𝕜). Interchanging the arguments in the bilinear form yields the weak topology WeakSpace 𝕜 E := E.

Main definitions

The main definitions are the types WeakBilin B for the general case and the two special cases WeakDual 𝕜 E and WeakSpace 𝕜 E with the respective topology instances on it.

• Given B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜, the type WeakBilin B is a type synonym for E.
• The instance WeakBilin.instTopologicalSpace is the weak topology induced by the bilinear form B.
• WeakDual 𝕜 E is a type synonym for Dual 𝕜 E (when the latter is defined): both are equal to the type E →L[𝕜] 𝕜 of continuous linear maps from a module E over 𝕜 to the ring 𝕜.
• The instance WeakDual.instTopologicalSpace is the weak-* topology on WeakDual 𝕜 E, i.e., the coarsest topology making the evaluation maps at all z : E continuous.
• WeakSpace 𝕜 E is a type synonym for E (when the latter is defined).
• The instance WeakSpace.instTopologicalSpace is the weak topology on E, i.e., the coarsest topology such that all v : dual 𝕜 E remain continuous.

Main results

We establish that WeakBilin B has the following structure:

• WeakBilin.instContinuousAdd: The addition in WeakBilin B is continuous.
• WeakBilin.instContinuousSMul: The scalar multiplication in WeakBilin B is continuous.

We prove the following results characterizing the weak topology:

• eval_continuous: For any y : F, the evaluation mapping fun x => B x y is continuous.
• continuous_of_continuous_eval: For a mapping to WeakBilin B to be continuous, it suffices that its compositions with pairing with B at all points y : F is continuous.
• tendsto_iff_forall_eval_tendsto: Convergence in WeakBilin B can be characterized in terms of convergence of the evaluations at all points y : F.

Notations

No new notation is introduced.

References

• [H. H. Schaefer, Topological Vector Spaces][schaefer1966]

Tags

weak-star, weak dual, duality

def WeakBilin {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [CommSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] : (E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) → Type u_5

The space E equipped with the weak topology induced by the bilinear form B.

Equations

• WeakBilin x = E

instance WeakBilin.instAddCommMonoid {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [CommSemiring 𝕜] [a : AddCommMonoid E] [Module 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) : AddCommMonoid (WeakBilin B)

Equations

• WeakBilin.instAddCommMonoid B = a

instance WeakBilin.instModule {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [CommSemiring 𝕜] [AddCommMonoid E] [m : Module 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) : Module 𝕜 (WeakBilin B)

Equations

• WeakBilin.instModule B = m

instance WeakBilin.instAddCommGroup {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [CommSemiring 𝕜] [a : AddCommGroup E] [Module 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) : AddCommGroup (WeakBilin B)

Equations

• WeakBilin.instAddCommGroup B = a

instance WeakBilin.instModule' {𝕜 : Type u_2} {𝕝 : Type u_3} {E : Type u_5} {F : Type u_6} [CommSemiring 𝕜] [CommSemiring 𝕝] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] [m : Module 𝕝 E] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) : Module 𝕝 (WeakBilin B)

Equations

• WeakBilin.instModule' B = m

instance WeakBilin.instIsScalarTower {𝕜 : Type u_2} {𝕝 : Type u_3} {E : Type u_5} {F : Type u_6} [CommSemiring 𝕜] [CommSemiring 𝕝] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] [SMul 𝕝 𝕜] [Module 𝕝 E] [s : IsScalarTower 𝕝 𝕜 E] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) : IsScalarTower 𝕝 𝕜 (WeakBilin B)

Equations

• ⋯ = s

instance WeakBilin.instTopologicalSpace {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [TopologicalSpace 𝕜] [CommSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) : TopologicalSpace (WeakBilin B)

Equations

• WeakBilin.instTopologicalSpace B = TopologicalSpace.induced (fun (x : WeakBilin B) (y : F) => (B x) y) Pi.topologicalSpace

theorem WeakBilin.coeFn_continuous {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [TopologicalSpace 𝕜] [CommSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) : Continuous fun (x : WeakBilin B) (y : F) => (B x) y

The coercion (fun x y => B x y) : E → (F → 𝕜) is continuous.

theorem WeakBilin.eval_continuous {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [TopologicalSpace 𝕜] [CommSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) (y : F) : Continuous fun (x : WeakBilin B) => (B x) y

theorem WeakBilin.continuous_of_continuous_eval {α : Type u_1} {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [TopologicalSpace 𝕜] [CommSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) [TopologicalSpace α] {g : α → WeakBilin B} (h : ∀ (y : F), Continuous fun (a : α) => (B (g a)) y) : Continuous g

theorem WeakBilin.embedding {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [TopologicalSpace 𝕜] [CommSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] {B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜} (hB : Function.Injective ⇑B) : Embedding fun (x : WeakBilin B) (y : F) => (B x) y

The coercion (fun x y => B x y) : E → (F → 𝕜) is an embedding.

theorem WeakBilin.tendsto_iff_forall_eval_tendsto {α : Type u_1} {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [TopologicalSpace 𝕜] [CommSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) {l : Filter α} {f : α → WeakBilin B} {x : WeakBilin B} (hB : Function.Injective ⇑B) : Filter.Tendsto f l (nhds x) ↔ ∀ (y : F), Filter.Tendsto (fun (i : α) => (B (f i)) y) l (nhds ((B x) y))

instance WeakBilin.instContinuousAdd {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [TopologicalSpace 𝕜] [CommSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) [ContinuousAdd 𝕜] : ContinuousAdd (WeakBilin B)

Addition in WeakBilin B is continuous.

Equations

• ⋯ = ⋯

instance WeakBilin.instContinuousSMul {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [TopologicalSpace 𝕜] [CommSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) [ContinuousSMul 𝕜 𝕜] : ContinuousSMul 𝕜 (WeakBilin B)

Scalar multiplication by 𝕜 on WeakBilin B is continuous.

Equations

• ⋯ = ⋯

instance WeakBilin.instTopologicalAddGroup {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [TopologicalSpace 𝕜] [CommRing 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) [ContinuousAdd 𝕜] : TopologicalAddGroup (WeakBilin B)

WeakBilin B is a TopologicalAddGroup, meaning that addition and negation are continuous.

Equations

• ⋯ = ⋯

def topDualPairing (𝕜 : Type u_8) (E : Type u_9) [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousConstSMul 𝕜 𝕜] : (E →L[𝕜] 𝕜) →ₗ[𝕜] E →ₗ[𝕜] 𝕜

The canonical pairing of a vector space and its topological dual.

Equations

• topDualPairing 𝕜 E = ContinuousLinearMap.coeLM 𝕜

theorem topDualPairing_apply {𝕜 : Type u_2} {E : Type u_5} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] (v : E →L[𝕜] 𝕜) (x : E) : ((topDualPairing 𝕜 E) v) x = v x

def WeakDual (𝕜 : Type u_8) (E : Type u_9) [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] : Type (max u_8 u_9)

The weak star topology is the topology coarsest topology on E →L[𝕜] 𝕜 such that all functionals fun v => v x are continuous.

Equations

• WeakDual 𝕜 E = WeakBilin (topDualPairing 𝕜 E)

instance WeakDual.instAddCommMonoid {𝕜 : Type u_2} {E : Type u_5} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] : AddCommMonoid (WeakDual 𝕜 E)

Equations

• WeakDual.instAddCommMonoid = WeakBilin.instAddCommMonoid (topDualPairing 𝕜 E)

instance WeakDual.instModule {𝕜 : Type u_2} {E : Type u_5} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] : Module 𝕜 (WeakDual 𝕜 E)

Equations

• WeakDual.instModule = WeakBilin.instModule (topDualPairing 𝕜 E)

instance WeakDual.instTopologicalSpace {𝕜 : Type u_2} {E : Type u_5} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] : TopologicalSpace (WeakDual 𝕜 E)

Equations

• WeakDual.instTopologicalSpace = WeakBilin.instTopologicalSpace (topDualPairing 𝕜 E)

instance WeakDual.instContinuousAdd {𝕜 : Type u_2} {E : Type u_5} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] : ContinuousAdd (WeakDual 𝕜 E)

Equations

• ⋯ = ⋯

instance WeakDual.instInhabited {𝕜 : Type u_2} {E : Type u_5} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] : Inhabited (WeakDual 𝕜 E)

Equations

• WeakDual.instInhabited = ContinuousLinearMap.inhabited

instance WeakDual.instFunLike {𝕜 : Type u_2} {E : Type u_5} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] : FunLike (WeakDual 𝕜 E) E 𝕜

Equations

• WeakDual.instFunLike = ContinuousLinearMap.funLike

instance WeakDual.instContinuousLinearMapClass {𝕜 : Type u_2} {E : Type u_5} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] : ContinuousLinearMapClass (WeakDual 𝕜 E) 𝕜 E 𝕜

Equations

• ⋯ = ⋯

instance WeakDual.instCoeFunWeakDualForAll {𝕜 : Type u_2} {E : Type u_5} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] : CoeFun (WeakDual 𝕜 E) fun (x : WeakDual 𝕜 E) => E → 𝕜

Helper instance for when there's too many metavariables to apply DFunLike.hasCoeToFun directly.

Equations

• WeakDual.instCoeFunWeakDualForAll = DFunLike.hasCoeToFun

instance WeakDual.instMulAction {𝕜 : Type u_2} {E : Type u_5} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] (M : Type u_8) [Monoid M] [DistribMulAction M 𝕜] [SMulCommClass 𝕜 M 𝕜] [ContinuousConstSMul M 𝕜] : MulAction M (WeakDual 𝕜 E)

If a monoid M distributively continuously acts on 𝕜 and this action commutes with multiplication on 𝕜, then it acts on WeakDual 𝕜 E.

Equations

• WeakDual.instMulAction M = ContinuousLinearMap.mulAction

instance WeakDual.instDistribMulAction {𝕜 : Type u_2} {E : Type u_5} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] (M : Type u_8) [Monoid M] [DistribMulAction M 𝕜] [SMulCommClass 𝕜 M 𝕜] [ContinuousConstSMul M 𝕜] : DistribMulAction M (WeakDual 𝕜 E)

If a monoid M distributively continuously acts on 𝕜 and this action commutes with multiplication on 𝕜, then it acts distributively on WeakDual 𝕜 E.

Equations

• WeakDual.instDistribMulAction M = ContinuousLinearMap.distribMulAction

instance WeakDual.instModule' {𝕜 : Type u_2} {E : Type u_5} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] (R : Type u_8) [Semiring R] [Module R 𝕜] [SMulCommClass 𝕜 R 𝕜] [ContinuousConstSMul R 𝕜] : Module R (WeakDual 𝕜 E)

If 𝕜 is a topological module over a semiring R and scalar multiplication commutes with the multiplication on 𝕜, then WeakDual 𝕜 E is a module over R.

Equations

• WeakDual.instModule' R = ContinuousLinearMap.module

instance WeakDual.instContinuousConstSMul {𝕜 : Type u_2} {E : Type u_5} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] (M : Type u_8) [Monoid M] [DistribMulAction M 𝕜] [SMulCommClass 𝕜 M 𝕜] [ContinuousConstSMul M 𝕜] : ContinuousConstSMul M (WeakDual 𝕜 E)

Equations

• ⋯ = ⋯

instance WeakDual.instContinuousSMul {𝕜 : Type u_2} {E : Type u_5} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] (M : Type u_8) [Monoid M] [DistribMulAction M 𝕜] [SMulCommClass 𝕜 M 𝕜] [TopologicalSpace M] [ContinuousSMul M 𝕜] : ContinuousSMul M (WeakDual 𝕜 E)

If a monoid M distributively continuously acts on 𝕜 and this action commutes with multiplication on 𝕜, then it continuously acts on WeakDual 𝕜 E.

Equations

• ⋯ = ⋯

theorem WeakDual.coeFn_continuous {𝕜 : Type u_2} {E : Type u_5} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] : Continuous fun (x : WeakDual 𝕜 E) (y : E) => x y

theorem WeakDual.eval_continuous {𝕜 : Type u_2} {E : Type u_5} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] (y : E) : Continuous fun (x : WeakDual 𝕜 E) => x y

theorem WeakDual.continuous_of_continuous_eval {α : Type u_1} {𝕜 : Type u_2} {E : Type u_5} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] [TopologicalSpace α] {g : α → WeakDual 𝕜 E} (h : ∀ (y : E), Continuous fun (a : α) => (g a) y) : Continuous g

instance WeakDual.instT2Space {𝕜 : Type u_2} {E : Type u_5} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] [T2Space 𝕜] : T2Space (WeakDual 𝕜 E)

Equations

• ⋯ = ⋯

def WeakSpace (𝕜 : Type u_8) (E : Type u_9) [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] : Type u_9

The weak topology is the topology coarsest topology on E such that all functionals fun x => v x are continuous.

Equations

• WeakSpace 𝕜 E = WeakBilin (LinearMap.flip (topDualPairing 𝕜 E))

instance WeakSpace.instAddCommMonoid {𝕜 : Type u_2} {E : Type u_5} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] : AddCommMonoid (WeakSpace 𝕜 E)

Equations

• WeakSpace.instAddCommMonoid = WeakBilin.instAddCommMonoid (LinearMap.flip (topDualPairing 𝕜 E))

instance WeakSpace.instModule {𝕜 : Type u_2} {E : Type u_5} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] : Module 𝕜 (WeakSpace 𝕜 E)

Equations

• WeakSpace.instModule = WeakBilin.instModule (LinearMap.flip (topDualPairing 𝕜 E))

instance WeakSpace.instTopologicalSpace {𝕜 : Type u_2} {E : Type u_5} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] : TopologicalSpace (WeakSpace 𝕜 E)

Equations

• WeakSpace.instTopologicalSpace = WeakBilin.instTopologicalSpace (LinearMap.flip (topDualPairing 𝕜 E))

instance WeakSpace.instContinuousAdd {𝕜 : Type u_2} {E : Type u_5} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] : ContinuousAdd (WeakSpace 𝕜 E)

Equations

• ⋯ = ⋯

def WeakSpace.map {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] [AddCommMonoid F] [Module 𝕜 F] [TopologicalSpace F] (f : E →L[𝕜] F) : WeakSpace 𝕜 E →L[𝕜] WeakSpace 𝕜 F

A continuous linear map from E to F is still continuous when E and F are equipped with their weak topologies.

Equations

• WeakSpace.map f = { toLinearMap := ↑f, cont := ⋯ }

theorem WeakSpace.map_apply {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] [AddCommMonoid F] [Module 𝕜 F] [TopologicalSpace F] (f : E →L[𝕜] F) (x : E) : (WeakSpace.map f) x = f x

@[simp]

theorem WeakSpace.coe_map {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] [AddCommMonoid F] [Module 𝕜 F] [TopologicalSpace F] (f : E →L[𝕜] F) : ⇑(WeakSpace.map f) = ⇑f

def toWeakSpace (𝕜 : Type u_2) (E : Type u_5) [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] : E ≃ₗ[𝕜] WeakSpace 𝕜 E

There is a canonical map E → WeakSpace 𝕜 E (the "identity" mapping). It is a linear equivalence.

Equations

• toWeakSpace 𝕜 E = LinearEquiv.refl 𝕜 E

def continuousLinearMapToWeakSpace (𝕜 : Type u_2) (E : Type u_5) [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] : E →L[𝕜] WeakSpace 𝕜 E

For a topological vector space E, "identity mapping" E → WeakSpace 𝕜 E is continuous. This definition implements it as a continuous linear map.

Equations

• continuousLinearMapToWeakSpace 𝕜 E = let __spread.0 := toWeakSpace 𝕜 E; { toLinearMap := ↑__spread.0, cont := ⋯ }

@[simp]

theorem continuousLinearMapToWeakSpace_eq_toWeakSpace (𝕜 : Type u_2) (E : Type u_5) [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] (x : E) : (continuousLinearMapToWeakSpace 𝕜 E) x = (toWeakSpace 𝕜 E) x

theorem continuousLinearMapToWeakSpace_bijective {𝕜 : Type u_2} {E : Type u_5} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] : Function.Bijective ⇑(continuousLinearMapToWeakSpace 𝕜 E)

theorem isOpenMap_toWeakSpace_symm {𝕜 : Type u_2} {E : Type u_5} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] : IsOpenMap ⇑(LinearEquiv.symm (toWeakSpace 𝕜 E))

The canonical map from WeakSpace 𝕜 E to E is an open map.

theorem WeakSpace.isOpen_of_isOpen {𝕜 : Type u_2} {E : Type u_5} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] (V : Set E) (hV : IsOpen (⇑(continuousLinearMapToWeakSpace 𝕜 E) '' V)) : IsOpen V

A set in E which is open in the weak topology is open.

theorem tendsto_iff_forall_eval_tendsto_topDualPairing {α : Type u_1} {𝕜 : Type u_2} {E : Type u_5} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] {l : Filter α} {f : α → WeakDual 𝕜 E} {x : WeakDual 𝕜 E} : Filter.Tendsto f l (nhds x) ↔ ∀ (y : E), Filter.Tendsto (fun (i : α) => ((topDualPairing 𝕜 E) (f i)) y) l (nhds (((topDualPairing 𝕜 E) x) y))