Weak topologies on modules #

Given a bilinear form B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜, the weak topology on E is the coarsest topology such that for all y : F every map (B · y) is continuous; equivalently, it is the topology on E induced by the map (B · · : E → (F → 𝕜)).

This file defines a Prop-valued typeclass LinearMap.IsWeak expressing that an existing topology on E is the weak topology. Although this could be passed around explicitly as a hypothesis Topology.IsInducing (B · ·), given the ubiquity of weak topologies in functional analysis, the numerous properties that can be deduced because the inducing map B is bilinear, the fact that several theorems (e.g., one version of the bipolar theorem) require this hypothesis, and we can instantiate this class for several extant types in Mathlib, we choose to make this a typeclass instead.

Note that establishing LinearMap.IsWeak before proving theorems about a particular type can help prevent abuse of definitional equalities. This because spaces equipped with a weak topology are frequently type synonyms of some other type E'. For example, suppose E' is a type (potentially with some extant topology other than the weak topology) and B' : E' →ₗ[𝕜] F →ₗ[𝕜] 𝕜 is a bilinear form. To consider the weak topology on E' induced by B', in practice we must create a type synonym E with an instance TopologicalSpace E := .induced (B' · ·) Pi.topologicalSpace. It would then be tempting to create theorems such as:

example (y : F) : Continuous (fun x : E ↦ B' x y) := sorry

However, this statement contains an abuse of the the definitional equality E := E' since x : E, but B' has domain E'. Moreover, one might be tempted to say that B'.IsWeak, but this is impossible because the domain of B' is E', which is equipped with the incorrect topology. Instead, what one should do is to first define a new bilinear form B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜 by composing B' with the linear equivalence between E and E', and then establish B.IsWeak. If then one proves theorems about E using only the LinearMap.IsWeak API, then one can have more confidence that the statements are type correct.

Main definitions #

LinearMap.IsWeak: a typeclass expressing that the topology on E is the weak topology induced by the bilinear form B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜.
LinearMap.IsWeak.eval: the evaluation map F →ₗ[𝕜] StrongDual 𝕜 E sending y : F to the continuous linear functional (B · y).

Main results #

We prove the following results characterizing the weak topology:

LinearMap.IsWeak.continuous_eval: For any y : F, the evaluation mapping (B · y) is continuous.
LinearMap.IsWeak.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.
LinearMap.IsWeak.tendsto_iff_forall_eval_tendsto: Convergence in WeakBilin B can be characterized in terms of convergence of the evaluations at all points y : F.