• A first validation
• • • Step 1: Formulation
    • Step 2: Approximation (floating-point arithmetic)
    • • The approximate zero
      • The approximate inverse
    • Step 3: Bounds (interval arithmetic)
    • Step 4: Conclusion
  • Two things to try

A first validation

We prove that the equation

\[u^3 - 2 = 0\]

has a solution in $\mathbb{R}$.

Step 1: Formulation

We study the zeros of $F(u) \bydef u^3 - 2$, and we will look for them as fixed points of

\[G(u) \bydef u - A F(u),\]

where $A$ is a number approximating $1/DF(\num)$. A fixed point of $G$ is a zero of $F$ precisely when $A \ne 0$, which we get for free here.

using RadiiPolynomialF(u)  = u^3 - exact(2)DF(u) = exact(3) * u^2

exact(2) says that the literal 2 is to be considered an exact value. The last experiment at the bottom of this page shows what happens if it is omitted.

Step 2: Approximation (floating-point arithmetic)

Nothing here needs to be rigorous, this step only has to produce sufficiently accurate numbers:

• the quality of the approximation $\num$ is measured by $Y$, and
• the quality of the approximation $A$ is measured by $Z_1$.

The approximate zero

u_bar, converged = newton(u -> (F(u), DF(u)), 1.0)

(1.2599210498948732, true)

newton takes a single function returning both $F$ and $DF$, and returns the refined value together with a flag. The flag is meant to be read: converged == false means the value may not be sufficiently good numerically for the validation to succeed.

The approximate inverse

A = inv(DF(u_bar))

0.2099868416491455

Step 3: Bounds (interval arithmetic)

From here everything requires interval arithmetic. We need the bounds

\[|A F(\num)| \le Y, \qquad \sup_{u \in B(\num, R)} |1 - A DF(u)| \le Z_1.\]

The second is a supremum over a whole ball. Interval arithmetic can do this computation readily since interval(u_bar, R; format = :midpoint) is the ball $B(\num, R)$, so evaluating DF on it returns an enclosure of $DF$ over every point of that ball at once.

Y  = abs(interval(A) * F(interval(u_bar)))R   = 2sup(Y)u_R = interval(u_bar, R; format = :midpoint)   # the ball B(ū, R)Z₁  = abs(interval(1) - interval(A) * DF(u_R))Y, Z₁

([0.0, 9.32529e-17]_com, [0.0, 6.66134e-16]_com)

Step 4: Conclusion

We now check that $G$ contracts on a ball:

ie, proved = interval_of_existence(Y, Z₁, R)

([9.32528e-17, 1.86506e-16]_com, true)

proved is true, so the Radii Polynomial Theorem applies: there is a real root of $u^3 - 2 = 0$ within inf(ie) of u_bar, and it is the only one within sup(ie).

inf(ie), sup(ie)

(9.325289058687932e-17, 1.8650578117375848e-16)

The proven bound is at the scale of machine epsilon.

Two things to try

R = 1e-20ie, proved = interval_of_existence(Y, Z₁, R)

(∅_trv, false)

Y_sloppy = abs(interval(A) * (interval(u_bar)^3 - 2))isguaranteed(Y), isguaranteed(Y_sloppy)

(true, false)