×

A symbolic-numeric validation algorithm for linear ODEs with Newton-Picard method. (English) Zbl 07433040

Summary: A symbolic-numeric validation algorithm is developed to compute rigorous and tight uniform error bounds for polynomial approximate solutions to linear ordinary differential equations, and in particular D-finite functions. It relies on an a posteriori validation scheme, where such an error bound is computed afterwards, independently from how the approximation was built. Contrary to Newton-Galerkin validation methods, widely used in the mathematical community of computer-assisted proofs, our algorithm does not rely on finite-dimensional truncations of differential or integral operators, but on an efficient approximation of the resolvent kernel using a Chebyshev spectral method. The result is a much better complexity of the validation process, carefully investigated throughout this article. Indeed, the approximation degree for the resolvent kernel depends linearly on the magnitude of the input equation, while the truncation order used in Newton-Galerkin may be exponential in the same quantity. Numerical experiments based on an implementation in C corroborate this complexity advantage over other a posteriori validation methods, including Newton-Galerkin.

MSC:

65G20 Algorithms with automatic result verification
65L60 Finite element, Rayleigh-Ritz, Galerkin and collocation methods for ordinary differential equations
65L70 Error bounds for numerical methods for ordinary differential equations
65Y20 Complexity and performance of numerical algorithms

Software:

gfun; Coq
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Abramowitz, M., Stegun, I.A.: Handbook of Mathematical Functions with Formulas, Graphs, and Mathematical Tables, volume 55 of National Bureau of Standards Applied Mathematics Series. Courier Corporation (1964) · Zbl 0171.38503
[2] Benoit, A.; Joldes, M.; Mezzarobba, M., Rigorous uniform approximation of D-finite functions using Chebyshev expansions, Math. Comput., 86, 305, 1303-1341 (2017) · Zbl 1361.65045 · doi:10.1090/mcom/3135
[3] Berinde, V.: Iterative Approximation of Fixed Points. Lecture Notes in Mathematics, vol. 1912. Springer, Berlin (2007) · Zbl 1165.47047
[4] Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development: Coq’Art: the Calculus of Inductive Constructions. Springer (2013) · Zbl 1069.68095
[5] Berz, M.; Makino, K., Verified integration of ODEs and flows using differential algebraic methods on high-order Taylor models, Reliable Comput., 4, 4, 361-369 (1998) · Zbl 0976.65061 · doi:10.1023/A:1024467732637
[6] Bournez, O., Graça, D.S., Pouly, A.: On the complexity of solving initial value problems. In: Proceedings of the 37th International Symposium on Symbolic and Algebraic Computation, pp. 115-121 (2012). doi:10.1145/2442829.2442849 · Zbl 1323.68312
[7] Boyd, J.P.: Chebyshev and Fourier spectral methods. Dover Publications (2001) · Zbl 0994.65128
[8] Bréhard, F.; Brisebarre, N.; Joldes, M., Validated and numerically efficient Chebyshev spectral methods for linear ordinary differential equations, ACM Trans. Math. Softw., 44, 4, 44:1-44:42 (2018) · Zbl 1484.65155 · doi:10.1145/3208103
[9] Bréhard, F., Mahboubi, A., Pous, D.: A certificate-based approach to formally verified approximations. In: 10th International Conference on Interactive Theorem Proving (ITP 2019), vol. 141, pp. 8:1-8:19 (2019). doi:10.4230/LIPIcs.ITP.2019.8 · Zbl 07649957
[10] Brisebarre, N., Joldes, M.: Chebyshev interpolation polynomial-based tools for rigorous computing. In: Proceedings of the 2010 International Symposium on Symbolic and Algebraic Computation, pp. 147-154. ACM (2010). URL: doi:10.1145/1837934.1837966 · Zbl 1321.65018
[11] Chyzak, F.: The ABC of Creative Telescoping: Algorithms, Bounds, Complexity. Memoir of accreditation to supervise research (HDR), Université d’Orsay (2014). https://tel.archives-ouvertes.fr/tel-01069831
[12] Epstein, C.; Miranker, WL; Rivlin, TJ, Ultra-arithmetic. I. Function data types, Math. Comput. Simul., 24, 1-18 (1982) · Zbl 0493.42005 · doi:10.1016/0378-4754(82)90045-3
[13] Epstein, C.; Miranker, WL; Rivlin, TJ, Ultra-arithmetic. II. Intervals of polynomials, Math. Comput. Simul., 24, 19-29 (1982) · Zbl 1402.65040 · doi:10.1016/0378-4754(82)90046-5
[14] Fox, L., Parker, I.B.: Chebyshev Polynomials in Numerical Analysis. Oxford University Press, London-New York-Toronto, Ont. (1968) · Zbl 0153.17502
[15] Gottlieb, D., Orszag, S.A.: Numerical Analysis of Spectral Methods: Theory and Applications, vol. 26. SIAM (1977) · Zbl 0412.65058
[16] Greengard, L., Spectral integration and two-point boundary value problems, SIAM J. Numer. Anal., 28, 4, 1071-1080 (1991) · Zbl 0731.65064 · doi:10.1137/0728057
[17] Hungria, A.; Lessard, J-P; Mireles James, JD, Rigorous numerics for analytic solutions of differential equations: the radii polynomial approach, Math. Comput., 85, 299, 1427-1459 (2016) · Zbl 1332.65114 · doi:10.1090/mcom/3046
[18] Jiménez-Pastor, A.; Pillwein, V.; Singer, MF, Some structural results on \(D^n\)-finite functions, Adv. Appl. Math., 117, 102027 (2020) · Zbl 1480.12006 · doi:10.1016/j.aam.2020.102027
[19] Joldes, M.: Rigorous Polynomial Approximations and Applications. PhD thesis, École normale supérieure de Lyon - Université de Lyon, Lyon, France (2011). https://tel.archives-ouvertes.fr/tel-00657843
[20] Kaucher, E., Miranker, W.L.: Validating computation in a function space. In: Reliability in computing: the role of interval methods in scientific computing, pages 403-425. Academic Press Professional, Inc. (1988). doi:10.1016/B978-0-12-505630-4.50028-6 · Zbl 0659.65058
[21] Kedem, G., A posteriori error bounds for two-point boundary value problems, SIAM J. Numer. Anal., 18, 3, 431-448 (1981) · Zbl 0469.65062 · doi:10.1137/0718028
[22] Koutschan, C.: Advanced Applications of the Holonomic Systems Approach. PhD thesis, Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria (2009). https://www3.risc.jku.at/research/combinat/software/ergosum/RISC/HolonomicFunctions.html · Zbl 1344.68301
[23] Lalescu, T.: Introduction à la Théorie des Équations Intégrales (Introduction to the Theory of Integral Equations). Hermann, Librairie Scientifique A (1911) · JFM 42.0385.11
[24] Lessard, J-P; Reinhardt, C., Rigorous numerics for nonlinear differential equations using Chebyshev series, SIAM J. Numer. Anal., 52, 1, 1-22 (2014) · Zbl 1290.65060 · doi:10.1137/13090883X
[25] Mezzarobba, M.: Autour de l’ évaluation numérique des fonctions D-finies. PhD thesis, École polytechnique (2011). URL: https://tel.archives-ouvertes.fr/pastel-00663017/
[26] Moore, R.E.: Interval Analysis. Prentice-Hall (1966) · Zbl 0176.13301
[27] Nakao, MT, Numerical verification methods for solutions of ordinary and partial differential equations, Numer. Funct. Anal. Optim., 22, 3-4, 321-356 (2001) · Zbl 1106.65315 · doi:10.1081/NFA-100105107
[28] Neumaier, A., Taylor forms—use and limits, Reliable Comput., 9, 1, 43-79 (2003) · Zbl 1071.65070 · doi:10.1023/A:1023061927787
[29] Olver, S.; Townsend, A., A fast and well-conditioned spectral method, SIAM Rev., 55, 3, 462-489 (2013) · Zbl 1273.65182 · doi:10.1137/120865458
[30] Plum, M., Computer-assisted existence proofs for two-point boundary value problems, Computing, 46, 1, 19-34 (1991) · Zbl 0782.65107 · doi:10.1007/BF02239009
[31] Rall, LB, Resolvent kernels of Green’s function kernels and other finite-rank modifications of Fredholm and Volterra kernels, J. Optim. Theory Appl., 24, 59-88 (1978) · Zbl 0348.45002 · doi:10.1007/BF00933182
[32] Salvy, B.: D-finiteness: Algorithms and applications. In: M. Kauers (ed.) ISSAC 2005: Proceedings of the 18th International Symposium on Symbolic and Algebraic Computation, Beijing, China, July 24-27, 2005, pages 2-3. ACM Press (2005). doi:10.1145/1073884.1073886
[33] Salvy, B.: Linear differential equations as a data-structure. Foundations of Computational Mathematics, pp. 1071-1012, (2019). doi:10.1007/s10208-018-09411-x · Zbl 1431.68166
[34] Salvy, B.; Zimmermann, P., Gfun: a Maple package for the manipulation of generating and holonomic functions in one variable, ACM Trans. Math. Softw. (TOMS), 20, 2, 163-177 (1994) · Zbl 0888.65010 · doi:10.1145/178365.178368
[35] Stanley, RP, Differentiably finite power series, Eur. J. Combinat., 1, 175-188 (1980) · Zbl 0445.05012 · doi:10.1016/S0195-6698(80)80051-5
[36] Trefethen, L.N.: Approximation Theory and Approximation Practice. SIAM (2013). http://www.chebfun.org/ATAP/ · Zbl 1264.41001
[37] Tucker, W.: Validated Numerics: A Short Introduction to Rigorous Computations. Princeton University Press (2011) · Zbl 1231.65077
[38] van den Berg, JB; Lessard, J-P, Rigorous numerics in dynamics, Not. AMS, 62, 9, 1 (2015) · Zbl 1338.68301 · doi:10.1090/noti1276
[39] van der Hoeven, J., Fast evaluation of holonomic functions near and in regular singularities, J. Symbol. Comput., 31, 6, 717-743 (2001) · Zbl 0982.65024 · doi:10.1006/jsco.2000.0474
[40] Wilczak, D.; Zgliczyński, P., \(C^r\)-Lohner algorithm, Schedae Informaticae, 20, 9-42 (2011)
[41] Yamamoto, N.: A numerical verification method for solutions of boundary value problems with local uniqueness by Banach’s fixed-point theorem. SIAM J. Numer. Anal. 35(5), 2004-2013 (1998). doi:10.1137/S0036142996304498 · Zbl 0972.65084
[42] Zgliczyński, P., \(C^1\) Lohner algorithm, Found. Comput. Math., 2, 4, 429-465 (2002) · Zbl 1049.65038 · doi:10.1007/s102080010025
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.