How to define positive measure?

Stream: mathlib4

[Rahul Sahjwani]

I'm trying to make a definition of a positive measure but I'm not quite sure how to go about it. How would I say something like \mu is a Measure defined on a MeasureSpace \alpha inside the definition?

In particular I want to end up with the following definition: \mu is a positive measure on \alpha if \mu is defined on the set underlying \alpha and \mu(S) > 0 \forall measurable subsets S of \alpha.

[Kevin Buzzard]

Even S = the empty set?

[Rahul Sahjwani]

Sorry I meant \geq 0. So I suppose the word nonnegative is more appropriate.

[Kevin Buzzard]

You can take a look at the code samples in section 13 of my course here https://github.com/ImperialCollegeLondon/formalising-mathematics-2024/tree/main/FormalisingMathematics2024/Section13measureTheory to see some of the basics.

[Rahul Sahjwani]

Thank you!

[Kevin Buzzard]

And you can see from the definition of docs#MeasureTheory.Measure that in Lean's opinion, a measure is, amongst other things, an assignment of an "extended nonnegative real" docs#ENNReal to each measurable set, so in particular if you use Mathlib's definition of a measure then it will automatically be what you call positive.

[Rahul Sahjwani]

Oh, thats quite convinient! I am also trying to define a sigma finite measure so I will likely run into similar issues over there but that helps. Thank you!

[Kevin Buzzard]

I don't know the first thing about measure theory but I just typed "sigma finite measure" into LeanSearch here and it's giving me docs#MeasureTheory.SigmaFinite ; you can read the docstring yourself and see if it's what you want.

[Rahul Sahjwani]

That's exactly I was looking for! Thank you! I will make sure to use LeanSearch before asking from now on!