Higher order differential calculus in Mathlib

on YouTube ↗26m

" summary

A higher‑order differential calculus library is implemented in Mathlib using Lean that supports arbitrary scalar fields, functions on domains (not only open sets), and a unified C^n/C^∞/C^ω hierarchy. It replaces naive derivative-within choices by a local C^n-on-domains definition to avoid nonuniqueness, adds analytic (C^ω) hypotheses so second derivatives remain symmetric over exotic fields like Q_p, and provides an API that lets existing proofs survive the refactor. This enables formalized Lie group and Lie algebra constructions across fields and it works in practice.

AI-written summary · about

" chapters (13)

1. 0:00Talk introduction
2. 1:57Textbook definitions fail
3. 3:00Derivative in arbitrary dims
4. 4:28Derivatives with domain restr
5. 8:00Textbook higher order limits
6. 10:12Need domains and field support
7. 12:02Defining CN functions challenges
8. 15:56Local CN function definition
9. 18:02Final CN function definition
10. 19:03Lie groups application refactor
11. 23:19Unified Lie group approach
12. 24:01Refactoring CN maps lessons
13. 25:03Q&A