James Sundstrom

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

1

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...

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

2

Prove that a function that is bounded and a.e. continuous within a box is integrable on that box. This generalizes integrable_of_continuousOn. As an intermediate step, define the oscillation of a...