Why is there no MeasureTheory.HasIntegral?

Stream: mathlib4

[Weiyi Wang]

In comparison, ∑' has a corresponding HasSum that effectively states both Summable and the resulting value. I would expect ∫ to similarly has a HasIntegral that states both Integrable and the result, but apparently there isn't one (except BoxIntegral.HasIntegral but that is for BoxIntegral)

I am wondering this because I find theories like MeasureTheory.integral_add hard to use, because you would need to separately supply a prove for integrability, and you will also need to do MeasureTheory.Integrable.add separately in preparation for the next operation in the proof chain.

[Yury G. Kudryashov]

The short answer is "because it was written this way".

[Yury G. Kudryashov]

We can consider a refactor but I'm not sure that we need it.

[Yury G. Kudryashov]

For many integrals that can be computed, integrability follows from continuity and can be filled in by fun_prop (possibly, with more lemmas tagged as fun_prop).

[Yury G. Kudryashov]

(note: I'm writing this after a long flight, so I may be very wrong; let's wait for the opinions of other people who use Mathlib integrals a lot)

[Weiyi Wang]

The integration I am working on comes from Fourier transform and is unfortunately "improper", or over an infinite interval, so I don't think continuity can help here...

[Weiyi Wang]

But I see what you mean "because it was written this way". The internal definition structure of sum and integral look indeed different. For now, I suppose I can write a wrapper HasIntegral for myself with some theorems I use

[Yury G. Kudryashov]

Do you have absolute convergence?

[Weiyi Wang]

I think I have. I can prove that my function decays exponentially