integration by parts

[affeldt-aist]

Motivation for this change

preliminary usable version of integration by parts

(and "within continuous" version of continuous_FTC2)

NB: we've been trying to "weaken" the hypotheses of lemmas in ftc.v to avoid requiring integrability over the whole set in the hope to ease their applications (this seems to be confirmed by the use of the new version of continuous_FTC1 to prove change-of-variables lemma)

based on PR #1246 (merged)

FYI @IshiguroYoshihiro

Checklist

• added corresponding entries in CHANGELOG_UNRELEASED.md

- [ ] added corresponding documentation in the headers

Reference: How to document

Reminder to reviewers

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

[zstone1]

A few annoying boundary condition issues. If you want, we can weaken those conditions via tietze, or other limiting approaches if the proofs are hard to edit. If you want some guidance on that I'm happy to provide.

[affeldt-aist]

The last commit weakens the hypotheses from {in _, continuous _} to {within _, continuous _} of the corollary of FTC1 ("FTC2 for continuous functions") and of integration by parts (newly introduced). I went through a weakening of the hypotheses of FTC1 theorems for that purpose: moving from integrability over the whole set to local integrability + integrability over a family of intervals possibly open-ended on the left (the two are redundant when dealing with bounded intervals but not when the interval on which we want to integrate is say ]-oo, x]). By the way, the resulting theorems are used in another branch to prove properties of the beta distribution, so they are usable in practice.

[zstone1]

I'm a little confused by requiring both

  mu.-integrable [set` Interval a (BRight u)] (EFin \o f) ->
  locally_integrable setT (f \_ [set` Interval a (BRight u)]) ->

If I were being optimistic, I would expect that

mu.-integrable [set` Interval a (BRight u)] (EFin \o f)

actually just implies

mu.-integrable setT (EFin \o f \_ [set` Interval a (BRight u))

unconditionally. So the original form of FTC0 applies. I haven't actually tried this, so I'm curious what will go wrong.

[affeldt-aist]

Let me try...

[affeldt-aist]

You are right, I have visibly been confused, fixing the PR right now.

[zstone1]

Ok, glad we could simplify that. My next question is, if you leave the original FTC0 alone, and add a this new statement as FTC0_restricted, can we simplify the proof by just applying FTC0 with the restricted function?

[affeldt-aist]

I think that I have a script that does that, should be pushed by tomorrow.

[affeldt-aist]

it seems so: see a078951

[zstone1]

A few more thoughts on ways to simplify the conditions does these lemmas.

[zstone1]

Since R is locally compact, this is the same as

(\forall r \near 0^'+, integrable setT (f \_ (closed_ball x r)))

There is also the powerser_filter_from thing which let's you state it as

(\forall U \near powerset_filter_from (nbhs x),, integrable U f)

Either is fine.

[affeldt-aist]

I have reverted to this version:

Lemma nice_lebesgue_differentiation (f : R -> R) :
  locally_integrable setT f -> forall x, lebesgue_pt f x ->
  (fine (mu (E x n)))^-1%:E * \int[mu]_(y in E x n) (f y)%:E
    @[n --> \oo] --> (f x)%:E.

[zstone1]

Ok, glad we could simplify that. My next question is, if you leave the original FTC0 alone, and add a this new statement as FTC0_restricted, can we simplify the proof by just applying FTC0 with the restricted function?

[zstone1]

Ah, this looks much cleaner now! Thanks for all the updates. There's always more proof linting to do, but I'm not seeing any more structural issues. I'm fine to merge if/when you're happy with the state of the proof scripts.

[affeldt-aist]

I did some more linting and I don't mind if you squash and merge.
There is surely room for improvement but we might come back to
it soon with integration by substitution in the pipeline anyway.