mathlib documentation

topology.algebra.module.weak_dual

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 λ x, B x y is continuous.

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

Main definitions #

The main definitions are the types weak_bilin B for the general case and the two special cases weak_dual 𝕜 E and weak_space 𝕜 E with the respective topology instances on it.

Given B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜, the type weak_bilin B is a type synonym for E.
The instance weak_bilin.topological_space is the weak topology induced by the bilinear form B.
weak_dual 𝕜 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 weak_dual.topological_space is the weak-* topology on weak_dual 𝕜 E, i.e., the coarsest topology making the evaluation maps at all z : E continuous.
weak_space 𝕜 E is a type synonym for E (when the latter is defined).
The instance weak_dual.topological_space is the weak topology on E, i.e., the coarsest topology such that all v : dual 𝕜 E remain continuous.

Main results #

We establish that weak_bilin B has the following structure:

weak_bilin.has_continuous_add: The addition in weak_bilin B is continuous.
weak_bilin.has_continuous_smul: The scalar multiplication in weak_bilin B is continuous.

We prove the following results characterizing the weak topology:

eval_continuous: For any y : F, the evaluation mapping λ x, B x y is continuous.
continuous_of_continuous_eval: For a mapping to weak_bilin 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 weak_bilin 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

Tags #

weak-star, weak dual, duality

@[protected, instance]

def weak_bilin.add_comm_monoid {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [comm_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] [add_comm_monoid F] [module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) :

add_comm_monoid (weak_bilin B)

@[protected, instance]

def weak_bilin.module {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [comm_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] [add_comm_monoid F] [module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) :

module 𝕜 (weak_bilin B)

@[nolint]

def weak_bilin {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [comm_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] [add_comm_monoid F] [module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) :

Type u_5

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

Equations

weak_bilin B = E

Instances for weak_bilin

@[protected, instance]

def weak_bilin.add_comm_group {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [comm_semiring 𝕜] [a : add_comm_group E] [module 𝕜 E] [add_comm_monoid F] [module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) :

add_comm_group (weak_bilin B)

Equations

weak_bilin.add_comm_group B = a

@[protected, instance]

def weak_bilin.module' {𝕜 : Type u_2} {𝕝 : Type u_3} {E : Type u_5} {F : Type u_6} [comm_semiring 𝕜] [comm_semiring 𝕝] [add_comm_group E] [module 𝕜 E] [add_comm_group F] [module 𝕜 F] [m : module 𝕝 E] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) :

module 𝕝 (weak_bilin B)

Equations

weak_bilin.module' B = m

@[protected, instance]

def weak_bilin.is_scalar_tower {𝕜 : Type u_2} {𝕝 : Type u_3} {E : Type u_5} {F : Type u_6} [comm_semiring 𝕜] [comm_semiring 𝕝] [add_comm_group E] [module 𝕜 E] [add_comm_group F] [module 𝕜 F] [has_smul 𝕝 𝕜] [module 𝕝 E] [s : is_scalar_tower 𝕝 𝕜 E] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) :

is_scalar_tower 𝕝 𝕜 (weak_bilin B)

@[protected, instance]

def weak_bilin.topological_space {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [topological_space 𝕜] [comm_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] [add_comm_monoid F] [module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) :

topological_space (weak_bilin B)

Equations

weak_bilin.topological_space B = topological_space.induced (λ (x : weak_bilin B) (y : F), ⇑(⇑B x) y) Pi.topological_space

theorem weak_bilin.coe_fn_continuous {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [topological_space 𝕜] [comm_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] [add_comm_monoid F] [module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) :

continuous (λ (x : weak_bilin B) (y : F), ⇑(⇑B x) y)

The coercion (λ x y, B x y) : E → (F → 𝕜) is continuous.

theorem weak_bilin.eval_continuous {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [topological_space 𝕜] [comm_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] [add_comm_monoid F] [module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) (y : F) :

continuous (λ (x : weak_bilin B), ⇑(⇑B x) y)

theorem weak_bilin.continuous_of_continuous_eval {α : Type u_1} {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [topological_space 𝕜] [comm_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] [add_comm_monoid F] [module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) [topological_space α] {g : α → weak_bilin B} (h : ∀ (y : F), continuous (λ (a : α), ⇑(⇑B (g a)) y)) :

theorem weak_bilin.embedding {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [topological_space 𝕜] [comm_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] [add_comm_monoid F] [module 𝕜 F] {B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜} (hB : function.injective ⇑B) :

embedding (λ (x : weak_bilin B) (y : F), ⇑(⇑B x) y)

The coercion (λ x y, B x y) : E → (F → 𝕜) is an embedding.

theorem weak_bilin.tendsto_iff_forall_eval_tendsto {α : Type u_1} {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [topological_space 𝕜] [comm_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] [add_comm_monoid F] [module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) {l : filter α} {f : α → weak_bilin B} {x : weak_bilin B} (hB : function.injective ⇑B) :

filter.tendsto f l (nhds x) ↔ ∀ (y : F), filter.tendsto (λ (i : α), ⇑(⇑B (f i)) y) l (nhds (⇑(⇑B x) y))

@[protected, instance]

def weak_bilin.has_continuous_add {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [topological_space 𝕜] [comm_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] [add_comm_monoid F] [module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) [has_continuous_add 𝕜] :

has_continuous_add (weak_bilin B)

Addition in weak_space B is continuous.

@[protected, instance]

def weak_bilin.has_continuous_smul {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [topological_space 𝕜] [comm_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] [add_comm_monoid F] [module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) [has_continuous_smul 𝕜 𝕜] :

has_continuous_smul 𝕜 (weak_bilin B)

Scalar multiplication by 𝕜 on weak_bilin B is continuous.

@[protected, instance]

def weak_bilin.topological_add_group {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [topological_space 𝕜] [comm_ring 𝕜] [add_comm_group E] [module 𝕜 E] [add_comm_group F] [module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) [has_continuous_add 𝕜] :

topological_add_group (weak_bilin B)

weak_space B is a topological_add_group, meaning that addition and negation are continuous.

def top_dual_pairing (𝕜 : Type u_1) (E : Type u_2) [comm_semiring 𝕜] [topological_space 𝕜] [has_continuous_add 𝕜] [add_comm_monoid E] [module 𝕜 E] [topological_space E] [has_continuous_const_smul 𝕜 𝕜] :

(E →L[𝕜] 𝕜) →ₗ[𝕜] E →ₗ[𝕜] 𝕜

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

Equations

top_dual_pairing 𝕜 E = continuous_linear_map.coe_lm 𝕜

theorem dual_pairing_apply {𝕜 : Type u_2} {E : Type u_5} [comm_semiring 𝕜] [topological_space 𝕜] [has_continuous_add 𝕜] [has_continuous_const_smul 𝕜 𝕜] [add_comm_monoid E] [module 𝕜 E] [topological_space E] (v : E →L[𝕜] 𝕜) (x : E) :

⇑(⇑(top_dual_pairing 𝕜 E) v) x = ⇑v x

@[protected, instance]

def weak_dual.add_comm_monoid (𝕜 : Type u_1) (E : Type u_2) [comm_semiring 𝕜] [topological_space 𝕜] [has_continuous_add 𝕜] [has_continuous_const_smul 𝕜 𝕜] [add_comm_monoid E] [module 𝕜 E] [topological_space E] :

add_comm_monoid (weak_dual 𝕜 E)

@[protected, instance]

def weak_dual.module (𝕜 : Type u_1) (E : Type u_2) [comm_semiring 𝕜] [topological_space 𝕜] [has_continuous_add 𝕜] [has_continuous_const_smul 𝕜 𝕜] [add_comm_monoid E] [module 𝕜 E] [topological_space E] :

module 𝕜 (weak_dual 𝕜 E)

def weak_dual (𝕜 : Type u_1) (E : Type u_2) [comm_semiring 𝕜] [topological_space 𝕜] [has_continuous_add 𝕜] [has_continuous_const_smul 𝕜 𝕜] [add_comm_monoid E] [module 𝕜 E] [topological_space E] :

Type (max u_2 u_1)

The weak star topology is the topology coarsest topology on E →L[𝕜] 𝕜 such that all functionals λ v, top_dual_pairing 𝕜 E v x are continuous.

Equations

weak_dual 𝕜 E = weak_bilin (top_dual_pairing 𝕜 E)

Instances for weak_dual

@[protected, instance]

def weak_dual.has_continuous_add (𝕜 : Type u_1) (E : Type u_2) [comm_semiring 𝕜] [topological_space 𝕜] [has_continuous_add 𝕜] [has_continuous_const_smul 𝕜 𝕜] [add_comm_monoid E] [module 𝕜 E] [topological_space E] :

has_continuous_add (weak_dual 𝕜 E)

@[protected, instance]

def weak_dual.topological_space (𝕜 : Type u_1) (E : Type u_2) [comm_semiring 𝕜] [topological_space 𝕜] [has_continuous_add 𝕜] [has_continuous_const_smul 𝕜 𝕜] [add_comm_monoid E] [module 𝕜 E] [topological_space E] :

topological_space (weak_dual 𝕜 E)

@[protected, instance]

def weak_dual.inhabited {𝕜 : Type u_2} {E : Type u_5} [comm_semiring 𝕜] [topological_space 𝕜] [has_continuous_add 𝕜] [has_continuous_const_smul 𝕜 𝕜] [add_comm_monoid E] [module 𝕜 E] [topological_space E] :

inhabited (weak_dual 𝕜 E)

Equations

weak_dual.inhabited = continuous_linear_map.inhabited

@[protected, instance]

def weak_dual.weak_dual.continuous_linear_map_class {𝕜 : Type u_2} {E : Type u_5} [comm_semiring 𝕜] [topological_space 𝕜] [has_continuous_add 𝕜] [has_continuous_const_smul 𝕜 𝕜] [add_comm_monoid E] [module 𝕜 E] [topological_space E] :

continuous_linear_map_class (weak_dual 𝕜 E) 𝕜 E 𝕜

Equations

weak_dual.weak_dual.continuous_linear_map_class = continuous_linear_map.continuous_semilinear_map_class

@[protected, instance]

def weak_dual.has_coe_to_fun {𝕜 : Type u_2} {E : Type u_5} [comm_semiring 𝕜] [topological_space 𝕜] [has_continuous_add 𝕜] [has_continuous_const_smul 𝕜 𝕜] [add_comm_monoid E] [module 𝕜 E] [topological_space E] :

has_coe_to_fun (weak_dual 𝕜 E) (λ (_x : weak_dual 𝕜 E), E → 𝕜)

Helper instance for when there's too many metavariables to apply fun_like.has_coe_to_fun directly.

Equations

weak_dual.has_coe_to_fun = fun_like.has_coe_to_fun

@[protected, instance]

def weak_dual.mul_action {𝕜 : Type u_2} {E : Type u_5} [comm_semiring 𝕜] [topological_space 𝕜] [has_continuous_add 𝕜] [has_continuous_const_smul 𝕜 𝕜] [add_comm_monoid E] [module 𝕜 E] [topological_space E] (M : Type u_1) [monoid M] [distrib_mul_action M 𝕜] [smul_comm_class 𝕜 M 𝕜] [has_continuous_const_smul M 𝕜] :

mul_action M (weak_dual 𝕜 E)

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

Equations

weak_dual.mul_action M = continuous_linear_map.mul_action

@[protected, instance]

def weak_dual.distrib_mul_action {𝕜 : Type u_2} {E : Type u_5} [comm_semiring 𝕜] [topological_space 𝕜] [has_continuous_add 𝕜] [has_continuous_const_smul 𝕜 𝕜] [add_comm_monoid E] [module 𝕜 E] [topological_space E] (M : Type u_1) [monoid M] [distrib_mul_action M 𝕜] [smul_comm_class 𝕜 M 𝕜] [has_continuous_const_smul M 𝕜] :

distrib_mul_action M (weak_dual 𝕜 E)

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

Equations

weak_dual.distrib_mul_action M = continuous_linear_map.distrib_mul_action

@[protected, instance]

def weak_dual.module' {𝕜 : Type u_2} {E : Type u_5} [comm_semiring 𝕜] [topological_space 𝕜] [has_continuous_add 𝕜] [has_continuous_const_smul 𝕜 𝕜] [add_comm_monoid E] [module 𝕜 E] [topological_space E] (R : Type u_1) [semiring R] [module R 𝕜] [smul_comm_class 𝕜 R 𝕜] [has_continuous_const_smul R 𝕜] :

module R (weak_dual 𝕜 E)

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

Equations

weak_dual.module' R = continuous_linear_map.module

@[protected, instance]

def weak_dual.has_continuous_const_smul {𝕜 : Type u_2} {E : Type u_5} [comm_semiring 𝕜] [topological_space 𝕜] [has_continuous_add 𝕜] [has_continuous_const_smul 𝕜 𝕜] [add_comm_monoid E] [module 𝕜 E] [topological_space E] (M : Type u_1) [monoid M] [distrib_mul_action M 𝕜] [smul_comm_class 𝕜 M 𝕜] [has_continuous_const_smul M 𝕜] :

has_continuous_const_smul M (weak_dual 𝕜 E)

@[protected, instance]

def weak_dual.has_continuous_smul {𝕜 : Type u_2} {E : Type u_5} [comm_semiring 𝕜] [topological_space 𝕜] [has_continuous_add 𝕜] [has_continuous_const_smul 𝕜 𝕜] [add_comm_monoid E] [module 𝕜 E] [topological_space E] (M : Type u_1) [monoid M] [distrib_mul_action M 𝕜] [smul_comm_class 𝕜 M 𝕜] [topological_space M] [has_continuous_smul M 𝕜] :

has_continuous_smul M (weak_dual 𝕜 E)

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

theorem weak_dual.coe_fn_continuous {𝕜 : Type u_2} {E : Type u_5} [comm_semiring 𝕜] [topological_space 𝕜] [has_continuous_add 𝕜] [has_continuous_const_smul 𝕜 𝕜] [add_comm_monoid E] [module 𝕜 E] [topological_space E] :

continuous (λ (x : weak_dual 𝕜 E) (y : E), ⇑x y)

theorem weak_dual.eval_continuous {𝕜 : Type u_2} {E : Type u_5} [comm_semiring 𝕜] [topological_space 𝕜] [has_continuous_add 𝕜] [has_continuous_const_smul 𝕜 𝕜] [add_comm_monoid E] [module 𝕜 E] [topological_space E] (y : E) :

continuous (λ (x : weak_dual 𝕜 E), ⇑x y)

theorem weak_dual.continuous_of_continuous_eval {α : Type u_1} {𝕜 : Type u_2} {E : Type u_5} [comm_semiring 𝕜] [topological_space 𝕜] [has_continuous_add 𝕜] [has_continuous_const_smul 𝕜 𝕜] [add_comm_monoid E] [module 𝕜 E] [topological_space E] [topological_space α] {g : α → weak_dual 𝕜 E} (h : ∀ (y : E), continuous (λ (a : α), ⇑(g a) y)) :

@[protected, instance]

def weak_dual.t2_space {𝕜 : Type u_2} {E : Type u_5} [comm_semiring 𝕜] [topological_space 𝕜] [has_continuous_add 𝕜] [has_continuous_const_smul 𝕜 𝕜] [add_comm_monoid E] [module 𝕜 E] [topological_space E] [t2_space 𝕜] :

t2_space (weak_dual 𝕜 E)

@[protected, instance]

def weak_space.has_continuous_add (𝕜 : Type u_1) (E : Type u_2) [comm_semiring 𝕜] [topological_space 𝕜] [has_continuous_add 𝕜] [has_continuous_const_smul 𝕜 𝕜] [add_comm_monoid E] [module 𝕜 E] [topological_space E] :

has_continuous_add (weak_space 𝕜 E)

@[protected, instance]

def weak_space.module (𝕜 : Type u_1) (E : Type u_2) [comm_semiring 𝕜] [topological_space 𝕜] [has_continuous_add 𝕜] [has_continuous_const_smul 𝕜 𝕜] [add_comm_monoid E] [module 𝕜 E] [topological_space E] :

module 𝕜 (weak_space 𝕜 E)

@[protected, instance]

def weak_space.add_comm_monoid (𝕜 : Type u_1) (E : Type u_2) [comm_semiring 𝕜] [topological_space 𝕜] [has_continuous_add 𝕜] [has_continuous_const_smul 𝕜 𝕜] [add_comm_monoid E] [module 𝕜 E] [topological_space E] :

add_comm_monoid (weak_space 𝕜 E)

@[protected, instance]

def weak_space.topological_space (𝕜 : Type u_1) (E : Type u_2) [comm_semiring 𝕜] [topological_space 𝕜] [has_continuous_add 𝕜] [has_continuous_const_smul 𝕜 𝕜] [add_comm_monoid E] [module 𝕜 E] [topological_space E] :

topological_space (weak_space 𝕜 E)

@[nolint]

def weak_space (𝕜 : Type u_1) (E : Type u_2) [comm_semiring 𝕜] [topological_space 𝕜] [has_continuous_add 𝕜] [has_continuous_const_smul 𝕜 𝕜] [add_comm_monoid E] [module 𝕜 E] [topological_space E] :

Type u_2

The weak topology is the topology coarsest topology on E such that all functionals λ x, top_dual_pairing 𝕜 E v x are continuous.

Equations

weak_space 𝕜 E = weak_bilin (top_dual_pairing 𝕜 E).flip

Instances for weak_space

def weak_space.map {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [comm_semiring 𝕜] [topological_space 𝕜] [has_continuous_add 𝕜] [has_continuous_const_smul 𝕜 𝕜] [add_comm_monoid E] [module 𝕜 E] [topological_space E] [add_comm_monoid F] [module 𝕜 F] [topological_space F] (f : E →L[𝕜] F) :

weak_space 𝕜 E →L[𝕜] weak_space 𝕜 F

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

Equations

weak_space.map f = {to_linear_map := f.to_linear_map, cont := _}

theorem weak_space.map_apply {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [comm_semiring 𝕜] [topological_space 𝕜] [has_continuous_add 𝕜] [has_continuous_const_smul 𝕜 𝕜] [add_comm_monoid E] [module 𝕜 E] [topological_space E] [add_comm_monoid F] [module 𝕜 F] [topological_space F] (f : E →L[𝕜] F) (x : E) :

⇑(weak_space.map f) x = ⇑f x

@[simp]

theorem weak_space.coe_map {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [comm_semiring 𝕜] [topological_space 𝕜] [has_continuous_add 𝕜] [has_continuous_const_smul 𝕜 𝕜] [add_comm_monoid E] [module 𝕜 E] [topological_space E] [add_comm_monoid F] [module 𝕜 F] [topological_space F] (f : E →L[𝕜] F) :

⇑(weak_space.map f) = ⇑f

theorem tendsto_iff_forall_eval_tendsto_top_dual_pairing {α : Type u_1} {𝕜 : Type u_2} {E : Type u_5} [comm_semiring 𝕜] [topological_space 𝕜] [has_continuous_add 𝕜] [has_continuous_const_smul 𝕜 𝕜] [add_comm_monoid E] [module 𝕜 E] [topological_space E] {l : filter α} {f : α → weak_dual 𝕜 E} {x : weak_dual 𝕜 E} :

filter.tendsto f l (nhds x) ↔ ∀ (y : E), filter.tendsto (λ (i : α), ⇑(⇑(top_dual_pairing 𝕜 E) (f i)) y) l (nhds (⇑(⇑(top_dual_pairing 𝕜 E) x) y))