Commit 2024-07-08 07:29 7dd2c4d8

feat(Analysis/BoxIntegral/Basic): a bounded, a.e. continuous function is integrable on a box (#13968) 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 function at a point x (and oscillationWithin for the oscillation at x within a specific subset). Also prove some lemmas about oscillation, namely that oscillation is 0 at a point if and only if the function is continuous there, and a statement about uniformity of oscillation on a compact set, with versions for oscillation and oscillationWithin. This is essentially the same as #13013, but I'm making a new PR because I messed up the other branch.