An inequality.
in [Math]
|
Prev: Original Result Tunze.
Next: open challenge to Chandler Davis; Iain Davidson reminds one of Flath -- Euclid's IP proof #5.01 Correcting Math
From: Rob Johnson on 9 Aug 2010 16:17 In article <4c6033fd$0$10191$ba4acef3(a)reader.news.orange.fr>, Raymond Manzoni <raymman(a)free.fr> wrote: >Rob Johnson a �crit : >> In article <4c5efa99$0$10185$ba4acef3(a)reader.news.orange.fr>, >> Raymond Manzoni <raymman(a)free.fr> wrote: >>> Shin Dongjun a �crit : >>>> Prove (log3)^2 > (log4)^3. >>>> >>>> (Don't use an approximation like log3 = 0.4771) >>>> >>>> log is common logarithms that is, base of log is 10. >>> >>> You could, for example, study f(x)= (x-1) ln(ln(x)) for x > e ... >> >> This works well for proving the other direction for natural logs: >> >> ln(3)^2 < ln(4)^3 [1] >> >> The derivative of (x-1) ln(ln(x)) = ln(ln(x)) + (x-1) 1/(x ln(x)), >> which is positive for x > e. Thus, (x-1) ln(ln(x)) is monotonically >> increasing for x > e, which implies [1]. >> >> However, since the OP is about common logs, we get >> >> (x-1) log(log(x)) >> >> = (x-1) (ln(ln(x)) - ln(ln(10)))/ln(10) >> >> whose derivative is >> >> ln(ln(x)) - ln(ln(10)) + (x-1)/(x ln(x)) >> ---------------------------------------- >> ln(10) >> >> which is negative for x in [3,3.7517684] and positive for x in >> [3.7517684,4]. Thus, (x-1) log(log(x)) is decreasing for about 3/4 >> of the interval in question and increasing for about 1/4. However, >> trying to use this in a proof seems difficult. >> >> Rob Johnson <rob(a)trash.whim.org> > > > You are right Rob I noticed my mistake too (from your other >answer...) and the fact that the derivative became 0 in (3,4) as you >indicated (invalidating my attempt at least directly). > > In fact I was searching a correct way to handle this and got some >results 'in line' with your response : > >1) > Let's prove directly that (log(3)/log(2))^2 > 8 log(2) : > > Tables of powers : > 2^n : 2, 4, 8, 16, 32, 64, 128, 256, 512, 1024, 2048 > 3^n : 3, 9, 27, 81, 243, 729, 2187 > > so that 3^7 > 2^11 (2187>2048, 9>8 is too weak...) > > and (log(3)/log(2))^2 > (11/7)^2 > > On the other side 10 log(2)= log(1024)= log(1000*(1+24/1000)) = 3 >+ log(1+24/1000) < 3 + 24/(1000 ln(10)) (the series for log(1+x) is >alternate) > so (using ln(10)>2 and 24<25) 10 log(2) < 3 + 1/80 > > so that 8 log(2) < 241/100 < (11/7)^2 < (log(3)/log(2))^2 >(laborious ...) > > >2) > Starting with 3^12 > 2^19 is more direct : > (log(3)/log(2))^2 > (19/12)^2 > (360/12^2 = 5/2) > > 2^16 < 10^5 so that 8 log(2) < 5/2 > > (to find 19/12 I used continued fractions of log(3)/log(2)) > > >... > Other tricks could be tried (use 3^4 > 80 to get log(3)^2 > (1 + 3 >log(2))^2/16 that has to be greater than 8 log(2)^3 and so on...) > > but I was overall dissatisfied by all these answers... (kind of >cheating since we replace 'real values approximations' by large integers >computations). Perhaps too that I didn't get the point of the problem >since... I still prefer my initial answer even if of no value here! :-) > > Thanks for the correction anyway, > Raymond I, too, was left with an unsatisfied feeling with this problem after my solution. I computed log(3)/log(4) and sqrt(log(4)/log(10)) and used continued fractions to find the rational number between them with the smallest denominator (7/9). However, I find computing 4^81 somewhat distasteful in a problem that essentially asks for hand computation. However, I played around a bit more and found a smaller set of rational approximants with denominators no greater than 14 that can be used. These can be more easily verified: 3^14 > 4^11 (11/14)^2 > 8/13 10^8 > 4^13 These inequalities prove that (log(3)/log(4))^2 > (11/14)^2 > 8/13 > log(4)/log(10) Since the exponents are more reasonable, this makes me feel a bit better. However, I still feel there must be a better solution. Rob Johnson <rob(a)trash.whim.org> take out the trash before replying to view any ASCII art, display article in a monospaced font
From: Gc on 10 Aug 2010 04:51 On 8 elo, 20:39, Shin Dongjun <acam...(a)gmail.com> wrote: > Prove (log3)^2 > (log4)^3. > > (Don't use an approximation like log3 = 0.4771) > > log is common logarithms that is, base of log is 10. log(3)^2 = log(12/4)^2 = (log(12) - log(4))^2 = log(12)^2 - 2log(12)log(4) + log(4)^2 > log(4)^2, because log(12)log(12) > 2log(12)log(4) = log(12)log(8).
From: Gc on 10 Aug 2010 04:56 On 10 elo, 11:51, Gc <gcut...(a)hotmail.com> wrote: > On 8 elo, 20:39, Shin Dongjun <acam...(a)gmail.com> wrote: > > > Prove (log3)^2 > (log4)^3. > > > (Don't use an approximation like log3 = 0.4771) > > > log is common logarithms that is, base of log is 10. > > log(3)^2 = log(12/4)^2 = (log(12) - log(4))^2 = log(12)^2 - > 2log(12)log(4) + log(4)^2 > log(4)^2, because log(12)log(12) > > 2log(12)log(4) = log(12)log(8).
From: Gc on 10 Aug 2010 05:05 On 10 elo, 11:51, Gc <gcut...(a)hotmail.com> wrote: > On 8 elo, 20:39, Shin Dongjun <acam...(a)gmail.com> wrote: > > > Prove (log3)^2 > (log4)^3. > > > (Don't use an approximation like log3 = 0.4771) > > > log is common logarithms that is, base of log is 10. > > log(3)^2 = log(12/4)^2 = (log(12) - log(4))^2 = log(12)^2 - > 2log(12)log(4) + log(4)^2 > log(4)^2, because log(12)log(12) > > 2log(12)log(4) = log(12)log(8). No,OMG, forget his.
From: Rob Johnson on 10 Aug 2010 05:28
In article <dd0464f6-0c3f-4b6c-b3cf-8895e792b4f5(a)f42g2000yqn.googlegroups.com>, Gc <gcut667(a)hotmail.com> wrote: >On 8 elo, 20:39, Shin Dongjun <acam...(a)gmail.com> wrote: >> Prove (log3)^2 > (log4)^3. >> >> (Don't use an approximation like log3 = 0.4771) >> >> log is common logarithms that is, base of log is 10. > >log(3)^2 = log(12/4)^2 = (log(12) - log(4))^2 = log(12)^2 - >2log(12)log(4) + log(4)^2 > log(4)^2, because log(12)log(12) > >2log(12)log(4) = log(12)log(8). 2 log(4) = log(16) not log(8). A big tip-off that something is wrong is that you've just proven that log(3)^2 > log(4)^2, which is false. Rob Johnson <rob(a)trash.whim.org> take out the trash before replying to view any ASCII art, display article in a monospaced font |