fubini for s-finite measures #877
Conversation
affeldt-aist
added
the
enhancement ✨
There was a problem hiding this comment.
Proof makes sense. Personally, I like this style of equational reasoning. The explicit terms appearing in the transitivity calls make it clear how the sums and integrals are moving around. It's very much how a measure theory textbook would feel to read.
Inspired by agda's equational reasoning stuff, I made a little notation to for formalize it in a different library. See https://github.com/zstone1/coq-complex/blob/master/src/helpers.v around line 170. It has the benefit of being able to _ away unchanged terms. I'd love to have something like this in mathcomp. Also it's generalized to any transitive reflexive relation, including < and <=.
|
Thanks for taking a look. Indeed, the proof mimics a paper proof presented like equational reasoning, see page 16 of http://www.cs.ox.ac.uk/people/samuel.staton/papers/esop2017.pdf. |
Example of use: Indeed, I believe that there are situations where an approach which highlights what's changing improves maintainability despite the extra verbosity. |
Do you want to record this as a wish issue before merging? |
work on Hoelder's inequality expeS, fin_numX (math-comp#829) \bar R canonicals for tblattice Co-authored-by: Quentin Vermande <[email protected]> Co-authored-by: Alessandro Bruni <[email protected]> Co-authored-by: Takafumi Saikawa <[email protected]> Co-authored-by: Reynald Affeldt <[email protected]> add lemma power12_sqrt fix and strengthen eq_bigmax and eq_bigmin (math-comp#863) Itv (math-comp#869) * Add itv.v Taking inspiration on signed.v, replacing sign by intervals. * Add interval multiplication * Add hints to automatically solve _ <= 1 goals * Test to see if usable as a replacement for prob * use notation from mathcomp_extra.v * changelog and rm redundant code * prefix duplicated identifiers --------- Co-authored-by: Reynald Affeldt <[email protected]> complete changelog fubini for s-finite measures (math-comp#877) fixes, cleaning powere_pos lemmas fixed `powere_pos` definition more lemmas for `powere_pos` progress in fixing hoelder wip powere_pos lemmas cleanup up wip wip
work on Hoelder's inequality expeS, fin_numX (math-comp#829) \bar R canonicals for tblattice Co-authored-by: Quentin Vermande <[email protected]> Co-authored-by: Alessandro Bruni <[email protected]> Co-authored-by: Takafumi Saikawa <[email protected]> Co-authored-by: Reynald Affeldt <[email protected]> add lemma power12_sqrt fix and strengthen eq_bigmax and eq_bigmin (math-comp#863) Itv (math-comp#869) * Add itv.v Taking inspiration on signed.v, replacing sign by intervals. * Add interval multiplication * Add hints to automatically solve _ <= 1 goals * Test to see if usable as a replacement for prob * use notation from mathcomp_extra.v * changelog and rm redundant code * prefix duplicated identifiers --------- Co-authored-by: Reynald Affeldt <[email protected]> complete changelog fubini for s-finite measures (math-comp#877) fixes, cleaning powere_pos lemmas fixed `powere_pos` definition more lemmas for `powere_pos` progress in fixing hoelder wip powere_pos lemmas cleanup up wip wip
Motivation for this change
This PR contains only one lemma: Fubini for s-finite measure, it comes from the PR on kernels (PR #749 ).
Things done/to do
CHANGELOG_UNRELEASED.md- [ ] added corresponding documentation in the headersAutomatic note to reviewers
Read this Checklist and put a milestone if possible.