Signed measures as Banach space

Stream: Is there code for X?

[Tomas Skrivan]

Is there a result saying that the space of all signed measures with finite total variation form a Banach space?

[Tomas Skrivan]

(ahh sorry I wanted to post this to "Is there code for X?")

[Jireh Loreaux]

I'm not aware that we even have a topology on measures of any flavor (except maybe probability measures), let alone a norm structure. (I'm not super familiar with that end of the library though, so I could be wrong, but I couldn't find it in the docs either.)

[Tomas Skrivan]

Ahh that is too bad, I want to formalize semantics for differentiation of probabilistic programs and I would need that.

[Rémy Degenne]

We have a topology on finite measures and probability measures. docs#MeasureTheory.FiniteMeasure.instTopologicalSpace
There is an open PR for a distance #8719
We don't have much about signed measures though.