# 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.

## Main definitions #

The main definition is the type `WeakBilin B`.

- 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`.

## 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`.

## References #

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

## Tags #

weak-star, weak dual, duality

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

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

Equations

- WeakBilin x✝ = E

Instances For

source
instance instAddCommMonoidWeakBilin {𝕜 : Type u_2} {E : Type u_1} {F : Type u_3} [CommSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] (x✝ : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) :
AddCommMonoid (WeakBilin x✝)
Equations

- instAddCommMonoidWeakBilin x✝ = inst✝³

source
instance instModuleWeakBilin {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [CommSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] (x✝ : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) :
Module 𝕜 (WeakBilin x✝)
Equations

- instModuleWeakBilin x✝ = inst✝²

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

- WeakBilin.instAddCommGroup B = a

source
@[instance 100]
instance WeakBilin.instModule' {𝕜 : Type u_2} {𝕝 : Type u_3} {E : Type u_4} {F : Type u_5} [CommSemiring 𝕜] [CommSemiring 𝕝] [AddCommMonoid E] [Module 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] [m : Module 𝕝 E] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) :
Module 𝕝 (WeakBilin B)
Equations

- WeakBilin.instModule' B = m

source
instance WeakBilin.instIsScalarTower {𝕜 : Type u_2} {𝕝 : Type u_3} {E : Type u_4} {F : Type u_5} [CommSemiring 𝕜] [CommSemiring 𝕝] [AddCommMonoid E] [Module 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] [SMul 𝕝 𝕜] [Module 𝕝 E] [s : IsScalarTower 𝕝 𝕜 E] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) :
IsScalarTower 𝕝 𝕜 (WeakBilin B)
source
instance WeakBilin.instTopologicalSpace {𝕜 : Type u_2} {E : Type u_4} {F : Type u_5} [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

source
theorem WeakBilin.coeFn_continuous {𝕜 : Type u_2} {E : Type u_4} {F : Type u_5} [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.

source
theorem WeakBilin.eval_continuous {𝕜 : Type u_2} {E : Type u_4} {F : Type u_5} [TopologicalSpace 𝕜] [CommSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) (y : F) :
Continuous fun (x : WeakBilin B) => (B x) y
source
theorem WeakBilin.continuous_of_continuous_eval {α : Type u_1} {𝕜 : Type u_2} {E : Type u_4} {F : Type u_5} [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
source
theorem WeakBilin.isEmbedding {𝕜 : Type u_2} {E : Type u_4} {F : Type u_5} [TopologicalSpace 𝕜] [CommSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] {B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜} (hB : Function.Injective ⇑B) :
Topology.IsEmbedding fun (x : WeakBilin B) (y : F) => (B x) y

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

source
theorem WeakBilin.tendsto_iff_forall_eval_tendsto {α : Type u_1} {𝕜 : Type u_2} {E : Type u_4} {F : Type u_5} [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))
source
instance WeakBilin.instContinuousAdd {𝕜 : Type u_2} {E : Type u_4} {F : Type u_5} [TopologicalSpace 𝕜] [CommSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) [ContinuousAdd 𝕜] :
ContinuousAdd (WeakBilin B)

Addition in `WeakBilin B` is continuous.

source
instance WeakBilin.instContinuousSMul {𝕜 : Type u_2} {E : Type u_4} {F : Type u_5} [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.

source
def WeakBilin.eval {𝕜 : Type u_2} {E : Type u_4} {F : Type u_5} [TopologicalSpace 𝕜] [CommSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] :
F →ₗ[𝕜] StrongDual 𝕜 (WeakBilin B)

Map `F` into the topological dual of `E` with the weak topology induced by `F`

Equations

- WeakBilin.eval B = { toFun := fun (f : F) => { toLinearMap := B.flip f, cont := ⋯ }, map_add' := ⋯, map_smul' := ⋯ }

Instances For

source
instance WeakBilin.instIsTopologicalAddGroup {𝕜 : Type u_2} {E : Type u_4} {F : Type u_5} [TopologicalSpace 𝕜] [CommRing 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) [ContinuousAdd 𝕜] :
IsTopologicalAddGroup (WeakBilin B)

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