I found this reference for measure-theoretic integration in Lean. However, I cannot find any integration in the Lean 4 Measure Theory library. Have these not yet been ported, or can they be found elsewhere? Would it be particularly difficult to do this? I'd like to be able to talk about general integration in the setting of a functional analysis project I've been considering, but I unfortunately don't know anything about porting from Lean 3 to Lean 4.

Hence the second part of the question: How does porting form Lean 3 to Lean 4 work? What process goes into adapting the library? Is it all manual work, or do we have a program capable to converting between the two?

  • 2
    $\begingroup$ Porting is nearly done, we're looking at early to mid July for the completion. You can check which mathlib3 files have been ported here leanprover-community.github.io/mathlib-port-status $\endgroup$ Commented Jun 20, 2023 at 15:42
  • $\begingroup$ @KevinBuzzard Impressive. Is it possible that these definitions are 3rd party work that hasn't been added to the library? I don't see any measure theory files in progress. $\endgroup$
    – Alex Byard
    Commented Jun 20, 2023 at 15:57
  • $\begingroup$ @KevinBuzzard Btw, who does the porting? Is it just individuals working for Microsoft? $\endgroup$
    – Alex Byard
    Commented Jun 20, 2023 at 15:58
  • 1
    $\begingroup$ @AlexByard The “interval integral” seems to be ported: leanprover-community.github.io/mathlib4_docs/Mathlib/… $\endgroup$
    – Jason Rute
    Commented Jun 20, 2023 at 18:20
  • 1
    $\begingroup$ @AlexByard, if you come over to leanprover.zulipchat.com and post a message, we can help you work out what "it" and "everything" are, and how to make them not broken. :-) $\endgroup$ Commented Jun 21, 2023 at 3:21


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.