radon measures

Stream: maths

[Johan Commelin]

Has anything been done with Radon measures? https://en.wikipedia.org/wiki/Radon_measure
I don't think mathlib has anything about them, so far.

[Johan Commelin]

I guess mathlib has all the ingredients for the measure theoretic definition (inner regular, locally finite). But what about the functional analytic approach? Do we have ctu functions with compact support?

[Johan Commelin]

Aha docs#has_compact_support exists. But not the bundled locally convex TVS.

[Kalle Kytölä]

Not exactly an answer to @Johan Commelin's question, but in my opinion related:

@Jesse Reimann is working on the Riesz-Markov-Kakutani representation theorem (i.e., characterizing positive linear functionals on compactly supported continuous functions on locally compact Hausdorff spaces as regular Borel measures). First in compact Hausdorff spaces, though, in which case the relevant measures are simply finite Borel measures (regularity is automatic) and there is no need to require compact support, so one in fact simply characterizes the dual of X →ᵇ ℝ≥0 (indeed the full dual (X →ᵇ ℝ≥0) →ₗ[ℝ≥0] ℝ≥0, which just happens to coincide with the mere topological dual (X →ᵇ ℝ≥0) →L[ℝ≥0] ℝ≥0). The locally compact case should not be an awful lot harder (although you never know what Lean throws at you).

[Johan Commelin]

Thanks, maybe we should just go with that dual space, and postpone the measure theoretic definition to some later point in time.

[Moritz Doll]

Defining $C_c(X)$ might be a good way to test whether the locally convex space library has everything one needs for concrete applications.

[Anatole Dedecker]

Well I defined $C_c^n(X)$ in my distribution projects, and it went quite well, so that should be okay. If anyone needs it I can work on this.

[Anatole Dedecker]

(Maybe « It went well » is over optimistic, I should say « I added the missing API to make it work well »)

[Anatole Dedecker]

Kalle Kytölä said:

Not exactly an answer to Johan Commelin's question, but in my opinion related:

Jesse Reimann is working on the Riesz-Markov-Kakutani representation theorem (i.e., characterizing positive linear functionals on compactly supported continuous functions on locally compact Hausdorff spaces as regular Borel measures). First in compact Hausdorff spaces, though, in which case the relevant measures are simply finite Borel measures (regularity is automatic) and there is no need to require compact support, so one in fact simply characterizes the dual of X →ᵇ ℝ≥0 (indeed the full dual (X →ᵇ ℝ≥0) →ₗ[ℝ≥0] ℝ≥0, which just happens to coincide with the mere topological dual (X →ᵇ ℝ≥0) →L[ℝ≥0] ℝ≥0). The locally compact case should not be an awful lot harder (although you never know what Lean throws at you).

This is really nice btw ! Which proof are you following ?

[Jesse Reimann]

Anatole Dedecker said:

This is really nice btw ! Which proof are you following ?

We're following Rudin's proof - but at least for compact X we are shortening the construction of the measure by instead using docs#measure_theory.content.