Our website would like to use cookies to store information on your computer. You may delete and block all cookies from this site, but parts of the site will not work as a result. Find out more about how we use cookies.
 In the process of refining my program to search for an odd weird number, I needed to determine an upper bound: the least integer p such that (1 + 1/p)^k <= 1 + 1/(r - 1), for given integer k >= 1 and rational r > 1. Now analytically this is straightforward: rearrange to isolate p, and we get p >= 1/((1 + 1/(r - 1))^(1/k) - 1). But the program is written to use an arbitrary precision integer library, and I can't do that in integers: I'd need to go to some high-precision reals, and that's going to get complex and (above all) slow. So I wondered whether there was an expression I could calculate more easily that would get close: after all, I only need an integer, and to a real the gap between one integer and the next is huge. In the simple case, when k = 1, we get p = r - 1. By observation with higher k it looks like p is a bit less than kr, so let's see what we can do with that. If we take p = kr, we need to show:``` (1 + 1/(kr))^k <= 1 + 1/(r - 1) ``` There's a standard expansion of (1+n)^k, so the first step is easy - note that you can read "sum_{i=0}^{k}{ f(i) }" as "the sum of the values of f(i), when i successively takes each of the values from 0 to k":```(1 + 1/(kr))^k = sum_{i=0}^{k}{ (k!/(i!(k-i)!)) / (kr)^i } ``` Now k!/(k-i)! is a product of i numbers from k downwards, so it can't be more than k^i (and can be equal only when i is 0 or 1); and we're dividing by a factor of k^i, so that cancels out neatly:```(1 + 1/(kr))^k = sum_{i=0}^{k}{ (k!/(i!(k-i)!)) / (kr)^i } <= sum_{i=0}^{k}{ 1 / (i! r^i) } ``` Also note that i! must be at least 1 within the relevant range, so 1/i! <= 1:```(1 + 1/(kr))^k = sum_{i=0}^{k}{ (k!/(i!(k-i)!)) / (kr)^i } <= sum_{i=0}^{k}{ 1 / (i! r^i) } <= sum_{i=0}^{k}{ 1 / r^i } ``` And it just happens that there's a well-known sum for the infinite series 1/r^i, which conveniently happens to be ... 1 + 1/(r - 1). And since all the terms in the series are positive, the sum of just a few of them must be less than that:```(1 + 1/(kr))^k = sum_{i=0}^{k}{ (k!/(i!(k-i)!)) / (kr)^i } <= sum_{i=0}^{k}{ 1 / (i! r^i) } <= sum_{i=0}^{k}{ 1 / r^i } < 1 + 1/(r - 1) ```QED. Well that all seems pretty painless: so what does it give us? Well, some typical numbers from early in the program would be r = 385, with k some small integer like 3 or 4. Let's see what the calculator says for the full on calculation:``` p = 1/((1 + 1/(1 - r))^(1/k) - 1) r = 385, k = 3 => p ~= 1152.999427 r = 385, k = 4 => p ~= 1537.499206 ``` Now this gets interesting: taking p = kr gives us 1155 and 1540 respectively for those two calculations, while the calculated numbers seem strangely close to 3r - 2 and 4r - 2.5 respectively: other values for k show the pattern continuing, with the calculated p in each case being a tiny bit less than (kr - (k + 1)/2). That's interesting also, because when k = 1 the inequality becomes equality: (1 + 1/(1.r - (1 + 1)/2))^1 simplifies to exactly 1 + 1/(r - 1). And matching our inequality exactly at k = 1, and within a factor of about one in a million for larger k sounds pretty good - particularly because with the values so spookily close to exact I'd expect them to fall out of the algebra with just a little bit of fiddling. We just need to repeat our earlier trick with a new inequality:``` (1 + 1/(kr - (k + 1)/2))^k <= 1 + 1/(r - 1) ``` [Sound effects: a little bit of fiddling, then a bit more. A pencil snaps.] Nope, can't see where to go from there: the first proof was very simple, but the steps that established inequalities were what simplified the initial expression, and between them they managed to use up all the (quite generous) slack in the system. This new one is way tighter, and there's no way we're going to get away with anything like that. Next step, go talk to Simon: does he have some graphing software handy that'll show what some of these values look like? He does indeed, and we try one out. I don't think the picture will change much with small changes to r from 385, but since r can in principle be any rational number greater than 1, that calculation of 1/(r - 1) gets to move a lot more when r is close to 1, so let's try setting it to 11/10: the inequality then becomes:``` (1 + 1/(11k/10 - (k + 1)/2))^k <= 11 ```and the left hand side (LHS) rearranges to (1 + 10/(6k - 5))^k. Here's what the graph looks like: [to be inserted when I get a screenshot]. The graph decreases uniformly from infinity at the singularity when k = 0, and since our inequality gives an exact match at k = 1 we'd have proof enough if we could show the graph acts like that for every r > 1. Can we show that? Well a function f(x) is decreasing if f(x + d) < f(x) for arbitrarily small positive d. Which is another inequality:``` (1 + 1/(kr - (k + 1)/2))^k < (1 + 1/((k + d)r - ((k + d) + 1)/2))^(k + d) ``` Ouch, that looks horrible, and I'm not going to touch it with a bargepole. [Later] Silly me, it is at least a bit easier than that: a function f(x) is decreasing wherever it's derivative f'(x) < 0. But the derivative looks just as nasty - (f(x)^x)' = f(x)(xf'(x)/f(x) + ln(f(x)) - so I'm not going to bother. Ok, time to step back and rethink. What I'd like to do is get something simpler than that (kr - (k + 1)/2) expression by factoring out the k, but that gives (k(r - 1/2) - 1/2) which is hardly better. But let's remember these are my own variables and the r is only used in one other place: what happens if I hide the 1/2 with a change of variable? Let's say s = r - 1/2, what would that give us? The LHS is easy: we just substitute in the s, and just for kicks I'll multiply through by 2 to get rid of the other 1/2:``` (1 + 2/(2ks - 1))^k ``` For the RHS it's probably easier if we combine it into a single fraction:``` 1 + 1/(r - 1) = r/(r - 1) = (s + 1/2) / (s - 1/2) = (2s + 1) / (2s - 1) ```Ooh, pretty. :) But now the 2's are bugging me, so let's redefine it slightly: let's say instead s = 2r - 1, that gives:``` (1 + 2/(ks - 1))^k <= (s + 1) / (s - 1) ``` That gives me an idea: what if we turn the LHS into a single fraction as well?``` 1 + 2/(ks - 1) = (ks + 1) / (ks - 1) ``` Dang, now we're getting somewhere - put them together, check the range for which s is valid, and we now have, for k >= 1, s > 1:` ((ks + 1) / (ks - 1))^k <= (s + 1) / (s - 1)` That's so pretty it just has to be true. I still have no idea how to prove it, but at least it's now looking like something that might be a theorem someone's previously proven, or failing that one that a proper mathematician might be motivated to have a crack at: time to go ask around. Hugo
 Proving an inequality Hugo van der Sanden - 03:20 22/06/05 Re: Proving an inequality Simon - 08:18 22/06/05 Now I understand what you were trying to do! Somewhere on a CD I've got an old demo copy of Mathematica, which may be more capable of producing the graph you want. I'll have a look later. -- simon Re: Proving an inequality Hugo van der Sanden - 18:51 01/07/05 ...or failing that one that a proper mathematician might be motivated to have a crack at: time to go ask around. So I went to the Math Forum to "Ask Dr. Math", and got two excellent replies which proved the result in two different ways. Unfortunately I didn't get an answer to "is it ok for me to publish those responses?", so I'll just have to try and reproduce them as best I can. To prove:` ((ks + 1) / (ks - 1))^k <= (s + 1) / (s - 1)` The first approach One way to simplify the problem is to cross-multiply to remove the fractions:``` (ks + 1)^k . (s - 1) <= (ks - 1)^k . (s + 1) ``` Now we can turn the powers into sums:``` sum_{i=0}^k {(s - 1) C(k, i) (ks)^(k - i)} <= sum_{i=0}^k {(s + 1) C(k, i) (ks)^(k - i) (-1)^i} ``` And subtract one side from the other:``` sum_{i=0}^k {((s + 1) (-1)^i - (s - 1)) C(k, i) (ks)^(k - i)} >= 0 ``` Now we can resolve the (-1)^i by splitting the sum into even and odd i:``` sum_{i=0}^{k/2} {2 C(k, 2i) (ks)^(k - 2i)} >= sum_{i=0}^{(k-1)/2} {2s C(k, 2i + 1) (ks)^(k - 2i - 1)} ``` All these terms are positive, and since we count from 0 there are at least as many even values of i as odd values, so if the inequality is satisfied when we match up the evens and odds in pairs we'll have proven the result. So we need:``` 2 C(k, 2i) (ks)^(k - 2i) >= 2s C(k, 2i + 1) (ks)^(k - 2i - 1) C(k, 2i) (ks)^(k - 2i) >= s C(k, 2i + 1) (ks)^(k - 2i - 1) C(k, 2i) (ks) >= s C(k, 2i + 1) k C(k, 2i) >= C(k, 2i + 1) k k! / ((2i)! (k - 2i)!) >= k! / ((2i + 1)! (k - 2i - 1)!) k / (k - 2i) >= 1 / (2i + 1) k(2i + 1) >= k - 2i ki >= i ```.. and since k >= 1, i >= 0 the proof is complete. The second approach We can make the two sides more similar to each other by raising to the power of s; since both sides are positive, and s >= 1 the sign of the inequality stays the same:``` ((ks + 1) / (ks - 1))^(ks) >= ((s + 1) / (s - 1))^s ``` Since we know k >= 1 this is equivalent to showing that ((x + 1) / (x - 1))^x is a decreasing function, which is true if its derivative is negative in the relevant range (ie when x > 1). Now I'm not entirely sure how to differentiate this - the simple form of the Chain Rule doesn't apply, so I think we need to use the more complex partial derivative version:``` f(x) = (x + 1) / (x - 1) g(x) = x z(f, g) = f(x)^g(x) dz/dx = ∂z/∂f df/dx + ∂z/∂g dg/dx ``` Assuming this is correct, we get:``` z' = g . f^(g - 1) f' + g' ln(f) f^f g' = z( f'g/f + g'^2 ln(f) ) = z( -2x / (x^2 - 1) + (ln(x + 1) - ln(x - 1) ) <= 0 ```and since z > 0, we just need:``` 2 x / (x^2 - 1) >= ln(x + 1) - ln(x - 1) ``` For the next bit a change of variables is in order so that we can take advantage of some standard expansions. Let y = 1/x so that our range becomes 0 < y < 1, and we then get:``` 2y / (1 - y^2) >= ln(1 + y) - ln(1 - y) ``` The LHS can be simplified to 1 / (1 - y) - 1 / (1 + y) which gives us the MacLaurin expansion:``` 2y + 2y^3 + 2y^5 + 2y^7 + ... ``` The RHS similarly expands to:``` 2y + 2y^3/3 + 2y^5/5 + 2y^7/7 + ... ``` Comparing these terms pairwise, since y is positive the LHS is trivially greater than or equal to the RHS for each pair, so the LHS sum is indeed greater than or equal to RHS sum, and once again we have proven our result. Hugo Re: Proving an inequality Bruce Ure - 23:41 17/07/05 This stuff is really rather beautiful but I can't pretend I understand even the simplest bits of it. I still enjoy reading it enormously, though, and I don't think failure to understand detracts all that much from it. So keep it coming :-) Are you actually searching for weird numbers at the moment, or solely working on this algorithmic hieroglyphics as a means to making the search more efficient? Re: Proving an inequality Hugo van der Sanden - 01:04 18/07/05 I have searched all 7-factor possibilities without finding a wierd number. There are an enormous number of 8-factor possibilities to check, so there was no point starting that run before my imminent house move (which will perforce involve having the computer turned off (eek!) at some point). Even then, starting that search is of little use except to get an estimate of how many years the search would take, so that I'd have an idea how far I'd need to improve the algorithm to have a hope of completing it. For the record my programme can now check the 10^8 or so primitive abundant 7-factor numbers in about 45 minutes; a correspondent (Bob Hearn) estimates the 8-factor numbers at around 3 x 10^15, so my baseline is about 2,500 years. I still have some work to do on correctness though - the list of numbers I check doesn't exactly correspond with Bob's, and while I'm aware of some differences that are insignificant I need to fix the program to remove them before I can verify that there are no remaining differences that are significant. Hugo Re: Proving an inequality Bruce Ure - 01:17 19/07/05 Fascinating. What have you written it in? If perl, does that mean it would run on [my|a] PC running perl (on windows)? Re: Proving an inequality Hugo van der Sanden - 02:05 19/07/05 Current version is about 400 lines of C code using the GMP library. My code should be fairly straightforward to compile if you have a reasonably standards-compliant C compiler, though I may unwittingly have used a couple of unportable typedefs. I'm not sure if there is a pre-compiled Win* version of the library though - I couldn't see one at a glance, at least. You may find that you need some or all of MinGW, but it may turn out to be easier than that. If you want to play, the latest version is gmp_ptrack.c-0.07. Hugo Re: Proving an inequality Bruce Ure - 10:43 19/07/05 I think that puts this in that category of things which I would love to play with but probably can't justify just at the moment. But thanks. Maybe you could show me if/when I visit you in your new place. (Strictly between you and me, like... I know someone who deals numbers. Want me to see if he can get you an 8-factor weird? He had some lovely primes last week. I know he was busy trying to fit an irrational into his car at the weekend but he's probably sorted it by now.)