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.

Main results #

We establish that weak_bilin B has the following structure:

We prove the following results characterizing the weak topology:

Notations #

No new notation is introduced.

References #

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 β†’β‚—[π•œ] π•œ) :
@[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
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 β†’β‚—[π•œ] π•œ) :
Equations
@[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
@[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 β†’β‚—[π•œ] π•œ) :
Equations
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 π•œ] :

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 π•œ π•œ] :

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 π•œ] :

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
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] :
@[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
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] :
@[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] :
@[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
@[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
@[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
@[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 π•œ] :

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

Equations
@[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
@[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 π•œ] :
@[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 π•œ] :

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_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] :
@[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] :
@[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] :
@[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
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
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) :
@[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) :
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))