Formalizing the change of variables formula for integrals in mathlib

Add to your list(s) Download to your calendar using vCal

• Professor Sébastien Gouëzel (Université de Rennes)
• Thursday 15 June 2023, 17:00-18:00
• MR20 Centre for Mathematical Sciences.

If you have a question about this talk, please contact Angeliki Koutsoukou-Argyraki.

Hybrid talk (please see abstract for link) Note: different room, MR20 this time

We report on a formalization of the change of variables formula in integrals, in the mathlib library for Lean. Our version of this theorem is extremely general, and builds on developments in linear algebra, analysis, measure theory and descriptive set theory. This is made possible by the highly integrated development model of mathlib.

WATCH ONLINE HERE : https://www.microsoft.com/en-gb/microsoft-teams/join-a-meeting?rtc=1 Meeting ID: 379 992 884 209 Passcode: TYR8 Sh

This talk is part of the Formalisation of mathematics with interactive theorem provers series.

This talk is included in these lists:

• All CMS events
• All Talks (aka the CURE list)
• CMS Events
• Cambridge talks
• DPMMS Lists
• DPMMS Pure Maths study groups
• DPMMS info aggregator
• DPMMS lists
• Department of Computer Science and Technology talks and seminars
• Formalisation of mathematics with interactive theorem provers
• Hanchen DaDaDash
• Interested Talks
• MR20 Centre for Mathematical Sciences
• School of Physical Sciences
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31

Note that ex-directory lists are not shown.