Zulip Chat Archive

Stream: Is there code for X?

Topic: definite and indefinite integrals on the reals


view this post on Zulip Kevin Buzzard (Apr 13 2020 at 22:19):

Can we prove

t=01t2dt=13\int_{t=0}^1t^2\mathrm{d}t=\frac{1}{3}

or

t=1xdtt=log(x)\int_{t=1}^x\frac{\mathrm{d}t}{t}=\log(x)

for x>0x>0?

I'm sorry to use this stream for these questions. I haven't been keeping up with analysis at all and it's been moving fast. I am just looking at what our undergraduates do in their methods course and am wondering how much of it we can currently formalise.

view this post on Zulip Kevin Buzzard (Apr 13 2020 at 23:00):

PS I am not sure that I care which theory of integration one uses here, I am just looking for something which looks to a mathematician like it might say one of the theorems above.

view this post on Zulip Patrick Massot (Apr 14 2020 at 07:52):

No, there is a stuck PR that would allow to do that, but the author disappeared.

view this post on Zulip Yury G. Kudryashov (Apr 14 2020 at 17:38):

I can take over this PR once I'm done grading the exam.

view this post on Zulip Yury G. Kudryashov (Apr 14 2020 at 19:09):

If @Jeremy Avigad will say that it's OK.

view this post on Zulip Yury G. Kudryashov (Apr 14 2020 at 19:10):

Jeremy says that a couple of weeks ago @Joe said that he's going to come back to these PRs.

view this post on Zulip Jeremy Avigad (Apr 14 2020 at 19:18):

Yes, it is o.k. with me. I asked Joe to coordinate, so hopefully he will respond to the ping.


Last updated: May 07 2021 at 19:12 UTC