define null set and fix the definition of domination of measure/charge

[IshiguroYoshihiro]

Motivation for this change

This PR define null_set and use this for definition of nu `<< mu.
following, e.g., https://proofwiki.org/wiki/Characterization_of_Null_Sets_of_Variation_of_Signed_Measure
(definition for signed measures)

The previous definition can be recovered using the lemma
measure_null_dominatesP for contents and the lemma charge_null_dominatesP
for signed measures (https://proofwiki.org/wiki/Category:Absolutely_Continuous_Signed_Measures)

We recover the definition of nlab
(a null B satisfied m(A | B) = m(A), https://ncatlab.org/nlab/show/null+subset
or https://www.math.uwaterloo.ca/~beforres/PMath451/Course_Notes/Chapter4.pdf
Def 2.2.2) as the lemma null_setU.

fixes #1754

Checklist

• added corresponding entries in CHANGELOG_UNRELEASED.md

• added corresponding documentation in the headers

Reference: How to document

Merge policy

As a rule of thumb:

• PRs with several commits that make sense individually and that
  all compile are preferentially merged into master.
• PRs with disorganized commits are very likely to be squash-rebased.

Reminder to reviewers

• Read this Checklist
• Put a milestone if possible
• Check labels

[affeldt-aist]

@holgerthies

[IshiguroYoshihiro]

https://proofwiki.org/wiki/Characterization_of_Null_Sets_of_Variation_of_Signed_Measure
This lemma should be useful too.

[affeldt-aist]

https://proofwiki.org/wiki/Characterization_of_Null_Sets_of_Variation_of_Signed_Measure This lemma should be useful too.

Maybe turn this comment into a "wish" issue.

[affeldt-aist]

@holgerthies

ping :-)