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
Instances For
@[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 := ⋯ }