basic calculus in mathlib

Stream: new members

[Daniel Ever]

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]

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

[Patrick Massot]

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]

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]

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]

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?