feat(Analysis/BoxIntegral/Basic): a bounded, a.e. continuous function is integrable on a box

[js2357]

trafficstars

Prove that a bounded, a.e. continuous function on R^n is integrable on a box. In principle, this generalizes integrable_of_continuousOn, though it currently requires a.e. continuity on all of R^n rather than just on the box, so integrable_of_continuousOn is not a special case of it yet.

As an intermediate step, define the oscillation of a function at a point and prove some lemmas about oscillation.

---

[xroblot]

It would be nice if you could also add the equivalent of MeasureTheory.ContinuousOn.hasBoxIntegral for this case.

[xroblot]

Could you merge with Mathlib to resolve the conflict? I was busy grading copies lately but I should be able to have another look at this PR today or tomorrow

[xroblot]

I am not at all in expert in this domain so I cannot really comment on the math. The code we wrote is really good but sometimes a little less concise than the style used in Mathlib. I have done some suggestions in that direction but it is up to you to accept those or not or to modify them according to your own style.

[js2357]

I wouldn't really consider myself an expert in the area either, but I doubt that there's going to be a substantially easier way to prove this.

I accepted all the suggestions.

[xroblot]

I wouldn't really consider myself an expert in the area either, but I doubt that there's going to be a substantially easier way to prove this.

I accepted all the suggestions.

👍

At this point, I'll suggest that you make a post on Zulip in the PR reviews stream so that other people can have a look at this PR.

[js2357]

The latest version reduces the proof of the main theorem by about 20 lines of code, to try to address the comment about the proof being a little too long. (The ideas of the proof are not changed, only reorganized.) I think the reorganization also keeps the indentation under control better, so what's left is hopefully more readable.

[github-actions[bot]]

PR summary 74c655cb97

Import changes

No significant changes to the import graph

---

Declarations diff

+ AEContinuous.hasBoxIntegral + eq_zero_iff_continuousAt + eq_zero_iff_continuousWithinAt + integrable_of_bounded_and_ae_continuous + integrable_of_bounded_and_ae_continuousWithinAt + oscillation + oscillationWithin + oscillationWithin_eq_zero + oscillationWithin_nhd_eq_oscillation + oscillationWithin_univ_eq_oscillation + oscillation_eq_zero + to + uniform_oscillation + uniform_oscillationWithin

You can run this locally as follows

## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

[xroblot]

Could you please merge with master to solve the conflict. Eventually, this PR will move up the PR queue and will get a review but it needs to be without conflict for that.

[js2357]

Could you please merge with master to solve the conflict. Eventually, this PR will move up the PR queue and will get a review but it needs to be without conflict for that.

The new version of this is at #13968 -- that's the one that should be reviewed. I'm only keeping this PR alive for now to preserve the discussion here.

[xroblot]

Right, sorry. I got confused. I'll change the tag to WIP on this PR then to avoid any further confusion.

[jcommelin]

Since #13968 has been merged, I guess this one can be closed, right? If not, please reopen, and bring the PR up to date.