{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,16]],"date-time":"2025-06-16T16:05:23Z","timestamp":1750089923096,"version":"3.37.3"},"reference-count":70,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2021,11,23]],"date-time":"2021-11-23T00:00:00Z","timestamp":1637625600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,11,23]],"date-time":"2021-11-23T00:00:00Z","timestamp":1637625600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100006103","name":"Domaine d\u2019Int\u00e9r\u00eat Majeur Logiciels et Syst\u00e8mes Complexes","doi-asserted-by":"publisher","award":["MILC"],"award-info":[{"award-number":["MILC"]}],"id":[{"id":"10.13039\/501100006103","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Digicosme","award":["ANR-11-LABEX-0045-DIGICOSME"],"award-info":[{"award-number":["ANR-11-LABEX-0045-DIGICOSME"]}]},{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["ERC Synergy EMC2 810367"],"award-info":[{"award-number":["ERC Synergy EMC2 810367"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2022,5]]},"DOI":"10.1007\/s10817-021-09612-0","type":"journal-article","created":{"date-parts":[[2021,11,23]],"date-time":"2021-11-23T05:02:42Z","timestamp":1637643762000},"page":"175-213","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["A Coq Formalization of Lebesgue Integration of Nonnegative Functions"],"prefix":"10.1007","volume":"66","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1970-3019","authenticated-orcid":false,"given":"Sylvie","family":"Boldo","sequence":"first","affiliation":[]},{"given":"Fran\u00e7ois","family":"Cl\u00e9ment","sequence":"additional","affiliation":[]},{"given":"Florian","family":"Faissole","sequence":"additional","affiliation":[]},{"given":"Vincent","family":"Martin","sequence":"additional","affiliation":[]},{"given":"Micaela","family":"Mayero","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,11,23]]},"reference":[{"key":"9612_CR1","doi-asserted-by":"crossref","unstructured":"Abdulaziz, M., Paulson, L.C.: An Isabelle\/HOL formalisation of Green\u2019s 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\u201319. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-43144-4_1","DOI":"10.1007\/978-3-319-43144-4_1"},{"key":"9612_CR2","volume-title":"Sobolev Spaces. Pure and Applied Mathematics","author":"RA Adams","year":"1975","unstructured":"Adams, R.A.: Sobolev Spaces. Pure and Applied Mathematics, vol. 65. Academic Press, New York\u2013San Francisco\u2013London (1975)"},{"key":"9612_CR3","unstructured":"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"},{"key":"9612_CR4","doi-asserted-by":"publisher","DOI":"10.1090\/gsm\/032","volume-title":"A Modern Theory of Integration, Volume 32 of Graduate Studies in Mathematics","author":"RG Bartle","year":"2001","unstructured":"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"},{"key":"9612_CR5","doi-asserted-by":"crossref","unstructured":"Bertot, Y., Gonthier, G., Biha, S.O., Pasca, I.: Canonical big operators. In: Mohamed, O.A., Mu\u00f1oz, 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\u2013101. Springer, Berlin (2008). https:\/\/doi.org\/10.1007\/978-3-540-71067-7_11","DOI":"10.1007\/978-3-540-71067-7_11"},{"key":"9612_CR6","volume-title":"Probability and Measure. Wiley Series in Probability and Mathematical Statistics","author":"P Billingsley","year":"1995","unstructured":"Billingsley, P.: Probability and Measure. Wiley Series in Probability and Mathematical Statistics, 3rd edn. Wiley, New York (1995)","edition":"3"},{"key":"9612_CR7","volume-title":"Foundations of Constructive Analysis","author":"E Bishop","year":"1967","unstructured":"Bishop, E.: Foundations of Constructive Analysis. McGraw-Hill Book Co., New York\u2013Toronto\u2013London (1967)"},{"key":"9612_CR8","volume-title":"Constructive Measure Theory. Number 116 in Memoirs of the American Mathematical Society","author":"E Bishop","year":"1972","unstructured":"Bishop, E., Cheng, H.: Constructive Measure Theory. Number 116 in Memoirs of the American Mathematical Society. American Mathematical Society, Providence (1972)"},{"key":"9612_CR9","doi-asserted-by":"publisher","first-page":"262","DOI":"10.4064\/fm-20-1-262-176","volume":"20","author":"S Bochner","year":"1933","unstructured":"Bochner, S.: Integration von funktionen, deren werte die elemente eines vektorraumes sind. Fundam. Math. 20, 262\u2013276 (1933). (In German)","journal-title":"Fundam. Math."},{"key":"9612_CR10","doi-asserted-by":"crossref","unstructured":"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\u2013252. IEEE (2011). https:\/\/doi.org\/10.1109\/ARITH17396.2011","DOI":"10.1109\/ARITH.2011.40"},{"key":"9612_CR11","doi-asserted-by":"crossref","unstructured":"Boldo, S., Cl\u00e9ment, F., Filli\u00e2tre, 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\u2013456 (2013). https:\/\/hal.inria.fr\/hal-00649240\/","DOI":"10.1007\/s10817-012-9255-4"},{"key":"9612_CR12","doi-asserted-by":"crossref","unstructured":"Boldo, S., Cl\u00e9ment, F., Filli\u00e2tre, 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\u2013352 (2014). https:\/\/hal.inria.fr\/hal-00769201\/","DOI":"10.1016\/j.camwa.2014.06.004"},{"key":"9612_CR13","doi-asserted-by":"crossref","unstructured":"Boldo, S., Lelay, C., Melquiond, G.: Coquelicot: a user-friendly library of real analysis for Coq. Math. Comput. Sci. 9(1), 41\u201362 (2015). https:\/\/hal.inria.fr\/hal-00860648\/","DOI":"10.1007\/s11786-014-0181-1"},{"key":"9612_CR14","doi-asserted-by":"crossref","unstructured":"Boldo, S., Lelay, C., Melquiond, G.: Formalization of real analysis: a survey of proof assistants and libraries. Math. Struct. Comput. Sci. 26(7), 1196\u20131233 (2016). https:\/\/hal.inria.fr\/hal-00806920\/","DOI":"10.1017\/S0960129514000437"},{"key":"9612_CR15","doi-asserted-by":"crossref","unstructured":"Boldo, S., Cl\u00e9ment, F., Faissole, F., Martin, V., Mayero, M.: A Coq formal proof of the Lax\u2013Milgram theorem. In: Proceedings of the 6th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2017), pp. 79\u201389. Association for Computing Machinery, New York (2017). https:\/\/hal.inria.fr\/hal-01391578\/","DOI":"10.1145\/3018610.3018625"},{"key":"9612_CR16","unstructured":"Bourbaki, N.: \u00c9l\u00e9ments de math\u00e9matiques. Livre\u00a0VI\u00a0: Int\u00e9gration. Chapitres\u00a01\u00e0\u00a04, 2nd edn. Hermann, Paris (1965). (In French)"},{"key":"9612_CR17","unstructured":"Bourbaki, N.: \u00c9l\u00e9ments de math\u00e9matiques. Livre\u00a0III\u00a0: Topologie g\u00e9n\u00e9rale. Chapitres\u00a01 \u00e0\u00a04, 2nd edn. Hermann, Paris (1971). (In French)"},{"key":"9612_CR18","unstructured":"Brezis, H.: Analyse fonctionnelle\u2014Th\u00e9orie et applications. Collection Math\u00e9matiques Appliqu\u00e9es pour la Ma\u00eetrise. Masson, Paris (1983). (In French)"},{"key":"9612_CR19","doi-asserted-by":"publisher","DOI":"10.7135\/UPO9781614442097","volume-title":"A Garden of Integrals, Volume 31 of The Dolciani Mathematical Expositions","author":"FE Burk","year":"2007","unstructured":"Burk, F.E.: A Garden of Integrals, Volume 31 of The Dolciani Mathematical Expositions. Mathematical Association of America, Washington (2007)"},{"key":"9612_CR20","volume-title":"Algebraic Theory of Measure and Integration","author":"C Carath\u00e9odory","year":"1963","unstructured":"Carath\u00e9odory, C.: Algebraic Theory of Measure and Integration. Chelsea Publishing Co., New York (1963)"},{"key":"9612_CR21","first-page":"595","volume":"205","author":"H Cartan","year":"1937","unstructured":"Cartan, H.: Th\u00e9orie des filtres. C. R. Acad. Sci. 205, 595\u2013598 (1937). (In French)","journal-title":"C. R. Acad. Sci."},{"key":"9612_CR22","doi-asserted-by":"crossref","unstructured":"Ciarlet, P.G.: The Finite Element Method for Elliptic Problems, Volume\u00a040 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)","DOI":"10.1137\/1.9780898719208"},{"key":"9612_CR23","unstructured":"Cl\u00e9ment, 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"},{"key":"9612_CR24","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4614-6956-8","volume-title":"Measure Theory. Birkh\u00e4user Advanced Texts: Basler Lehrb\u00fccher","author":"DL Cohn","year":"2013","unstructured":"Cohn, D.L.: Measure Theory. Birkh\u00e4user Advanced Texts: Basler Lehrb\u00fccher, 2nd edn. Birkh\u00e4user\/Springer, New York (2013). https:\/\/doi.org\/10.1007\/978-1-4614-6956-8","edition":"2"},{"key":"9612_CR25","unstructured":"Coq-ref. The Coq reference manual. https:\/\/coq.inria.fr\/refman\/"},{"issue":"4","key":"9612_CR26","doi-asserted-by":"publisher","first-page":"279","DOI":"10.2307\/1967495","volume":"19","author":"PJ Daniell","year":"1918","unstructured":"Daniell, P.J.: A general form of integral. Ann. Math. (2) 19(4), 279\u2013294 (1918). https:\/\/doi.org\/10.2307\/1967495","journal-title":"Ann. Math. (2)"},{"key":"9612_CR27","doi-asserted-by":"crossref","unstructured":"de\u00a0Moura, 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\u2013388. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21401-6_26","DOI":"10.1007\/978-3-319-21401-6_26"},{"key":"9612_CR28","unstructured":"Dieudonn\u00e9, J.: \u00c9l\u00e9ments d\u2019analyse. Chapitres XII \u00e0 XV. Cahiers Scientifiques, Fasc. XXXI. Gauthier-Villars, Paris, Tome II (1968). (In French)"},{"key":"9612_CR29","doi-asserted-by":"publisher","DOI":"10.1017\/9781108591034","volume-title":"Probability\u2014Theory and Examples, Volume\u00a049 of Cambridge Series in Statistical and Probabilistic Mathematics","author":"R Durrett","year":"2019","unstructured":"Durrett, R.: Probability\u2014Theory and Examples, Volume\u00a049 of Cambridge Series in Statistical and Probabilistic Mathematics, 5th edn. Cambridge University Press, Cambridge (2019). https:\/\/doi.org\/10.1017\/9781108591034","edition":"5"},{"key":"9612_CR30","doi-asserted-by":"crossref","unstructured":"Endou, N.: Fubini\u2019s theorem. Formaliz. Math. 27(1), 67\u201374 (2019). https:\/\/doi.org\/10.2478\/forma-2019-0007","DOI":"10.2478\/forma-2019-0007"},{"key":"9612_CR31","unstructured":"Endou, N., Narita, K., Shidama, Y.: Lebesgue integral of simple valued function in Mizar. Formaliz. Math. 13(1), 67\u201371 (2005). https:\/\/fm.mizar.org\/2005-13\/pdf13-1\/mesfunc3.pdf"},{"issue":"4","key":"9612_CR32","doi-asserted-by":"publisher","first-page":"305","DOI":"10.2478\/v10037-008-0037-8","volume":"16","author":"N Endou","year":"2008","unstructured":"Endou, N., Narita, K., Shidama, Y.: Fatou\u2019s lemma and the Lebesgue\u2019s convergence theorem. Formaliz. Math. 16(4), 305\u2013309 (2008). https:\/\/doi.org\/10.2478\/v10037-008-0037-8","journal-title":"Formaliz. Math."},{"key":"9612_CR33","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-4355-5","volume-title":"Theory and Practice of Finite Elements, Volume 159 of Applied Mathematical Sciences","author":"A Ern","year":"2004","unstructured":"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"},{"key":"9612_CR34","doi-asserted-by":"crossref","unstructured":"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\u2013128. IEEE (2017)","DOI":"10.1109\/SYNASC.2017.00030"},{"key":"9612_CR35","volume-title":"An Introduction to Probability Theory and Its Applications","author":"W Feller","year":"1968","unstructured":"Feller, W.: An Introduction to Probability Theory and Its Applications, vol. I, 3rd edn. Wiley, New York\u2013London\u2013Sydney (1968)","edition":"3"},{"key":"9612_CR36","volume-title":"Real Analysis\u2014Modern Techniques and Their Applications. Pure and Applied Mathematics (New York)","author":"GB Folland","year":"1999","unstructured":"Folland, G.B.: Real Analysis\u2014Modern Techniques and Their Applications. Pure and Applied Mathematics (New York), 2nd edn. Wiley, New York (1999)","edition":"2"},{"key":"9612_CR37","unstructured":"Gallou\u00ebt, T., Herbin, R.: Mesure, int\u00e9gration, probabilit\u00e9s. Ellipses Edition Marketing (2013). https:\/\/hal.archives-ouvertes.fr\/hal-01283567\/. (In French)"},{"key":"9612_CR38","doi-asserted-by":"publisher","DOI":"10.1017\/9781139029834","volume-title":"Fundamentals of Nonparametric Bayesian Inference, Volume\u00a044 of Cambridge Series in Statistical and Probabilistic Mathematics","author":"S Ghosal","year":"2017","unstructured":"Ghosal, S., van der Vaart, A.: Fundamentals of Nonparametric Bayesian Inference, Volume\u00a044 of Cambridge Series in Statistical and Probabilistic Mathematics. Cambridge University Press, Cambridge (2017). https:\/\/doi.org\/10.1017\/9781139029834"},{"key":"9612_CR39","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-27595-6","volume-title":"Functional Analysis and the Feynman Operator Calculus","author":"TL Gill","year":"2016","unstructured":"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"},{"key":"9612_CR40","unstructured":"Gostiaux, B.: Cours de math\u00e9matiques sp\u00e9ciales\u20142.\u00a0Topologie, analyse r\u00e9elle. Math\u00e9matiques. Presses Universitaires de France, Paris (1993). (In French)"},{"key":"9612_CR41","doi-asserted-by":"publisher","first-page":"101707","DOI":"10.1016\/j.sysarc.2020.101707","volume":"106","author":"Y Guan","year":"2020","unstructured":"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","journal-title":"J. Syst. Archit."},{"key":"9612_CR42","volume-title":"Theory of Integration","author":"R Henstock","year":"1963","unstructured":"Henstock, R.: Theory of Integration. Buttherworths, London (1963)"},{"key":"9612_CR43","doi-asserted-by":"crossref","unstructured":"H\u00f6lzl, 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\u2013151. Springer, Berlin (2011). https:\/\/doi.org\/10.1007\/978-3-642-22863-6_12","DOI":"10.1007\/978-3-642-22863-6_12"},{"key":"9612_CR44","doi-asserted-by":"crossref","unstructured":"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\u2013127. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-06200-6_9","DOI":"10.1007\/978-3-319-06200-6_9"},{"key":"9612_CR45","doi-asserted-by":"crossref","unstructured":"Immler, F., H\u00f6lzl, 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\u2013392. Springer, Berlin (2012). https:\/\/doi.org\/10.1007\/978-3-642-32347-8_26","DOI":"10.1007\/978-3-642-32347-8_26"},{"key":"9612_CR46","doi-asserted-by":"crossref","unstructured":"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\u2013199. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-43144-4_12","DOI":"10.1007\/978-3-319-43144-4_12"},{"issue":"3","key":"9612_CR47","doi-asserted-by":"publisher","first-page":"418","DOI":"10.21136\/CMJ.1957.100258","volume":"7","author":"J Kurzweil","year":"1957","unstructured":"Kurzweil, J.: Generalized ordinary differential equations and continuous dependence on a parameter. Czechoslov. Math. J. 7(3), 418\u2013449 (1957). https:\/\/doi.org\/10.21136\/CMJ.1957.100258","journal-title":"Czechoslov. Math. J."},{"key":"9612_CR48","doi-asserted-by":"crossref","unstructured":"Lebesgue, H.L.: Le\u00e7ons sur l\u2019int\u00e9gration et la recherche des fonctions primitives profess\u00e9es au Coll\u00e8ge 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)","DOI":"10.1017\/CBO9780511701825"},{"key":"9612_CR49","unstructured":"Lelay, C.: Repenser la biblioth\u00e8que r\u00e9elle de Coq : vers une formalisation de l\u2019analyse classique mieux adapt\u00e9e. Th\u00e8se de doctorat, Universit\u00e9 Paris-Sud, June (2015). https:\/\/tel.archives-ouvertes.fr\/tel-01228517\/. (In French)"},{"key":"9612_CR50","unstructured":"Lelay, C.: How to express convergence for analysis in Coq. In: The 7th Coq Workshop, June 2015. https:\/\/hal.archives-ouvertes.fr\/hal-01169321\/"},{"key":"9612_CR51","unstructured":"Maisonneuve, F.: Math\u00e9matiques\u00a02: Int\u00e9gration, transformations, int\u2019egrales et applications\u2014Cours et exercices. Presses de l\u2019\u00c9cole des Mines (2014). (In French)"},{"key":"9612_CR52","doi-asserted-by":"crossref","unstructured":"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\u2013468. Springer, Berlin (2013). https:\/\/doi.org\/10.1007\/978-3-642-39634-2_34","DOI":"10.1007\/978-3-642-39634-2_34"},{"key":"9612_CR53","unstructured":"Matuszewski, R. (ed.): Formalized Mathematics. Sciendo, Poland. https:\/\/fm.mizar.org\/"},{"key":"9612_CR54","unstructured":"Mayero, M.: Formalisation et automatisation de preuves en analyses r\u00e9elle et num\u00e9rique. Th\u00e8se de doctorat, Universit\u00e9 Paris VI, December 2001. http:\/\/www-lipn.univ-paris13.fr\/~mayero\/publis\/these-mayero.ps.gz. (In French)"},{"key":"9612_CR55","doi-asserted-by":"crossref","unstructured":"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\u2013402. Springer, Berlin (2010). https:\/\/doi.org\/10.1007\/978-3-642-14052-5_27","DOI":"10.1007\/978-3-642-14052-5_27"},{"key":"9612_CR56","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-0348-5567-9","volume-title":"The Bochner Integral","author":"J Mikusi\u0144ski","year":"1978","unstructured":"Mikusi\u0144ski, J.: The Bochner Integral. Academic Press, New York\u2013San Francisco (1978)"},{"issue":"1","key":"9612_CR57","first-page":"151","volume":"4","author":"P Musial","year":"2019","unstructured":"Musial, P., Tulone, F.: Dual of the class of HK$$_r$$ integrable functions. Minimax Theory Appl. 4(1), 151\u2013160 (2019)","journal-title":"Minimax Theory Appl."},{"key":"9612_CR58","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL\u2014A Proof Assistant for Higher-Order Logic, Volume 2283 of Lecture Notes in Computer Science","author":"T Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL\u2014A 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"},{"key":"9612_CR59","doi-asserted-by":"crossref","unstructured":"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\u2013752. Springer, Berlin (1992). https:\/\/doi.org\/10.1007\/3-540-55602-8_217","DOI":"10.1007\/3-540-55602-8_217"},{"key":"9612_CR60","unstructured":"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]"},{"key":"9612_CR61","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-85268-1","volume-title":"Numerical Approximation of Partial Differential Equations. Springer Series in Computational Mathematics","author":"A Quarteroni","year":"1994","unstructured":"Quarteroni, A., Valli, A.: Numerical Approximation of Partial Differential Equations. Springer Series in Computational Mathematics, vol. 23. Springer, Berlin (1994)"},{"key":"9612_CR62","volume-title":"Real and Complex Analysis","author":"W Rudin","year":"1987","unstructured":"Rudin, W.: Real and Complex Analysis, 3rd edn. McGraw-Hill Book Co., New York (1987)","edition":"3"},{"key":"9612_CR63","unstructured":"Schwartz, L.: Th\u00e9orie des distributions, 2nd edn. Hermann, Paris (1966). 1st edition in 1950\u20131951. (In French)"},{"key":"9612_CR64","unstructured":"Semeria, V.: Nombres r\u00e9els dans Coq. In: Dargaye, Z., Regis-Gianas, Y. (eds.) Actes des 31es Journ\u00e9es Francophones des Langages Applicatifs (JFLA), pp. 104\u2013111. IRIF (2020). https:\/\/hal.inria.fr\/hal-02427360\/. (In French)"},{"key":"9612_CR65","doi-asserted-by":"crossref","unstructured":"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)","DOI":"10.1007\/978-3-030-76384-8_20"},{"key":"9612_CR66","doi-asserted-by":"crossref","unstructured":"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\u2013381. ACM (2020). https:\/\/doi.org\/10.1145\/3372885.3373824","DOI":"10.1145\/3372885.3373824"},{"key":"9612_CR67","doi-asserted-by":"crossref","unstructured":"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.)","DOI":"10.1007\/b13794"},{"key":"9612_CR68","unstructured":"Weil, A.: Sur les espaces \u00e0 structure uniforme et sur la topologie g\u00e9n\u00e9rale. Hermann, Paris (1937). (In French)"},{"key":"9612_CR69","doi-asserted-by":"crossref","unstructured":"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)","DOI":"10.1007\/978-3-642-61859-8"},{"key":"9612_CR70","doi-asserted-by":"publisher","DOI":"10.1016\/B978-1-85617-633-0.00001-0","volume-title":"The Finite Element Method: Its Basis and Fundamentals","author":"OC Zienkiewicz","year":"2013","unstructured":"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","edition":"7"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-021-09612-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-021-09612-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-021-09612-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,4,9]],"date-time":"2022-04-09T08:10:30Z","timestamp":1649491830000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-021-09612-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,11,23]]},"references-count":70,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2022,5]]}},"alternative-id":["9612"],"URL":"https:\/\/doi.org\/10.1007\/s10817-021-09612-0","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2021,11,23]]},"assertion":[{"value":"15 April 2021","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"9 October 2021","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"23 November 2021","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}