checking if function is a probability measure

Stream: Is there code for X?

[Torey Hilbert]

Hello! Is there code anywhere for checking whether a given function set α -> ennreal is a probability measure on the measurable space α?

Less focused, but also in general I'm a little confused as to how we're defining measures - I can't seem to actually find the σ-algebras anywhere and it seems what's going on is that they're implicitly part of measurable_space α and then a measure μ is a function set α -> ennreal where we just only talk about the properties of the function over sets (set B : α) where the proposition (measurable_set B) is true. Is my understanding correct, and if so, if I write down a function set α : ennreal how do I turn it into a measure? I tried using measure_space.of_measure (https://leanprover-community.github.io/mathlib_docs/measure_theory/measure/measure_space_def.html#measure_theory.measure.of_measurable) but I couldn't get it to work and I don't think I was using it right.

Thank you so much! (Also just to make sure, is this the right place for simple questions like this?)

[Heather Macbeth]

@Torey Hilbert Welcome! This might be an #xy problem -- I was trying to come up with an example to help you and couldn't think of one where the measure is given to us directly as a function. Can you say more about your context?

[Heather Macbeth]

The declaration docs#measure_theory.measure.of_measurable you mentioned should work, if your measure really is given to you as a function.

[Rish Vaishnav]

If you can show your function is an outer measure (docs#measure_theory.outer_measure) then you can use docs#measure_theory.outer_measure.to_measure, proving the Carathéodory criterion instead of the countably additive property may be easier. Once you have a measure, you can use docs#measure_theory.is_probability_measure. But yeah it would help to have a bit more context.

Regarding measurable spaces, from what I can tell we don't distinguish them from σ-algebras at the moment -- that is, they're defined on a type, rather than a set.

[Torey Hilbert]

Thank you for the response @Heather Macbeth - I'm working on trying to construct Markov Kernels, and I was modeling them as, for measurable spaces α and β, a function μ : α -> set β -> ennreals. When trying to write down the definition of such an object, I wanted to then say that for all x : α, the function λ B : set β, μ x B is a probability measure (well, its restriction to to only the sets in the σ-algebra of β is a measure at least).

After having given it more thought (and also realizing I don't understand structures yet apparently), I was considering taking a different approach and trying to make it a structure with a function α -> measure β and a function measurable_set β -> (α -> ennreals) that each have to satisfy they're own axioms. Alternatively I could take a totally different approach and look for a different characterization of the object because there are like 5 other defining properties that I could use instead Lol

[Heather Macbeth]

Torey Hilbert said:

I was modeling them as, for measurable spaces α and β, a function μ : α -> set β -> ennreals.

I was considering taking a different approach and trying to make it a structure with a function α -> measure β and a function measurable_set β -> (α -> ennreals) that each have to satisfy they're own axioms.

Can you take it to be just

a function α -> measure β

?

[Torey Hilbert]

I guess I can yeah - and then just have something that can pull the other collection of functions that I was referring from the measures. Thank you, this was really helpful :+1: (One last question - is α -> measure β the correct way to describe a function that accepts an element of α and gives a measure on β? I was worried I was going to have to use the Giry monad or something so this would be a big relief to hear)

[Torey Hilbert]

@Rish Vaishnav I'm sure I'll have to use this at some other point, so thank you for showing me this too!