Topologies on spaces of measures

We define the weak and strong topologies on D(X, E). These are deliberately not declared as instances in order to avoid favouring one topology over the other.

@[reducible]

def AbstractMeasure.WeakTopology {X : Type u_1} {R : Type u_2} {E : Type u_3} [TopologicalSpace X] [NormedAddCommGroup E] [CommRing R] [Module R E] [TopologicalSpace R] [IsTopologicalRing R] : TopologicalSpace (AbstractMeasure X R E)

The weak topology on AbstractMeasure G R E (the weakest topology such that μ ↦ μ f is continuous for all f).

Equations

• AbstractMeasure.WeakTopology = TopologicalSpace.induced (fun (μ : AbstractMeasure X R E) (f : C(X, R)) => μ f) inferInstance

@[reducible]

def AbstractMeasure.StrongTopology {X : Type u_1} {R : Type u_2} {E : Type u_3} [TopologicalSpace X] [NontriviallyNormedField R] [NormedAddCommGroup E] [NormedSpace R E] : TopologicalSpace (AbstractMeasure X R E)

The strong topology on AbstractMeasure G R E (the topology induced by the norm).

Equations

• AbstractMeasure.StrongTopology = { IsOpen := AbstractMeasure.StrongTopology._aux_1, isOpen_univ := ⋯, isOpen_inter := ⋯, isOpen_sUnion := ⋯ }