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

[js2357]

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.

---

[github-actions[bot]]

PR summary c706e4dcfa

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
73 files Mathlib.Analysis.Complex.Polynomial Mathlib.NumberTheory.Cyclotomic.Rat Mathlib.NumberTheory.LSeries.HurwitzZetaValues Mathlib.NumberTheory.Harmonic.ZetaAsymp Mathlib.NumberTheory.Cyclotomic.Discriminant Mathlib.Analysis.Distribution.FourierSchwartz Mathlib.NumberTheory.GaussSum Mathlib.NumberTheory.EulerProduct.DirichletLSeries Mathlib.Analysis.Complex.AbsMax Mathlib.Geometry.Manifold.Complex Mathlib.Analysis.SpecialFunctions.Gamma.Beta Mathlib.Analysis.Complex.TaylorSeries Mathlib.Analysis.NormedSpace.Star.GelfandDuality Mathlib.MeasureTheory.Integral.DivergenceTheorem Mathlib.NumberTheory.NumberField.Discriminant Mathlib.Analysis.SpecialFunctions.Gamma.Deligne Mathlib.Analysis.Complex.PhragmenLindelof Mathlib.NumberTheory.ModularForms.JacobiTheta.Manifold Mathlib.NumberTheory.Cyclotomic.Three Mathlib.NumberTheory.LSeries.HurwitzZetaEven Mathlib.NumberTheory.LSeries.Deriv Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation Mathlib.Analysis.Fourier.Inversion Mathlib.Analysis.SpecialFunctions.Complex.Analytic Mathlib.Analysis.NormedSpace.Spectrum Mathlib.NumberTheory.Harmonic.GammaDeriv Mathlib.Analysis.Complex.CauchyIntegral Mathlib.Analysis.NormedSpace.Star.ContinuousFunctionalCalculus Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable Mathlib.Analysis.NormedSpace.Star.Spectrum Mathlib.NumberTheory.Cyclotomic.Embeddings Mathlib.Analysis.Complex.Schwarz Mathlib.NumberTheory.LSeries.RiemannZeta Mathlib.Analysis.NormedSpace.Algebra Mathlib.NumberTheory.FLT.Three Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody Mathlib.NumberTheory.NumberField.Units.Basic Mathlib.NumberTheory.DirichletCharacter.GaussSum Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable Mathlib.NumberTheory.LSeries.Dirichlet Mathlib.Tactic.NormNum.LegendreSymbol Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable Mathlib.Analysis.BoxIntegral.Basic Mathlib.Analysis.BoxIntegral.Integrability Mathlib.Analysis.Complex.RemovableSingularity Mathlib.Analysis.Complex.Liouville Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum Mathlib.Analysis.NormedSpace.Star.ContinuousFunctionalCalculus.Instances Mathlib.NumberTheory.LSeries.MellinEqDirichlet Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol Mathlib.Analysis.Complex.LocallyUniformLimit Mathlib.NumberTheory.LegendreSymbol.AddCharacter Mathlib.NumberTheory.Cyclotomic.PID Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity Mathlib.Analysis.NormedSpace.Star.ContinuousFunctionalCalculus.Order Mathlib.Analysis.NormedSpace.Star.ContinuousFunctionalCalculus.Restrict Mathlib.NumberTheory.NumberField.Units.DirichletTheorem Mathlib.NumberTheory.NumberField.Units.Regulator Mathlib.RingTheory.Polynomial.Selmer Mathlib.Analysis.MellinInversion Mathlib.Topology.ContinuousFunction.UniqueCFC Mathlib.NumberTheory.LSeries.HurwitzZetaOdd Mathlib.Analysis.Complex.Hadamard Mathlib.NumberTheory.NumberField.Embeddings Mathlib.Algebra.Polynomial.UnitTrinomial Mathlib.Analysis.Complex.OpenMapping Mathlib.NumberTheory.NumberField.ClassNumber Mathlib.NumberTheory.LSeries.HurwitzZeta Mathlib.Tactic Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform Mathlib.Analysis.BoxIntegral.DivergenceTheorem Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic	1
Mathlib.Analysis.Oscillation	838

---

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 + 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]

Two minor comments; I trust @xroblot has reviewed the mathematics.

Well, I am no an expert in this domain (although I know more and more about it thanks to Lean :wink:) but I can say two things: 1) the statement proved here in the same as the one on Wikipedia; 2) it fits perfectly with my application to number theory.

[github-actions[bot]]

🚀 Pull request has been placed on the maintainer queue by Ruben-VandeVelde.

[riccardobrasca]

Thanks!

bors merge

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style