University of Cambridge > Talks.cam > Formalisation of mathematics with interactive theorem provers > Formalizing the change of variables formula for integrals in mathlib

  Browse A-Z

Log in

Googledetails Microsoftdetails

🔐 Log In

Information on

Subscribing to talksdetails Finding a talkdetails Adding a talkdetails Disseminating talksdetails Help and Documentationdetails

ℹ️ Information

Formalizing the change of variables formula for integrals in mathlib

Download to your calendar using vCal

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:

Note that ex-directory lists are not shown.

Other lists

Teams - the link will be sent on the day. Please register at https://bit.ly/Empathy_during_infancy Average on weekdays: 8923.25747863 kWh The Computer Laboratory, FW26 and Online

Other talks

Tea and Coffee Break Together Now: Cooperation and Collaboration in Social Art Practice Title to be confirmed Title TBC Title TBC Title to be confirmed
 

© 2006-2025 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity