Proving Interval Integrability

Stream: mathlib4

[Michael Lopez]

Hello, I am trying to prove that a function is IntervalIntegrable, does anybody have experience with this? Any direction on this would be helpful.

[Patrick Massot]

This question isn't specific enough to allow people to help you. You need to tell us more about your function.

[Scott Morrison]

Perhaps a #mwe would be helpful?

[Floris van Doorn]

One common way this holds is because the function is continuous: docs4#Continuous.intervalIntegrable