Zulip Chat Archive

Stream: new members

Topic: basic calculus in mathlib

Daniel Ever (Feb 06 2022 at 20:30):

browsing the chat, forums and so on I keep noticing people mention how there's very little basic calculus in mathlib so far (i.e., FTC, various properties for integrals, multivariable stuff + basic complex analysis).

as a complete stranger to mathlib and math formalization I find it very contrintuitive, given than many much more abstract and challenging ideas are successfully formalized as time goes by.

is there any serious underlying reason for such disparity? if so, what can be done about it? thanks!

Patrick Massot (Feb 06 2022 at 21:05):

It's partly because many people came here from algebra, and partly because we want to deduce simple versions from sophisticated ones.

Patrick Massot (Feb 06 2022 at 21:06):

For a very recent example, see https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/gelfand.20formula/near/270909030 where Sébastien is going crazy over the change of variable formula.

Kevin Buzzard (Feb 06 2022 at 21:13):

Basic single variable calculus had to wait until multivariable calculus which had to wait for topological vector spaces and the Bochner integral etc etc. Very recently we got things like FTC and some cases of Cauchy integral formula so things are now in a position to get going

Alex J. Best (Feb 06 2022 at 21:14):

I think the situation has improved a bit from some of the old threads. At least in the tests folder there are now many examples of single variable real integrals and derivatives being handled semi-automatically by simp. Depending on what you mean by basic calculus I'd say some of those examples cover a fair bit of material

Daniel Ever (Feb 06 2022 at 21:56):

and what would be the motivation for such a top-down approach, trying to define everything in the most general way? is it simply more economical to come up with a single definition and then extend it to particular cases of interest, rather than have many almost (but not exactly) the same definitions for separate cases which can't be easily unified and cause pain and disorganization in the library?

Last updated: Dec 20 2023 at 11:08 UTC