mathlib documentation

topology.algebra.weak_dual_topology

Weak dual topology #

This file defines the weak-* topology on duals of suitable topological modules E over suitable topological semirings π•œ. The (weak) dual consists of continuous linear functionals E β†’L[π•œ] π•œ from E to scalars π•œ. The weak-* topology is the coarsest topology on this dual weak_dual π•œ E := (E β†’L[π•œ] π•œ) w.r.t. which the evaluation maps at all z : E are continuous.

The weak dual is a module over π•œ if the semiring π•œ is commutative.

Main definitions #

The main definitions are the type weak_dual π•œ E and a topology instance on it.

Main results #

We establish that weak_dual π•œ E has the following structure:

We prove the following results characterizing the weak-* topology:

Notations #

No new notation is introduced.

Implementation notes #

The weak-* topology is defined as the induced topology under the mapping that associates to a dual element x' the functional E β†’ π•œ, when the space E β†’ π•œ of functionals is equipped with the topology of pointwise convergence (product topology).

Typically one might assume that π•œ is a topological semiring in the sense of the typeclasses topological_space π•œ, semiring π•œ, has_continuous_add π•œ, has_continuous_mul π•œ, and that the space E is a topological module over π•œ in the sense of the typeclasses topological_space E, add_comm_monoid E, has_continuous_add E, module π•œ E, has_continuous_smul π•œ E. The definitions and results are, however, given with weaker assumptions when possible.

References #

Tags #

weak-star, weak dual

Weak star topology on duals of topological modules #

@[instance]
def weak_dual.has_coe_to_fun (π•œ : Type u_1) [topological_space π•œ] [semiring π•œ] (E : Type u_2) [topological_space E] [add_comm_monoid E] [module π•œ E] :
has_coe_to_fun (weak_dual π•œ E) (Ξ» (_x : weak_dual π•œ E), E β†’ π•œ)
def weak_dual (π•œ : Type u_1) [topological_space π•œ] [semiring π•œ] (E : Type u_2) [topological_space E] [add_comm_monoid E] [module π•œ E] :
Type (max u_2 u_1)

The weak dual of a topological module E over a topological semiring π•œ consists of continuous linear functionals from E to scalars π•œ. It is a type synonym with the usual dual (when the latter is defined), but will be equipped with a different topology.

Equations
@[instance]
def weak_dual.inhabited (π•œ : Type u_1) [topological_space π•œ] [semiring π•œ] (E : Type u_2) [topological_space E] [add_comm_monoid E] [module π•œ E] :
inhabited (weak_dual π•œ E)
@[instance]
def weak_dual.add_comm_monoid (π•œ : Type u_1) [topological_space π•œ] [semiring π•œ] (E : Type u_2) [topological_space E] [add_comm_monoid E] [module π•œ E] [has_continuous_add π•œ] :
Equations
@[instance]
def weak_dual.topological_space (π•œ : Type u_1) [topological_space π•œ] [semiring π•œ] (E : Type u_2) [topological_space E] [add_comm_monoid E] [module π•œ E] :

The weak-* topology instance weak_dual.topological_space on the dual of a topological module E over a topological semiring π•œ is defined as the induced topology under the mapping that associates to a dual element x' : weak_dual π•œ E the functional E β†’ π•œ, when the space E β†’ π•œ of functionals is equipped with the topology of pointwise convergence (product topology).

Equations
theorem weak_dual.coe_fn_continuous (π•œ : Type u_1) [topological_space π•œ] [semiring π•œ] (E : Type u_2) [topological_space E] [add_comm_monoid E] [module π•œ E] :
continuous (Ξ» (x' : weak_dual π•œ E) (z : E), ⇑x' z)
theorem weak_dual.eval_continuous (π•œ : Type u_1) [topological_space π•œ] [semiring π•œ] (E : Type u_2) [topological_space E] [add_comm_monoid E] [module π•œ E] (z : E) :
continuous (Ξ» (x' : weak_dual π•œ E), ⇑x' z)
theorem weak_dual.continuous_of_continuous_eval (π•œ : Type u_1) [topological_space π•œ] [semiring π•œ] (E : Type u_2) [topological_space E] [add_comm_monoid E] [module π•œ E] {Ξ± : Type u} [topological_space Ξ±] {g : Ξ± β†’ weak_dual π•œ E} (h : βˆ€ (z : E), continuous (Ξ» (a : Ξ±), ⇑(g a) z)) :
theorem weak_dual.tendsto_iff_forall_eval_tendsto (π•œ : Type u_1) [topological_space π•œ] [semiring π•œ] (E : Type u_2) [topological_space E] [add_comm_monoid E] [module π•œ E] {Ξ³ : Type u} {F : filter Ξ³} {ψs : Ξ³ β†’ weak_dual π•œ E} {ψ : weak_dual π•œ E} :
filter.tendsto ψs F (𝓝 ψ) ↔ βˆ€ (z : E), filter.tendsto (Ξ» (i : Ξ³), ⇑(ψs i) z) F (𝓝 (β‡‘Οˆ z))
@[instance]
def weak_dual.has_continuous_add (π•œ : Type u_1) [topological_space π•œ] [semiring π•œ] (E : Type u_2) [topological_space E] [add_comm_monoid E] [module π•œ E] [has_continuous_add π•œ] :

Addition in weak_dual π•œ E is continuous.

@[instance]
def weak_dual.module (π•œ : Type u) [topological_space π•œ] [comm_semiring π•œ] [has_continuous_add π•œ] [has_continuous_mul π•œ] (E : Type u_1) [topological_space E] [add_comm_group E] [module π•œ E] :
module π•œ (weak_dual π•œ E)

If the scalars π•œ are a commutative semiring, then weak_dual π•œ E is a module over π•œ.

Equations
@[instance]
def weak_dual.has_continuous_smul (π•œ : Type u) [topological_space π•œ] [comm_semiring π•œ] [has_continuous_add π•œ] [has_continuous_mul π•œ] (E : Type u_1) [topological_space E] [add_comm_group E] [module π•œ E] :
has_continuous_smul π•œ (weak_dual π•œ E)

Scalar multiplication in weak_dual π•œ E is continuous (when π•œ is a commutative semiring).