Hahn decomposition theorem

[affeldt-aist]

• introduces signed measures

Co-authored-by: IshiguroYoshihiro

based on PR #836 (has been merged into master)

Motivation for this change

Things done/to do

• added corresponding entries in CHANGELOG_UNRELEASED.md
• added corresponding documentation in the headers

Automatic note to reviewers

Read this Checklist and put a milestone if possible.

[affeldt-aist]

@IshiguroYoshihiro could you also take a look?

[affeldt-aist]

@IshiguroYoshihiro could you also take a look?

ping

[affeldt-aist]

ping @IshiguroYoshihiro @t6s

[zstone1]

Look pretty good, actually. I haven't gone through the proofs in too much detail. But they look, more-or-less, aligned with the textbook proofs. While I'm sure there are probably improvements in there, I'm not too worried about it. Qed is Qed.

What interests me is the use of FinNumFun. It actually causes some headache later, with mine_cvg_0_cvg_0. That proof is pretty easy in R because _ * 2 and min (_,1) are both trivially continuous. It's annoying to have to reprove all this in \bar R. I would love to see

1. Somehow support this kind of sorta-heterogeneous types in the definition of this hierarchy.
2. Transport the goal from \bar R to R. This seems much more plausible. We could do it ad-hoc, by showing fine is a homeomorphism on the image of (fun n => mine (x n * (2^-1)%:E) 1). But it should be possible to do this more generically.

This is not a dealbreaker for merging the PR. I'm mostly just recording this discomfort. This is something always brushed under the rug in textbooks, so no surprise we gotta deal with it here.

[affeldt-aist]

Indeed, it is pretty frustrating to have this proof (mine_cvg_0_cvg_0) that literally embeds the proof for the case in R...

[affeldt-aist]

In the last commit b674879 I split the lemma mine_cvg_0_cvg_0 into pieces so that it isolates the subcase about R. It is a bit longer but hopefully it will be easier to handle when we'll figure out how to generalize. I'll issue about that upon merging.