{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,6,23]],"date-time":"2024-06-23T00:12:38Z","timestamp":1719101558730},"reference-count":34,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2024,6,1]],"date-time":"2024-06-01T00:00:00Z","timestamp":1717200000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,6,1]],"date-time":"2024-06-01T00:00:00Z","timestamp":1717200000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2024,6]]},"DOI":"10.1007\/s10817-024-09696-4","type":"journal-article","created":{"date-parts":[[2024,6,4]],"date-time":"2024-06-04T09:44:12Z","timestamp":1717494252000},"update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Formalized\u00a0Functional\u00a0Analysis\u00a0with\u00a0Semilinear\u00a0Maps"],"prefix":"10.1007","volume":"68","author":[{"given":"Fr\u00e9d\u00e9ric","family":"Dupuis","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Robert Y.","family":"Lewis","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Heather","family":"Macbeth","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,6,4]]},"reference":[{"key":"9696_CR1","doi-asserted-by":"publisher","unstructured":"Affeldt, R., Cohen, C., Kerjean, M., Mahboubi, A., Rouhling, D., Sakaguchi, K.: Competing inheritance paths in dependent type theory: a case study in functional analysis. In: Peltier, N., Sofronie-Stokkermans, V. (eds.) Automated Reasoning\u201410th International Joint Conference, IJCAR 2020, Paris, France, July 1-4, 2020, Proceedings, Part II. Lecture Notes in Computer Science, vol. 12167, pp. 3\u201320. Springer, Berlin (2020). https:\/\/doi.org\/10.1007\/978-3-030-51054-1_1","DOI":"10.1007\/978-3-030-51054-1_1"},{"issue":"1","key":"9696_CR2","doi-asserted-by":"publisher","first-page":"43","DOI":"10.6092\/issn.1972-5787\/8124","volume":"11","author":"R Affeldt","year":"2018","unstructured":"Affeldt, R., Cohen, C., Rouhling, D.: Formalization techniques for asymptotic reasoning in classical analysis. J. Formaliz. Reason. 11(1), 43\u201376 (2018). https:\/\/doi.org\/10.6092\/issn.1972-5787\/8124","journal-title":"J. Formaliz. Reason."},{"key":"9696_CR3","doi-asserted-by":"publisher","unstructured":"Afshar, S.K., Aravantinos, V., Hasan, O., Tahar, S.: Formalization of complex vectors in higher-order logic. In: Watt, S.M., Davenport, J.H., Sexton, A.P., Sojka, P., Urban, J. (eds.) Intelligent Computer Mathematics - International Conference, CICM 2014, Coimbra, Portugal, July 7-11, 2014. Proceedings. Lecture Notes in Computer Science, vol. 8543, pp. 123\u2013137. Springer, Berlin (2014). https:\/\/doi.org\/10.1007\/978-3-319-08434-3_10","DOI":"10.1007\/978-3-319-08434-3_10"},{"key":"9696_CR4","doi-asserted-by":"publisher","unstructured":"Aransay, J., Divas\u00f3n, J.: Generalizing a mathematical analysis library in Isabelle\/HOL. In: Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NASA Formal Methods\u20147th International Symposium, NFM 2015, Pasadena, CA, USA, April 27-29, 2015, Proceedings. Lecture Notes in Computer Science, vol. 9058, pp. 415\u2013421. Springer, Berlin (2015). https:\/\/doi.org\/10.1007\/978-3-319-17524-9_30","DOI":"10.1007\/978-3-319-17524-9_30"},{"issue":"4","key":"9696_CR5","doi-asserted-by":"publisher","first-page":"509","DOI":"10.1007\/s10817-016-9379-z","volume":"58","author":"J Aransay","year":"2017","unstructured":"Aransay, J., Divas\u00f3n, J.: A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem. J. Autom. Reason. 58(4), 509\u2013535 (2017). https:\/\/doi.org\/10.1007\/s10817-016-9379-z","journal-title":"J. Autom. Reason."},{"key":"9696_CR6","unstructured":"Baanen, A.: Use and abuse of instance parameters in the Lean mathematical library. In: Andronick, J., Moura, L. (eds.) 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs). Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany (2022)"},{"key":"9696_CR7","doi-asserted-by":"publisher","unstructured":"Boldo, S., Cl\u00e9ment, F., Faissole, F., Martin, V., Mayero, M.: A Coq formal proof of the Lax\u2013Milgram theorem. In: Bertot, Y., Vafeiadis, V. (eds.) Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, Paris, France, January 16-17, 2017, pp. 79\u201389. ACM (2017). https:\/\/doi.org\/10.1145\/3018610.3018625","DOI":"10.1145\/3018610.3018625"},{"issue":"1","key":"9696_CR8","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/s11786-014-0181-1","volume":"9","author":"S Boldo","year":"2015","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:\/\/doi.org\/10.1007\/s11786-014-0181-1","journal-title":"Math. Comput. Sci."},{"issue":"5","key":"9696_CR9","doi-asserted-by":"publisher","first-page":"691","DOI":"10.1007\/s10817-020-09584-7","volume":"65","author":"A Bordg","year":"2021","unstructured":"Bordg, A., Lachnitt, H., He, Y.: Certified quantum computation in Isabelle\/HOL. J. Autom. Reason. 65(5), 691\u2013709 (2021). https:\/\/doi.org\/10.1007\/s10817-020-09584-7","journal-title":"J. Autom. Reason."},{"key":"9696_CR10","doi-asserted-by":"publisher","unstructured":"Buzzard, K., Commelin, J., Massot, P.: Formalising perfectoid spaces. In: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs. CPP 2020, pp. 299\u2013312. Association for Computing Machinery, New York, NY, USA (2020). https:\/\/doi.org\/10.1145\/3372885.3373830","DOI":"10.1145\/3372885.3373830"},{"key":"9696_CR11","unstructured":"Caballero, J.M.R., Unruh, D.: Complex Bounded Operators. Archive of Formal Proofs (2021). https:\/\/isa-afp.org\/entries\/Complex_Bounded_Operators.html. Formal proof development"},{"key":"9696_CR12","doi-asserted-by":"publisher","unstructured":"Commelin, J., Lewis, R.Y.: Formalizing the ring of Witt vectors. In: Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs. CPP 2021, pp. 264\u2013277. Association for Computing Machinery, New York, NY, USA (2021). https:\/\/doi.org\/10.1145\/3437992.3439919","DOI":"10.1145\/3437992.3439919"},{"key":"9696_CR13","series-title":"Lecture Notes in Mathematics","volume-title":"Lectures on p-Divisible Groups","author":"M Demazure","year":"2006","unstructured":"Demazure, M.: Lectures on p-Divisible Groups. Lecture Notes in Mathematics, Springer, Berlin (2006)"},{"key":"9696_CR14","doi-asserted-by":"publisher","unstructured":"Doorn, F.: Formalized Haar Measure. In: Cohen, L., Kaliszyk, C. (eds.) 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), vol. 193, pp. 18\u201311817. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2021). https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2021.18. https:\/\/drops.dagstuhl.de\/opus\/volltexte\/2021\/13913","DOI":"10.4230\/LIPIcs.ITP.2021.18"},{"key":"9696_CR15","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1007\/978-3-030-53518-6_16","volume-title":"Intell. Comput. Math.","author":"F Doorn","year":"2020","unstructured":"Doorn, F., Ebner, G., Lewis, R.Y.: Maintaining a library of formal mathematics. In: Benzm\u00fcller, C., Miller, B. (eds.) Intell. Comput. Math., pp. 251\u2013267. Springer, Cham (2020)"},{"key":"9696_CR16","doi-asserted-by":"publisher","unstructured":"Dupuis, F., Lewis, R.Y., Macbeth, H.: Formalized functional analysis with semilinear maps. In: Andronick, J., Moura, L. (eds.) 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), vol. 237, pp. 10\u201311019. Schloss Dagstuhl\u2014Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2022). https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2022.10 . https:\/\/drops.dagstuhl.de\/opus\/volltexte\/2022\/16719","DOI":"10.4230\/LIPIcs.ITP.2022.10"},{"key":"9696_CR17","unstructured":"Gou\u00ebzel, S.: Lp Spaces. Archive of Formal Proofs (2016). https:\/\/isa-afp.org\/entries\/Lp.html. Formal proof development"},{"issue":"2","key":"9696_CR18","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/s10817-012-9250-9","volume":"50","author":"J Harrison","year":"2013","unstructured":"Harrison, J.: The HOL Light theory of Euclidean space. J. Autom. Reason. 50(2), 173\u2013190 (2013). https:\/\/doi.org\/10.1007\/s10817-012-9250-9","journal-title":"J. Autom. Reason."},{"key":"9696_CR19","doi-asserted-by":"publisher","unstructured":"Hazewinkel, M.: Witt Vectors. Part 1. Handbook of Algebra, pp. 319\u2013472 (2009). https:\/\/doi.org\/10.1016\/s1570-7954(08)00207-6","DOI":"10.1016\/s1570-7954(08)00207-6"},{"key":"9696_CR20","doi-asserted-by":"publisher","unstructured":"H\u00f6lzl, J., Immler, F., Huffman, B.: Type classes and filters for mathematical analysis in Isabelle\/HOL. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) Interactive Theorem Proving\u20144th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings. Lecture Notes in Computer Science, vol. 7998, pp. 279\u2013294. Springer, Berlin (2013). https:\/\/doi.org\/10.1007\/978-3-642-39634-2_21","DOI":"10.1007\/978-3-642-39634-2_21"},{"key":"9696_CR21","unstructured":"Kudryashov, Y.: Formalizing the divergence theorem and the Cauchy integral formula in Lean. In: Andronick, J., Moura, L. (eds.) 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs). Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany (2022)"},{"issue":"1","key":"9696_CR22","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/s10817-018-9461-9","volume":"63","author":"P Lammich","year":"2019","unstructured":"Lammich, P., Lochbihler, A.: Automatic refinement to efficient data structures: a comparison of two approaches. J. Autom. Reason. 63(1), 53\u201394 (2019). https:\/\/doi.org\/10.1007\/s10817-018-9461-9","journal-title":"J. Autom. Reason."},{"key":"9696_CR23","unstructured":"Lurie, J.: Lecture Notes on the Fargues\u2013Fontaine Curve. Lecture 26: Isocrystals (2018). https:\/\/www.math.ias.edu\/205notes\/Lecture26-Isocrystals.pdf"},{"key":"9696_CR24","doi-asserted-by":"publisher","unstructured":"Mahboubi, A., Tassi, E.: Mathematical Components. Zenodo (2020). https:\/\/doi.org\/10.5281\/zenodo.4282710","DOI":"10.5281\/zenodo.4282710"},{"key":"9696_CR25","doi-asserted-by":"publisher","unstructured":"Mahmoud, M.Y., Aravantinos, V., Tahar, S.: Formalization of infinite dimension linear spaces with application to quantum theory. In: Brat, G., Rungta, N., Venet, A. (eds.) NASA Formal Methods, 5th International Symposium, NFM 2013, Moffett Field, CA, USA, May 14-16, 2013. Proceedings. Lecture Notes in Computer Science, vol. 7871, pp. 413\u2013427. Springer, Berlin (2013). https:\/\/doi.org\/10.1007\/978-3-642-38088-4_28","DOI":"10.1007\/978-3-642-38088-4_28"},{"key":"9696_CR26","doi-asserted-by":"crossref","unstructured":"Manin, J.I.: Theory of commutative formal groups over fields of finite characteristic. Uspehi Mat. Nauk 18(6(114)), 3\u201390 (1963)","DOI":"10.1070\/RM1963v018n06ABEH001142"},{"key":"9696_CR27","first-page":"378","volume-title":"CADE-25","author":"L Moura","year":"2015","unstructured":"Moura, L., Kong, S., Avigad, J., Doorn, F., Raumer, J.: The Lean Theorem Prover (system description). In: Felty, A.P., Middeldorp, A. (eds.) CADE-25, pp. 378\u2013388. Springer, Cham (2015)"},{"issue":"3","key":"9696_CR28","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1515\/forma-2015-0020","volume":"23","author":"K Narita","year":"2015","unstructured":"Narita, K., Endou, N., Shidama, Y.: The orthogonal projection and the Riesz representation theorem. Formaliz. Math. 23(3), 243\u2013252 (2015). https:\/\/doi.org\/10.1515\/forma-2015-0020","journal-title":"Formaliz. Math."},{"key":"9696_CR29","unstructured":"Nash, O.: A Formalisation of Gallagher\u2019s Ergodic Theorem (2023)"},{"key":"9696_CR30","unstructured":"Paulson, L.C.: Fourier Series. Archive of Formal Proofs (2019). https:\/\/isa-afp.org\/entries\/Fourier.html. Formal proof development"},{"issue":"4","key":"9696_CR31","doi-asserted-by":"publisher","first-page":"795","DOI":"10.1017\/S0960129511000119","volume":"21","author":"B Spitters","year":"2011","unstructured":"Spitters, B., Weegen, E.: Type classes for mathematics in type theory. Math. Struct. Comput. Sci. 21(4), 795\u2013825 (2011). https:\/\/doi.org\/10.1017\/S0960129511000119","journal-title":"Math. Struct. Comput. Sci."},{"key":"9696_CR32","doi-asserted-by":"publisher","unstructured":"The mathlib Community: The Lean mathematical library. In: CPP, pp. 367\u2013381. ACM, New York, NY, USA (2020). https:\/\/doi.org\/10.1145\/3372885.3373824","DOI":"10.1145\/3372885.3373824"},{"key":"9696_CR33","unstructured":"Wieser, E.: Scalar actions in Lean\u2019s mathlib. CoRR abs\/2108.10700 (2021) arxiv:2108.10700"},{"issue":"4","key":"9696_CR34","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1145\/362575.362577","volume":"14","author":"N Wirth","year":"1971","unstructured":"Wirth, N.: Program development by stepwise refinement. Commun. ACM 14(4), 221\u2013227 (1971). https:\/\/doi.org\/10.1145\/362575.362577","journal-title":"Commun. ACM"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-024-09696-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-024-09696-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-024-09696-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,6,22]],"date-time":"2024-06-22T07:07:22Z","timestamp":1719040042000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-024-09696-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,6]]},"references-count":34,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2024,6]]}},"alternative-id":["9696"],"URL":"https:\/\/doi.org\/10.1007\/s10817-024-09696-4","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,6]]},"assertion":[{"value":"25 April 2023","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"25 March 2024","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"4 June 2024","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors declare no competing interests.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Competing interest"}}],"article-number":"10"}}