signed measure

Stream: maths

[Jason KY.]

Hi,
I would like to prove Hahn decomposition and am I correct in saying that there is no signed measure in mathlib yet?
Using the definition from wikipedia, I think a natural definition for this is to define a signed measure as a function to with_top \R (satisfying the axioms). Would this be a good idea? Would theory about with_top \R be welcome in mathlib?

[Johan Commelin]

ereal is the type of real + infty. It's already in mathlib.

[Johan Commelin]

signed measures, I don't know

[Jason KY.]

I think ereal includes the negative infinity as well which I don't think is good for the definition of signed measure

[Sebastien Gouezel]

If mu is a signed measure, you want -mu to also be a signed measure. So, if you allow plus infinity, you also need minus infinity (and indeed ereal contains both).

[Jason KY.]

Thats a good point, thanks. In that case, would the following definition be any good?

structure signed_measure (α : Type*) [measurable_space α] :=
(measure_of : set α → ereal)
(empty : measure_of ∅ = 0)
(m_Union ⦃f : ℕ → set α⦄ :
  (∀ i, measurable_set (f i)) → pairwise (disjoint on f) →
  measure_of (⋃ i, f i) = ∑' i, measure_of (f i))

class faithful (s : signed_measure α) :=
(is_faithful : ∀ (a b : set α) (ha : measurable_set a) (hb : measurable_set b),
  s.measure_of a = ⊤ → s.measure_of b ≠ ⊥)

[Sebastien Gouezel]

It depends on what you want to do. Most signed measures I have ever encountered had finite total variation, and in this case you could even take the measure to be real-valued (or more generally vector-space valued, which has the advantage of treating in particular complex-valued measures). If allowing infinity is important for you, though, then I think your definition looks good (although I am not completely sure if you shouldn't add some summability assumptions -- but you will see that when trying to formalize theorems).

[Jason KY.]

I've now continued to work with the definition (and it seems that you were correct in that I didn't need infinity anyway) and gotten as far as proving the Hahn decomposition and the Jordan decomposition theorem. I've now realized a problem with this definition where two signed measures are equal iff the underlying function is equal for every set \a. This is not what I want since I would like two signed measure to be equal if they agree on measurable sets. To fix this I added the condition that a signed measure on nonmeasurable set is 0 (see here) and it seems to work fine. Is this a reasonable condition? Is there a better method of fixing this problem? Thanks

[Yaël Dillies]

What about the trick of defining the measure of a non measurable set as the sup of the measures of its measurable subsets?

[Sebastien Gouezel]

Are you aware that the Hahn decomposition is already in mathlib (for positive measures) in docs#measure_theory.hahn_decomposition ?

[Jason KY.]

Do I impose that as a condition in the structure, or do you mean do something similar to what was done for outer_measure for normal measures

[Jason KY.]

Sebastien Gouezel said:

Are you aware that the Hahn decomposition is already in mathlib (for positive measures) in docs#measure_theory.hahn_decomposition ?

Can I deduce the signed measure version from the positive measure version?

[Sebastien Gouezel]

That's not obvious to me!

[Jason KY.]

I guess my question is, should I pr what I have now or do you think my definition is crappy and needs to be reworked

[Sebastien Gouezel]

I think you should probably go for a general definition of vector-valued measure, called vector_measure, and require in the definition that things are summable, via

m_Union ⦃f : ℕ → set α⦄ :
  (∀ i, measurable_set (f i)) → pairwise (disjoint on f) →
  has_sum (λ i, measure_of (f i))) (measure_of (⋃ i, f i))

But your restriction that the measure of non-measurable sets should be zero looks perfectly fine to me.

Then develop everything you can for general vector-valued measure (to handle simultaneously signed measures and complex measures), and specialize to signed measures only when it's needed (no need for a new name, just use vector_measure ℝ).

[Jason KY.]

I wonder if we need to require things to be summable. In my current definition, I was able to prove that

theorem summable_measure_of
  (hf₁ : ∀ i, measurable_set (f i)) (hf₂ : pairwise (disjoint on f)) :
  summable (s ∘ f) := -- where `s` is any signed measure, `f : \N \to set \a`

[Jason KY.]

I will definitely try to generalize the definition for vector valued measures and report back when I made some progress

[Sebastien Gouezel]

Jason KY. said:

I wonder if we need to require things to be summable.

Maybe it's not strictly necessary, but in any case the definition will be usable only if it implies summability, so you might as well require it directly.

[Sebastien Gouezel]

Whenever you check that you have a vector measure, when checking m_Union even in its weak version you will need to prove the summability (because otherwise you won't be able to prove anything), so requiring summability in the definition will not make checking it harder, and it will make using it easier.

[Jason KY.]

I see what you mean, I will add the condition in that case

[Jason KY.]

Actually, i'm not sure requiring summability makes using it easier since in that case, we need to prove summable f whenever we want to use this property

[Jason KY.]

But, I think it might be necessary to require it nonetheless since I believe the proof only works for finite dimensional spaces

[Sebastien Gouezel]

My advice is to require has_sum in the property m_Union, see https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/signed.20measure/near/244965136. It requires that, for any disjoint sets f i, their measures are summable, and add up to the measure of their union.

[Sebastien Gouezel]

So, when you use it you don't need to prove summability, instead summability is given to you for free.

[Jason KY.]

Ah! Sorry I missed your suggestion. Thats much better than what I had in mind

[Jason KY.]

@Sebastien Gouezel This is what I have right now: https://github.com/JasonKYi/probability_theory/blob/main/src/vector_measure.lean#L41
Is there anything else you think needs changing?