analysis
analysis copied to clipboard
math-comp
Lebesgue Stieltjes measure
Motivation for this change
This is an attempt at generalizing lebesgue_mesure.v.
RFC, FYI @hoheinzollern @IshiguroYoshihiro
We have only replayed the first part so far and plan to work on proving more properties soon.
Co-authored-by: @t6s
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.
I've just checked out the lemma statements (not the proofs), and it looks pretty neat. The existing hlength_measure canonical instance provides a reasonably nice interface for it. And Hahn_ext_measure. One thing that makes me particularly happy about this is I think I can use this to state "spectral theorem". But I'm not 100% sure if it's general enough. That's something I'll look into shortly. In the meanwhile, I have only one question about this work. You carry around the (ndf : {homo f : x y / (x <= y)%R}) (rcf : right_continuous f conditions a lot. Which is fine while writing the proofs, but I can imagine this generating a lot of annoying side conditions when using them. Is there a nice way to package that up? Would a canonical structure for this make sense? Perhaps it's too cumbersome.
It might be a good timing to approve this PR. @zstone1 ? @CohenCyril ? The changelog and the PR should be up-to-date. To summarize, the construction of the Lebesgue measure has been generalized to the Lebesgue Stieltjes measure but the original construction of the Lebesgue measure has been kept in a module. We have not tried to rework the theory of the Lebesgue measure in this PR, just a straightforward generalization. The theory of the Lebesgue Stieltjes measure will soon be developed further and there are other lemmas that use the Lebesgue measure in other pending PRs so we will have occasions to come back to the code before the next release. The comment about the Sorgenfrey line has been moved to an issue so that we do not forget.
