Problem with this representation: real number ranges cannot be represented. given two rational numbers \(r_1 < r_2\), it should be there are infinitely many real numbers between \(r_1\) and \(r_2\), so support density of irrationals. https://en.wikipedia.org/wiki/Dense_order

In constructive mathematics, given two real numbers \(r_1' < r_2'\), there should exist a rational number r, such that \(r_1' < r\) and \(r < r_2'\). HOWEVER, these comparisons are a type error for Eq class. In particular this cannot be used to _define_ how to compare two real numbers.

what is meant is if \(r_1' < r_2'\) then there exists a rational r such that \(r_1' < {\mathbf{fromRational}}(r)\) and \({\mathbf{fromRational}}(r) < r_2'\)

In here properties of \({\mathbf{fromRational}}\) are important. Note that comparisons invoke the real comparison, so at most is a recursive definition of real comparison in terms of itself. But it doesn't include termination condition.

It should be so that _if_ two real numbers \(r_1\) and \(r_2\) are not the same real number, then \(r_1 < r_2\) makes sense. But comparing whether two real numbers are the same is undecidable (algorithm for this comparison will not halt if they are same). Would this mean that if \(r_1 < r_2\) is computable, wouldn't \(\neg(r_1 < r_2 \lor r_2 < r_1)\) be computable equality of reals; This is computable in the limit , but not computable? https://en.wikipedia.org/wiki/Computation_in_the_limit

So we are forced to consider only comparison between a rational and a real, but not between two reals. This is encapsulated in the Math.Tools.Interface.DedekindCut type class.

The solution is that when comparing a rational with a real, the rational's denominator determines the accuracy used. This additional information makes comparison between a rational and a real decidable, but doesn't help when comparing two reals.

d x = partial_derivate x

See Suppes: Axiomatic Set Theory. Note that we would like to check that \[\forall \epsilon > 0. \exists n. \forall k > n. |s_k - t_k| < \epsilon \]. However, this is undecidable in particular with respect to what to choose for n. We can nonetheless compute the stream of distances.

cseq_equivalence_matrix computes equivalence of cauchy sequences. However, the modulus argument is undecidable. But if you produce a modulus, this chooses the part of the cauchy sequence differences that should converge according to the convergence ratio of the epsilon from the infinitesimal instance. Thus if you can prove that the matrix elements converge to zero when elements of increasing index are chosen, you would have proven equality of the two cauchy sequences. This could be possible in special cases, even if it's undecidable in general. Note that it suffices to consider the convergence of the first column, because you could move any part to the first column by choosing reasonable values of the modulus. The other differences are included so computations and analysis of the situation can be easier to perform.

This version of cauchy sequence equality convergence check produces a stream of lists, where each list contains those elements which are close to each other in terms of choice of indices, e.g. \[C(s,t)_i = [ \lvert s_j - t_k \rvert | j \leftarrow naturals, k \leftarrow naturals, i = j + k]\] thus the complexity of the stream element lists of the result should increase in the same way than the complexity of the input stream elements. The lists in the result stream have monotonically increasing length. thus to compute results for particular level of approximation, it should suffice to choose a list from the result stream, and perform the equivalence check using the values in the list. To do this, it would be necessary to be able to determine how close to zero the elements in the list should be. the middle element (if any) of the list is probably the most interesting, because that would mean \(j == k\), therefore the computation result would be \(\lvert s_j - t_j \rvert\), but due to different rate of convergence of the input sequences, it can happen that the elementwise differences are not really representative of the stream convergence behaviour at the diagonal. however, analyzing these numbers should produce useful results about convergence of the input stream element differences. e.g choosing minimum and maximum element from each list determines best and worst approximation in the same depth of approximations. for the equality of the cauchy sequences to hold, the best approximation should stay close to zero and better so when further elements of the stream are obtained.

\[ {\rm{partial\_derive}}(\Delta, f, x) = \lim_{\epsilon \rightarrow 0}{{f(\Delta_{\epsilon}(x)) - f(x)}\over{\Delta_{\epsilon}(x) - x}} \]

\[ {\rm{partial\_derivate}}(\Delta, f, x) = \lim_{\epsilon \rightarrow 0}{{f(\Delta_{\epsilon}(x)) - f(x)}\over{\Delta_{\epsilon}(x) - x}} \]

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

An isomorphism \(Cl(R) \cong R\).

Least upper bound property | note this is really undecidable.

Squeeze theorem

Squeeze_theorem

Squeeze_theorem

compute rational approximation more precise than the given rational the precision is expressed as rational number close to zero, the result will be within range \([r-p,r+p]\), in the sense that in the sequence of rational approximations \(r = (r_i | i \in {\mathbf N})\) we have \(\lvert r_{i+1} - r_i \rvert \leq p\). Note that we do _not_ attempt to prove that all successive approximations have this same property, we need the differences to be monotonically decreasing for this to represent correct precision.

here precision is expresses as integer power of 10, e.g. \(1 == 10^{-1}\), \(2 == 10^{-2}\), \(3 == 10^{-3}\) and so on. so how many digits after the decimal point are required.

rational precision expressed as integer power of 10

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

i'th element of derivates_at(f,s) is \(D^i[f](s_i)\)

derivate_around doesn't require f to be defined at x, but requires limits from both sides of x to exist [it never evaluates f at x]. \[ \lim_{\epsilon \rightarrow 0} {{f(x+\epsilon)-f(x-\epsilon)}\over{2\epsilon}} \]

\[\lim_{\epsilon\rightarrow 0}{{f(a+\epsilon,b)-f(a,b)}\over{\epsilon}}\]

\[\lim_{\epsilon\rightarrow 0}{{f(a,b+\epsilon)-f(a,b)}\over{\epsilon}}\]

\[\lim_{\epsilon\rightarrow 0}{{f(a+\epsilon,b,c)-f(a,b,c)}\over{\epsilon}}\]

\[\lim_{\epsilon\rightarrow 0}{{f(a,b+\epsilon,c)-f(a,b,c)}\over{\epsilon}}\]

\[\lim_{\epsilon\rightarrow 0}{{f(a,b,c+\epsilon)-f(a,b,c)}\over{\epsilon}}\]

Arithmetic-geometric mean

Exponential function using limit definition \(\exp(x) = \lim_{n\rightarrow\infty}(1+{{x}\over{n}})^n\).

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

for integrate_curve (xa,ya) curve f dx, Requires: \(\lim_{x \rightarrow 0}curve(x) = 0 \land \lim_{i\rightarrow \infty} dx_i = 0\)

Integral This doesn't converge well.

This attempts to work around the density problem by computing range | in some type which does have enum instance, | then using the given function to map to reals.

This attempts to work around the density problem by computing range | in some type which does have enum instance, | then using the given function to map to reals.

Natural logarithm log(1+z) = z - z^22 + z^33 - ...

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

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

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

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

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

Tetration