RadiiPolynomial.jl

RadiiPolynomial is a software library to validate a numerical solution to an equation by computing rigorously a radius $r$ such that an exact solution exists within a closed ball (and is the only one there) centered at the approximation and of radius $r$.

Here is a complete computer-assisted proof for the initial value problem

\[\begin{cases} \displaystyle \dot{u}(t) = u(t)(1 - u(t)), & t \in [-2, 2],\\ u(0) = 1/2. \end{cases}\]

It proves that an analytic solution lies within inf(ie) of a polynomial approximation.

using RadiiPolynomial, LinearAlgebra# IVP as a zero-finding problemF(u)  = u - exact(0.5) - Integral(1) * (u * (exact(1) - u))DF(u) = exact(I) - Integral(1) * Multiplication(exact(1) - exact(2) * u)# approximate solution, with floating-point arithmeticK = 27u_bar, converged = newton(u -> (F(u), DF(u)), zeros(Taylor(K)))Π = Projection(Taylor(K))A_finite = inv(Π * DF(u_bar) * Π)# bounds, with interval arithmeticν   = interval(2)X   = Ell1(GeometricWeight(ν))u_i = interval(u_bar)A_i = interval(A_finite) + (interval(I) - interval(Π))Y   = norm(A_i * F(u_i), X)Z₁  = opnorm(interval(Projection(Taylor(K+1))) - A_i * DF(u_i) * Projection(Taylor(K+1)), X)Z₂  = max(opnorm(A_i * Π, X), interval(1)) * ν * interval(2)# check the hypotheses of the Radii Polynomial Theoremie, proved = interval_of_existence(Y, Z₁, Z₂, Inf)inf(ie), proved

(2.232051998824705e-6, true)

That proved == true is what distinguishes this from a standard numerical ODE solver. A complete walkthrough of this example is given in The logistic equation.

Where to go

Installation

RadiiPolynomial requires Julia v1.10 or above.

julia> using Pkgjulia> Pkg.add("RadiiPolynomial")

Open source and citation

RadiiPolynomial is released under the MIT license and developed at github.com/OlivierHnt/RadiiPolynomial.jl.

If you use it in a publication, in research or in teaching, please cite it using the BibTeX template CITATION.bib (more information).

RadiiPolynomial