nach oben

Tipp

A Coq Formalization of Lebesgue Integration of Nonnegative Functions

verfasst von: Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, Micaela Mayero

Erschienen in: Journal of Automated Reasoning | Ausgabe 2/2022

Einloggen, um Zugang zu erhalten

Abstract

Integration, just as much as differentiation, is a fundamental calculus tool that is widely used in many scientific domains. Formalizing the mathematical concept of integration and the associated results in a formal proof assistant helps in providing the highest confidence on the correctness of numerical programs involving the use of integration, directly or indirectly. By its capability to extend the (Riemann) integral to a wide class of irregular functions, and to functions defined on more general spaces than the real line, the Lebesgue integral is perfectly suited for use in mathematical fields such as probability theory, numerical mathematics, and real analysis. In this article, we present the Coq formalization of \(\sigma \)-algebras, measures, simple functions, and integration of nonnegative measurable functions, up to the full formal proofs of the Beppo Levi (monotone convergence) theorem and Fatou’s lemma. More than a plain formalization of the known literature, we present several design choices made to balance the harmony between mathematical readability and usability of Coq theorems. These results are a first milestone toward the formalization of \(L^p\) spaces such as Banach spaces.

Nächster Artikel A Bi-Directional Extensible Interface Between Lean and Mathematica

Sie möchten Zugang zu diesem Inhalt erhalten? Dann informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 69.000 Bücher
über 500 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt 90 Tage mit der neuen Mini-Lizenz testen!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 58.000 Bücher
über 300 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt 90 Tage mit der neuen Mini-Lizenz testen!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 50.000 Bücher
über 380 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt 90 Tage mit der neuen Mini-Lizenz testen!

Jetzt informieren

The

https://static-content.springer.com/image/art%3A10.1007%2Fs10817-021-09612-0/MediaObjects/10817_2021_9612_Figkb_HTML.gif

inductive set from https://isabelle.in.tum.de/dist/library/HOL/HOL-Analysis/Sigma_Algebra.html.

The

https://static-content.springer.com/image/art%3A10.1007%2Fs10817-021-09612-0/MediaObjects/10817_2021_9612_Figkc_HTML.gif

inductive type from https://leanprover-community.github.io/mathlib_docs/measure_theory/measurable_space_def.html#measurable_space.generate_measurable.

The

https://static-content.springer.com/image/art%3A10.1007%2Fs10817-021-09612-0/MediaObjects/10817_2021_9612_Figkn_HTML.gif

operator from https://leanprover-community.github.io/mathlib_docs/topology/algebra/infinite_sum.html#tsum.

https://www.cs.ru.nl/~freek/100/.

https://isabelle.in.tum.de/dist/library/HOL/HOL-Analysis/Nonnegative_Lebesgue_Integration.html.

https://shemesh.larc.nasa.gov/fm/ftp/larc/PVS-library/library/measure_integration.html, https://shemesh.larc.nasa.gov/fm/ftp/larc/PVS-library/library/lebesgue.html.

https://leanprover-community.github.io/mathlib_docs/measure_theory/constructions/borel_space.html#borel_space.

https://leanprover-community.github.io/mathlib_docs/measure_theory/integral/lebesgue.html#measure_theory.simple_func.

https://github.com/math-comp/analysis.

Abdulaziz, M., Paulson, L.C.: An Isabelle/HOL formalisation of Green’s theorem. In: Blanchette, J.C., Merz, S. (eds.) Proceedings of the 7th International Conference on Interactive Theorem Proving (ITP 2016), Volume 9807 of Lecture Notes in Computer Science, pp. 3–19. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-43144-4_1

Adams, R.A.: Sobolev Spaces. Pure and Applied Mathematics, vol. 65. Academic Press, New York–San Francisco–London (1975)

Affeldt, R., Cohen, C., Mahboubi, A., Rouhling, D., Strub, P.-Y.: Classical analysis with Coq. In: The 9th Coq Workshop (2018). https://easychair.org/smart-slide/slide/n3pK

Bartle, R.G.: A Modern Theory of Integration, Volume 32 of Graduate Studies in Mathematics. American Mathematical Society, Providence (2001). https://doi.org/10.1090/gsm/032 CrossRef

Bertot, Y., Gonthier, G., Biha, S.O., Pasca, I.: Canonical big operators. In: Mohamed, O.A., Muñoz, C., Tahar, S. (eds.) Proceedings of the 21st International Conference on Theorem Proving in Higher Order Logics (TPHOL 2008), Volume 5170 of Lecture Notes in Computer Science, pp. 86–101. Springer, Berlin (2008). https://doi.org/10.1007/978-3-540-71067-7_11

Billingsley, P.: Probability and Measure. Wiley Series in Probability and Mathematical Statistics, 3rd edn. Wiley, New York (1995) MATH

Bishop, E.: Foundations of Constructive Analysis. McGraw-Hill Book Co., New York–Toronto–London (1967) MATH

Bishop, E., Cheng, H.: Constructive Measure Theory. Number 116 in Memoirs of the American Mathematical Society. American Mathematical Society, Providence (1972)

Bochner, S.: Integration von funktionen, deren werte die elemente eines vektorraumes sind. Fundam. Math. 20, 262–276 (1933). ( In German) CrossRef

10.

Boldo, S., Melquiond, G.: Flocq: a unified library for proving floating-point algorithms in Coq. In: Proceedings of the IEEE 20th Symposium on Computer Arithmetic (ARITH-20), pp. 243–252. IEEE (2011). https://doi.org/10.1109/ARITH17396.2011

11.

Boldo, S., Clément, F., Filliâtre, J.-C., Mayero, M., Melquiond, G., Weis, P.: Wave equation numerical resolution: a comprehensive mechanized proof of a C program. J. Autom. Reason. 50(4), 423–456 (2013). https://hal.inria.fr/hal-00649240/

12.

Boldo, S., Clément, F., Filliâtre, J.-C., Mayero, M., Melquiond, G., Weis, P.: Trusting computations: a mechanized proof from partial differential equations to actual program. Comput. Math. Appl. 68(3), 325–352 (2014). https://hal.inria.fr/hal-00769201/

13.

Boldo, S., Lelay, C., Melquiond, G.: Coquelicot: a user-friendly library of real analysis for Coq. Math. Comput. Sci. 9(1), 41–62 (2015). https://hal.inria.fr/hal-00860648/

14.

Boldo, S., Lelay, C., Melquiond, G.: Formalization of real analysis: a survey of proof assistants and libraries. Math. Struct. Comput. Sci. 26(7), 1196–1233 (2016). https://hal.inria.fr/hal-00806920/

15.

Boldo, S., Clément, F., Faissole, F., Martin, V., Mayero, M.: A Coq formal proof of the Lax–Milgram theorem. In: Proceedings of the 6th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2017), pp. 79–89. Association for Computing Machinery, New York (2017). https://hal.inria.fr/hal-01391578/

16.

Bourbaki, N.: Éléments de mathématiques. Livre VI : Intégration. Chapitres 1à 4, 2nd edn. Hermann, Paris (1965). (In French)

17.

Bourbaki, N.: Éléments de mathématiques. Livre III : Topologie générale. Chapitres 1 à 4, 2nd edn. Hermann, Paris (1971). (In French)

18.

Brezis, H.: Analyse fonctionnelle—Théorie et applications. Collection Mathématiques Appliquées pour la Maîtrise. Masson, Paris (1983). ( In French)

19.

Burk, F.E.: A Garden of Integrals, Volume 31 of The Dolciani Mathematical Expositions. Mathematical Association of America, Washington (2007) CrossRef

20.

Carathéodory, C.: Algebraic Theory of Measure and Integration. Chelsea Publishing Co., New York (1963) MATH

21.

Cartan, H.: Théorie des filtres. C. R. Acad. Sci. 205, 595–598 (1937). ( In French) MATH

22.

Ciarlet, P.G.: The Finite Element Method for Elliptic Problems, Volume 40 of Classics in Applied Mathematics. Society for Industrial and Applied Mathematics (SIAM), Philadelphia (2002). https://doi.org/10.1137/1.9780898719208. Reprint of the 1978 original (North-Holland, Amsterdam)

23.

Clément, F., Martin, V.: Lebesgue integration. Detailed proofs to be formalized in Coq. Research Report RR-9386, Inria, Paris, Jan 2021. https://hal.inria.fr/hal-03105815v2. Version 2

24.

Cohn, D.L.: Measure Theory. Birkhäuser Advanced Texts: Basler Lehrbücher, 2nd edn. Birkhäuser/Springer, New York (2013). https://doi.org/10.1007/978-1-4614-6956-8 CrossRef

25.

Coq-ref. The Coq reference manual. https://coq.inria.fr/refman/

26.

Daniell, P.J.: A general form of integral. Ann. Math. (2) 19(4), 279–294 (1918). https://doi.org/10.2307/1967495 MathSciNetCrossRefMATH

27.

de Moura, L., Kong, S., Avigad, J., van Doorn, F., von Raumer, J.: The Lean theorem prover (system description). In: Felty, A.P., Middeldorp, A. (eds.) Proceedings of the 25th International Conference on Automated Deduction (CADE 2015), Volume 9195 of Lecture Notes in Computer Science, pp. 378–388. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21401-6_26

28.

Dieudonné, J.: Éléments d’analyse. Chapitres XII à XV. Cahiers Scientifiques, Fasc. XXXI. Gauthier-Villars, Paris, Tome II (1968). ( In French)

29.

Durrett, R.: Probability—Theory and Examples, Volume 49 of Cambridge Series in Statistical and Probabilistic Mathematics, 5th edn. Cambridge University Press, Cambridge (2019). https://doi.org/10.1017/9781108591034 CrossRef

30.

Endou, N.: Fubini’s theorem. Formaliz. Math. 27(1), 67–74 (2019). https://doi.org/10.2478/forma-2019-0007

31.

Endou, N., Narita, K., Shidama, Y.: Lebesgue integral of simple valued function in Mizar. Formaliz. Math. 13(1), 67–71 (2005). https://fm.mizar.org/2005-13/pdf13-1/mesfunc3.pdf

32.

Endou, N., Narita, K., Shidama, Y.: Fatou’s lemma and the Lebesgue’s convergence theorem. Formaliz. Math. 16(4), 305–309 (2008). https://doi.org/10.2478/v10037-008-0037-8 CrossRef

33.

Ern, A., Guermond, J.-L.: Theory and Practice of Finite Elements, Volume 159 of Applied Mathematical Sciences. Springer, New York (2004). https://doi.org/10.1007/978-1-4757-4355-5 CrossRefMATH

34.

Faissole, F.: Formalization and closedness of finite dimensional subspaces. In: Proceedings of the 19th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC 2017), pp. 121–128. IEEE (2017)

35.

Feller, W.: An Introduction to Probability Theory and Its Applications, vol. I, 3rd edn. Wiley, New York–London–Sydney (1968) MATH

36.

Folland, G.B.: Real Analysis—Modern Techniques and Their Applications. Pure and Applied Mathematics (New York), 2nd edn. Wiley, New York (1999) MATH

37.

Gallouët, T., Herbin, R.: Mesure, intégration, probabilités. Ellipses Edition Marketing (2013). https://hal.archives-ouvertes.fr/hal-01283567/. (In French)

38.

Ghosal, S., van der Vaart, A.: Fundamentals of Nonparametric Bayesian Inference, Volume 44 of Cambridge Series in Statistical and Probabilistic Mathematics. Cambridge University Press, Cambridge (2017). https://doi.org/10.1017/9781139029834 CrossRef

39.

Gill, T.L., Zachary, W.W.: Functional Analysis and the Feynman Operator Calculus. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-27595-6 CrossRefMATH

40.

Gostiaux, B.: Cours de mathématiques spéciales—2. Topologie, analyse réelle. Mathématiques. Presses Universitaires de France, Paris (1993). (In French)

41.

Guan, Y., Zhang, J., Shi, Z., Wang, Y., Li, Y.: Formalization of continuous Fourier transform in verifying applications for dependable cyber-physical systems. J. Syst. Archit. 106, 101707 (2020). https://doi.org/10.1016/j.sysarc.2020.101707 CrossRef

42.

Henstock, R.: Theory of Integration. Buttherworths, London (1963) MATH

43.

Hölzl, J., Heller, A.: Three chapters of measure theory in Isabelle/HOL. In: van Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) Proceedings of the 2nd International Conference on Interactive Theorem Proving (ITP 2011), Volume 6898 of Lecture Notes in Computer Science, pp. 135–151. Springer, Berlin (2011). https://doi.org/10.1007/978-3-642-22863-6_12

44.

Immler, F.: Formally verified computation of enclosures of solutions of ordinary differential equations. In: Badger, J.M., Rozier, K.Y. (eds.) Proceedings of the 6th International Symposium NASA Formal Methods (NFM 2014), Volume 8430 of Lecture Notes in Computer Science, pp. 113–127. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-06200-6_9

45.

Immler, F., Hölzl, J.: Numerical analysis of ordinary differential equations in Isabelle/HOL. In: Beringer, L., Felty, A.P. (eds.) Proceedings of the 3rd International Conference on Interactive Theorem Proving (ITP 2012), Volume 7406 of Lecture Notes in Computer Science, pp. 377–392. Springer, Berlin (2012). https://doi.org/10.1007/978-3-642-32347-8_26

46.

Immler, F., Traut, C.: The flow of ODEs. In: Blanchette, C.J., Merz, S. (eds.) Proceedings of the 7th International Conference on Interactive Theorem Proving (ITP 2016), Volume 9807 of Lecture Notes in Computer Science, pp. 184–199. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-43144-4_12

47.

Kurzweil, J.: Generalized ordinary differential equations and continuous dependence on a parameter. Czechoslov. Math. J. 7(3), 418–449 (1957). https://doi.org/10.21136/CMJ.1957.100258 MathSciNetCrossRefMATH

48.

Lebesgue, H.L.: Leçons sur l’intégration et la recherche des fonctions primitives professées au Collège de France. Cambridge Library Collection. Cambridge University Press, Cambridge (2009). https://doi.org/10.1017/CBO9780511701825. Reprint of the 1904 original [Gauthier-Villars, Paris]. (In French)

49.

Lelay, C.: Repenser la bibliothèque réelle de Coq : vers une formalisation de l’analyse classique mieux adaptée. Thèse de doctorat, Université Paris-Sud, June (2015). https://tel.archives-ouvertes.fr/tel-01228517/. (In French)

50.

Lelay, C.: How to express convergence for analysis in Coq. In: The 7th Coq Workshop, June 2015. https://hal.archives-ouvertes.fr/hal-01169321/

51.

Maisonneuve, F.: Mathématiques 2: Intégration, transformations, int’egrales et applications—Cours et exercices. Presses de l’École des Mines (2014). (In French)

52.

Makarov, E., Spitters, B.: The Picard algorithm for ordinary differential equations in Coq. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) Proceedings of the 4th International Conference on Interactive Theorem Proving (ITP 2013), Volume 7998 of Lecture Notes in Computer Science, pp. 463–468. Springer, Berlin (2013). https://doi.org/10.1007/978-3-642-39634-2_34

53.

Matuszewski, R. (ed.): Formalized Mathematics. Sciendo, Poland. https://fm.mizar.org/

54.

Mayero, M.: Formalisation et automatisation de preuves en analyses réelle et numérique. Thèse de doctorat, Université Paris VI, December 2001. http://www-lipn.univ-paris13.fr/~mayero/publis/these-mayero.ps.gz. (In French)

55.

Mhamdi, T., Hasan, O., Tahar, S.: On the formalization of the lebesgue integration theory in HOL. In: Kaufmann, M., Paulson, L.C. (eds.) Proceedings of the 1st International Conference on Interactive Theorem Proving (ITP 2010), Volume 6172 of Lecture Notes in Computer Science, pp. 387–402. Springer, Berlin (2010). https://doi.org/10.1007/978-3-642-14052-5_27

56.

Mikusiński, J.: The Bochner Integral. Academic Press, New York–San Francisco (1978) CrossRef

57.

Musial, P., Tulone, F.: Dual of the class of HK \(_r\) integrable functions. Minimax Theory Appl. 4(1), 151–160 (2019) MathSciNetMATH

58.

Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL—A Proof Assistant for Higher-Order Logic, Volume 2283 of Lecture Notes in Computer Science. Springer, Berlin (2002). https://doi.org/10.1007/3-540-45949-9 CrossRefMATH

59.

Owre, S., Rushby, J.M., Shankar, N.: PVS: a prototype verification system. In: Kapur, D. (ed.) Proceedings of the 11th International Conference on Automated Deduction (CADE 1992), Volume 607 of Lecture Notes in Computer Science, pp. 748–752. Springer, Berlin (1992). https://doi.org/10.1007/3-540-55602-8_217

60.

Owre, S., Shankar, N., Rushby, J.M., Stringer-Calvert, D.W.J.: PVS system guide. In: SRI International, Computer Science Laboratory, Menlo Park, CA, August 2020. http://pvs.csl.sri.com/doc/pvs-system-guide.pdf. Version 7.1 [1st version in 1999]

61.

Quarteroni, A., Valli, A.: Numerical Approximation of Partial Differential Equations. Springer Series in Computational Mathematics, vol. 23. Springer, Berlin (1994) CrossRef

62.

Rudin, W.: Real and Complex Analysis, 3rd edn. McGraw-Hill Book Co., New York (1987) MATH

63.

Schwartz, L.: Théorie des distributions, 2nd edn. Hermann, Paris (1966). 1st edition in 1950–1951. (In French)

64.

Semeria, V.: Nombres réels dans Coq. In: Dargaye, Z., Regis-Gianas, Y. (eds.) Actes des 31es Journées Francophones des Langages Applicatifs (JFLA), pp. 104–111. IRIF (2020). https://hal.inria.fr/hal-02427360/. (In French)

65.

Tekriwal, M., Duraisamy, K., Jeannin, J.-B.: A formal proof of the Lax equivalence theorem for finite difference schemes. In: 13th International Symposium on NASA Formal Methods (NFM 2021) (2021). (To appear)

66.

The mathlib Community. The Lean mathematical library. In: Blanchette, J., Hritcu, C. (eds.) Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020), pp. 367–381. ACM (2020). https://doi.org/10.1145/3372885.3373824

67.

Tsybakov, A.B.: Introduction to Nonparametric Estimation. Springer Series in Statistics. Springer, New York (2009). https://doi.org/10.1007/b13794. Revised and extended from the 2004 French original [Springer, Berlin], Zaiats, V. (Trans.)

68.

Weil, A.: Sur les espaces à structure uniforme et sur la topologie générale. Hermann, Paris (1937). ( In French)

69.

Yosida, K.: Functional Analysis. Classics in Mathematics. Springer, Berlin (1995). https://doi.org/10.1007/978-3-642-61859-8. Reprint of the 6th (1980) edition (Springer, Berlin)

70.

Zienkiewicz, O.C., Taylor, R.L., Zhu, J.Z.: The Finite Element Method: Its Basis and Fundamentals, 7th edn. Elsevier/Butterworth Heinemann, Amsterdam (2013). https://doi.org/10.1016/B978-1-85617-633-0.00001-0 CrossRefMATH

Titel: A Coq Formalization of Lebesgue Integration of Nonnegative Functions
verfasst von: Sylvie Boldo
François Clément
Florian Faissole
Vincent Martin
Micaela Mayero
Publikationsdatum: 23.11.2021
Verlag: Springer Netherlands
Erschienen in: Journal of Automated Reasoning / Ausgabe 2/2022
Print ISSN: 0168-7433
Elektronische ISSN: 1573-0670
DOI: https://doi.org/10.1007/s10817-021-09612-0

Springer Professional

Tipp

Weitere Artikel dieser Ausgabe durch Wischen aufrufen

A Coq Formalization of Lebesgue Integration of Nonnegative Functions

Abstract

Sie möchten Zugang zu diesem Inhalt erhalten? Dann informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Springer Professional "Technik"

Premium Partner

Springer Professional

Tipp

Weitere Artikel dieser Ausgabe durch Wischen aufrufen

Abstract

Bitte loggen Sie sich ein, um Zugang zu diesem Inhalt zu erhalten

Sie möchten Zugang zu diesem Inhalt erhalten? Dann informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Springer Professional "Technik"

Premium Partner