Stream: Constructive reals & analysis

Topic: Continue discussion from Coq PR #12186

view this post on Zulip Michael Soegtrop (Jun 10 2020 at 15:25):

at Russel:

where c = |y(1)| + y is a rough approximation that characterizes the magnitude of y (i.e. y \in [-c,c]). But you should verify this reasoning with a computer.

The problem I see with this is that computing y(1) - I read this as computing y to precision +- 1, might take a very long time in case y has a large magnitude - say the mass of the universe in kg. If y is very small - say some molecular orbital energy in J, it gives a useless much too large estimation of the size of y which results in an excessive precision request when computing x. As physicist I insist on scale invariant numbers - that is numbers where performance does not depend substantially on if a number is 10^100 or 10^-100. Something like a log(log(x)) dependence on the scale is usually OK for physicists. Although there are cases where even that can get tricky - especially for people studying combinatorial problems. Imagine you have <entropy> = k*ln <state space size> and someone actually wants to write down the state space size as a number because for whatever reason you can't work in the log space e.g. when evaluating some integral which you can't integrate symbolically in log space. If the entropy has some macroscopic value, say 1J/K, the natural logarithm of the state space size would be something like 10^23. So the state space size would be exp (10^23) which is a fairly large number. Of cause usually people don't do that (that is they work with the log of the state space size), but that is so because it is almost impossible to work with the state space size itself. But it can be quite tricky to compute the log of an integral without being able to compute the integral itself. Getting a bit more realistic: even when doing high school combinatorics one easily ends up with numbers beyond the exponent range of a pocket calculator. In the high school exams of my son they frequently used numbers for binomial distributions where the probabilities and binomial coefficients get so small/large that a pocket calculator cannot handle them any more (outside of 10^-100 and 10^100), so that you have to use approximation formulas.

For now I am not asking for numbers which can handle such situations. But they should be able to handle the usual pocket calculator range without issues.

Last updated: Jun 10 2023 at 23:01 UTC