Dirac measures and the norm topology

Dirac measures vary continuously in the weak topology. For a compact totally separated domain and ultrametric field coefficients, distinct Dirac measures are at operator-norm distance one. Over any nontrivially normed field, their distance is at least one, so on an infinite such domain the closed unit ball of the continuous dual is not norm compact. This distinguishes the strong topology on bounded measures from the weak topology used for integral measures.

All norms below are taken on the continuous dual through AbstractMeasure.toCLMEquiv; no norm or topology is installed on the abstract measure carrier.

References

J. Rodrigues Jacinto and C. Williams, An introduction to p-adic L-functions, Definitions 3.5 and 3.8, Example 3.10, and Remark 3.28(3). The measure carrier, Dirac measures, and the two topologies are Mathlib's.

theorem TauCeti.AbstractMeasure.continuous_dirac_weak {X : Type u_1} {R : Type u_2} [TopologicalSpace X] [NormedCommRing R] : Continuous (AbstractMeasure.dirac R)

The Dirac map is continuous for the weak topology of test-function evaluations.

@[simp]

theorem TauCeti.AbstractMeasure.norm_dirac {X : Type u_1} {K : Type u_3} [TopologicalSpace X] [CompactSpace X] [NontriviallyNormedField K] (x : X) : ‖AbstractMeasure.toCLMEquiv (AbstractMeasure.dirac K x)‖ = 1

A Dirac measure has operator norm one.

theorem TauCeti.AbstractMeasure.one_le_norm_dirac_sub {X : Type u_1} {K : Type u_3} [TopologicalSpace X] [CompactSpace X] [NontriviallyNormedField K] [TotallySeparatedSpace X] {x y : X} (hxy : x ≠ y) : 1 ≤ ‖AbstractMeasure.toCLMEquiv (AbstractMeasure.dirac K x - AbstractMeasure.dirac K y)‖

On a totally separated compact space, distinct Dirac measures are at operator-norm distance at least one.

theorem TauCeti.AbstractMeasure.norm_dirac_sub {X : Type u_1} {K : Type u_3} [TopologicalSpace X] [CompactSpace X] [NontriviallyNormedField K] [TotallySeparatedSpace X] [IsUltrametricDist K] {x y : X} (hxy : x ≠ y) : ‖AbstractMeasure.toCLMEquiv (AbstractMeasure.dirac K x - AbstractMeasure.dirac K y)‖ = 1

On a totally separated compact space, distinct Dirac measures are at operator-norm distance one over an ultrametric field.

theorem TauCeti.AbstractMeasure.not_isCompact_measure_unitBall {X : Type u_1} {K : Type u_3} [TopologicalSpace X] [CompactSpace X] [NontriviallyNormedField K] [TotallySeparatedSpace X] [Infinite X] : ¬IsCompact {L : C(X, K) →L[K] K | ‖L‖ ≤ 1}

The unit ball of the continuous dual on an infinite compact totally separated space is not compact for the operator norm. The coefficient field need not be complete, proper, or ultrametric.