Integral of 1/sqrt(x)

Stream: Is there code for X?

[David Loeffler]

Is there an easy way to locate in the library a proof of the integrability of x^t on [0..1], for real t with -1 < t < 0?

[Alex J. Best]

is docs#interval_integrable_rpow what you want?

[Alex J. Best]

I found this by thinking that it probably just follows from continuity, and then when searching for continuous.*rpow I saw one of the results was in analysis.special_functions.integrals so was probably right

[David Loeffler]

Hi Alex. Unfortunately that is not what I want, since it only handles the case of exponents >= 0 (where the result does indeed follow trivially from continuity). I am interested in the case of exponents in the range -1 < t < 0 in which case the integrand is not continuous at the lower endpoint -- it blows up, but slowly enough that the total integral is still finite.

[Heather Macbeth]

@David Loeffler This might really be missing. You could probably prove, using the fundamental theorem of calculus (see docs#interval_integral.integral_eq_sub_of_has_deriv_right_of_le and the variants which follow), that the interval_integral is $(1+t)^{-1}$. Then you could make a series of arguments to say that the interval_integral equals the integral which equals the lintegral and therefore the lintegral is finite. Not sure if there's a better way ...

[David Loeffler]

I'm afraid this would be circular, since interval_integral.integral_eq_sub_of_has_deriv_right_of_le has integrability among its assumptions!

[Heather Macbeth]

Here's a version without, I think: docs#interval_integral.integral_deriv_eq_sub'

[Heather Macbeth]

(Would take you up to epsilon above the endpoint.)

[David Loeffler]

That one won't work either, since it assumes existence of the derivative everywhere (including the endpoints).

Getting an integral over [eps, 1] for eps > 0, and showing that it tends to a limit as eps -> 0, is easy enough; the problem is showing that this limit is equal to the integral over [0, 1].

[David Loeffler]

@Yury G. Kudryashov Yury: do you have any thoughts on this?

[Heather Macbeth]

Maybe monotone convergence? docs#measure_theory.lintegral_tendsto_of_tendsto_of_monotone

[Heather Macbeth]

(Applied to the functions $f_n(x)$ which are piecewise $x^t$ on $[\tfrac{1}{n}, 1]$ and $0$ elsewhere.)

[David Loeffler]

Monotone convergence sounds like the mathematically correct approach, but it doesn't look straightforward to implement!

[Anatole Dedecker]

I developed tools for things like that last year, you should have a look docs#measure_theory.ae_cover. There are a few specific results at the end of the file but they don’t correspond to your case (computing an integral over a finite interval by computing it on smaller finite intervals). You should have a look

[Anatole Dedecker]

By the way, I was discovering measure theory at that time, so I’ve got a few ideas on way to improve this file, so I’ll work on that again at some point

[Bhavik Mehta]

You could also do a substitution t = 1/x to get an integral over [1, infty), which can be evaluated using the lemmas Anatole is talking about (indeed I needed that case in the unit-fractions project here)

[David Loeffler]

@Bhavik Mehta Unfortunately the integration-by-substitution stuff only seems to work for integrals with finite endpoints, so we can't use this to relate integrals over (0, 1) and over (1, \infty).

[Vincent Beffara]

David Loeffler said:

Monotone convergence sounds like the mathematically correct approach, but it doesn't look straightforward to implement!

In that particular case you would probably apply monotone convergence to $(x+1/n)^t$ rather than $x^t 1_{[1/n,1]}$, this requires special-casing the sign of the exponent (and you know that $t<0$ so you are fine) but the rest of the argument would be straightforward.

[David Loeffler]

I guess my concerns about the complication of implementing this aren't so much about the choice of the sequence of functions to use, but about navigating the API for measure theory in mathlib -- I'd rather not have to think about outer integrals, coercion between reals and ennreals, ae_covers etc. But maybe there's no avoiding it.

[Johan Commelin]

Do you feel like there is a hole in the API that you can pin down?

[Anatole Dedecker]

There are definitely missing results in the ae_cover file. docs#ae_cover is really meant to be a tool for factoring proofs, but we should state all the usefuk consequences imo. I'll try to add the missing results today or tomorrow, and see how hard it is to get what you want from there.

[Bhavik Mehta]

I think docs#ae_cover could do with versions for covering finite intervals by approximation of nested sets (in three versions, depending on which endpoints you want to take as a limit), then the existing general lemmas should be applied to these to get the useful lemmas. It's already very helpful for infinite intervals so I'm confident that Anatole has the right approach for doing it generally

[Yury G. Kudryashov]

IMHO, we should add a version of the FTC that assumes that the derivative is nonnegative but does not assume integrability of the derivative.

[Yury G. Kudryashov]

I can't come up with a short proof right now. I'll try not to forget to think about it tomorrow.