Documentation

This real representation takes epsilon as input as in epsilon-delta proof.

approximate takes a real \(r\), and a rational \(q\) and produces a rational \(q_2\) such that \(|r - q_2| \le q\)

\(r_1 (r_2 q) = (r_1 r_2) q\), where \(r_1,r_2 \in {\mathbf{R}}\), \(q \in {\mathbf{Q}}\).

that is, \[{\mathbf{approximate}}(r_1) \circ {\mathbf{approximate}}(r_2) = {\mathbf{approximate}}(r_1 r_2)\] that is, \[{\mathbf{approximate}}(r_1,{\mathbf{approximate}}(r_2,q)) = {\mathbf{approximate}}(r_1 r_2, q)\] that is \[{\mathbf{approximate}}(r_1,q_3)=q_2 \Leftrightarrow |r_1 - q_2| \le q_3\] \[{\mathbf{approximate}}(r_2,q) =q_3 \Leftrightarrow |r_2 - q_3| \le q\] \[{\mathbf{approximate}}(r_1 r_2, q)=q_2 \Leftrightarrow |r_1 r_2 - q_2| \le q\] \[{\mathbf{approximate}}(r_1 r_2, q)={\mathbf{approximate}}(r_1,q_3)={\mathbf{approximate}}(r_1,{\mathbf{approximate}}(r_2,q))\] \[\Leftrightarrow |r_1 - q_2| \le q_3 \land |r_2 - q_3| \le q\]

this propagates accuracy without changing it.

this propagates accuracy without changing it

inverseImage transforms accuracy computation of the real.

The first argument is the function lifted. The second argument describes change in accuracy by the function.

approx_compose will use the second real as the level of approximation to compute the first.

This lifts a rational function to a real function. This computes accuracy using the formula \(dx = df / f'(x)\). The accuracy behaves badly when \(f'(x) = 0\) due to divide-by-zero.

derivate for rational functions. The first argument is epsilon.

computes derivate. \[{{df}\over{dt}} = \lim_{\epsilon\rightarrow 0}{{f(t+\epsilon)-f(t)}\over{\epsilon}}\]

newton's method for finding root of function. \[x_{i+1} = x_i - {{f(x_i)}\over{f'(x_i)}}\]

square root of a real number \(x\), computed with newton's method as root of \(t \mapsto t^2 - x\).

logarithm of a real number \(x\), computed with newton's method as root of \(t \mapsto e^t - x\).

Using Simon Plouffe's BPP digit extraction algorithm for computing pi. See https://plouffe.fr/Simon%20Plouffe.htm See Pi for details. \[\pi = \sum_{k=0}^{\infty}{16^{-k}}({{4}\over{8k+1}}-{{2}\over{8k+4}}-{1\over{8k+5}}-{1\over{8k+6}})\]

https://en.wikipedia.org/wiki/Inverse_trigonometric_functions

https://en.wikipedia.org/wiki/Inverse_trigonometric_functions

https://en.wikipedia.org/wiki/Inverse_trigonometric_functions

trigonometric functions Computed using taylor series expansion of sin function. \[\sin(x) = \sum_{k=0}^{\infty}{{{(-1)^k}\over{(2k+1)!}}{x^{2k+1}}}\]

trigonometric functions Computed using taylor series expansion of cos function. \[\cos(x) = \sum_{k=0}^{\infty}{{{(-1)^k}\over{(2k)!}}{x^{2k}}}\]

For \(a,b \in {\mathbb Q}\) and \(0 \in (a,b) \) the invocation \(f(a)(b)\) of \(f\) in \(computable\_r(f)\) must produce approximation \(q\) of another real \(r\) as rational number, such that \( r - q \in (a,b) \).

this real_to_rational operation sets precision \(\epsilon\) to 0 and produces corresponding rational number. Many algorithms for reals will go to infinite loop, if this is used, or produce divide-by-zero. In particular, this is expected for irrationals. if rational number is produced, it's exact. However, computations on rational numbers, where real number was created using fromRational, will produce that rational. It also allows operations lifted from rationals to work, producing the result you'd obtain from rational numbers.