PR that depends on another

Stream: general

[Rémy Degenne]

how do I make a PR that uses code from another one, and is marked as depending on it? Do I create a new branch from the branch of the PR, then make my changes and PR the result? Then the dependent issues bot will mark it accordingly? Or is it all a more manual process.
I want to PR a proof that the almost-everywhere pointwise limit of ae_measurable functions is ae_measurable (in a metric, borel space), but I need a result from PR #5688

[Rémy Degenne]

My approach to that problem until now has been to simply wait for the other PR to be merged. After all, there is no hurry.

[Sebastien Gouezel]

I have just reviewed the PR, but I have a comment so I won't merge it right away.

For your question, you can merge the changes of the other PR into your own PR to get it to compile (or build directly your branch on top of the other one). To indicate that your PR is built on top of the other one, you should add at the end of your PR main comment the lines

---
- [ ] depends on: #5688

[Rémy Degenne]

Thanks! I suppose that I would then get a merge conflict if the other one is changed between the moment I merge it into my branch and the moment it gets merged into master, which I would resolve by merging master into my branch.

[Sebastien Gouezel]

Yes, you will need to merge master in any case.

[Rémy Degenne]

On the topic of the content of my coming PR: for measurable functions, measurability of the a.e. limit requires a complete measure, but that completeness is not required for the corresponding statement with ae_measurable functions, which I find really nice. Now I can remove that hypothesis of my proofs of the completeness of Lp spaces. Thanks for introducing those ae_measurable functions!

[Sebastien Gouezel]

In fact almost everywhere measurability is equivalent to measurability for the completed measure, so it is not suprising that this has such a nice behavior. This fact is not proved in mathlib (yet) because it is not really necessary for the development of the theory.

Sketch of proof that, if f is null-measurable, then it is ae-measurable (the other direction is trivial). Composing with arctan if necessary, we can assume that f is null-measurable and bounded. Take a canonical sequence of simple functions s_n approximating it. These simple functions are also null-measurable. Since they are simple, it is easy to modify them to obtain s'_n which is measurable and coincides almost everywhere with s_n. Then s'_n is a Cauchy sequence in L^1. Taking a subsequence if necessary, it converges almost everywhere, to a measurable function f' (which is given by the limit where convergence holds, and by 0 elsewhere). Then f coincides almost everywhere with f'.

[Patrick Massot]

If this isn't formalized, is it at least in some module docstring?

[Sebastien Gouezel]

It is in a commit message (of the PR introducing almost everywhere measurability). Not in a docstring as far as I remember.