A formal proof for x^2 = 2^x

[BMAD]

There are three solutions. Can you find a formal proof for all three?

[Federico]

Starting from the raising power operator, defined between two numbers x and y over a number field, x^y is not the same as y^x, due to the missing commutativity property respect than the other sum and multiplication rank binary operators.

So this post is questioning for wich value of x in natural, integers, reals (or complex) number fields this identity is verified:

x²  = 2^x .

This is what we call an equation to solve.

This problem could also be interpreted geometrically asking in which points the parabola y=x² intersect the esponential function y=2^x.

Before we start exploring over the natural number (positive integers), we know that 2^x > 0 and x² ≥ 0 for every x Reals.

So, we can exclude immediatly the case for the integer x=0 wich implies:  0² < 2^0,, that is 0 < 1.

Furthermore, for the same reason and due to negative power of 2, for every negative integer x ≤ 1, we have 2^x < x² .

So, for positive integers x>0, both 2^xand x² are crescent functions : 2^x+1 ≥ 2^x and (x+1)² ≥ x²,
and by the fact that:
   for x=1, 1² <2¹ (that is 1 < 2), and
   for x=3, 3² >2^{3 (}that is 9>8),
this implies that an integer solution is between 1 and 3.

Hence, our 1st trivial solution is for x=2:   2² = 2² = 4 .

In a similar way, from the fact that at x=5 , we have  2⁵ = 32 > 5² = 25, we candidate next integer solution to be between 3 and 5, that is x=4.

Analizing the number 4 as result of this 1st trivial solution,  It is interesting to observe that the number 2 let the 4 = 2+2 = 2*2 = 2^2 = ... ,  for every rank of the binary operator used.

4^2 = (2^2)^2 = 2^(2*2) = 2^(2+2) = 2^4 = 16.  (Notice that just for the positive integer 2 you can make (2^2)^2 = 2^(2^2) )
From this point on, infact, 2^x will exceed x^2 for every real x>=4, so no more positive real solution after 4.

Infact for every integer x>0
(x+4)² ≤ 2^(x+4)   ,     applying log in base 2 to both members, we can compare
2 log₂(x+4) ≤ x+4 ≤ x+4 + x+4 ≤ 2(x+4)
log₂(x+4) ≤ x+4 , for every real x>0.
So for every x>4 we proved that  x² ≤ 2^x.

But it's not the only interval where 2^x exceeds x².
infact,
x² = 2^x , can be rewritten as 2nd grade equation giving the:
x = 2^x , and x = 2^-x solutions.

Using the fact that
(-x)² = 2^x , or
(x)² = 2^-x 
x = 2^-x/2

From the theorem of the fixed point applied to our exponential,
starting from x₀=1, 
and proceeding recursively
x₁ = -2^x₀/2 = -√2
x₂ = -2^x₁/2 = -√2^-1/√2
x₃ = -2^x₂/2 = -√2^-√2/2
...
x_n = -2^x_n-1  = -√2^{-√2^(-√2^....n-1Times....^-√2))}

The greater will be n and the smaller will be the difference x_n+1 -x_n.
The limit for n that tends to infinity of x_n  is equal to value x:

x₁  = 1
x₁  = -1.41421356237310...
x₂  = -0.612547326536066...
x₃  = -0.808727927081827...
x₄  = -0.755569324854238...
x₅  = -0.769618475247432...
x₆  = -0.765880261444542...
x₇  = -0.766873153047868...
x₈  = -0.766609309719418...
x₉  = -0.766679412545762...
x₁₀ = -0.766660785691404...
x₁₁ = -0.766665734944187...
x₁₂ = -0.766664419898679...
x₁₃ = -0.766664769313767...
x₁₄ = -0.766664676472171...
x₁₅ = -0.766664701140715...
x₁₆ = -0.766664694586141...
x₁₇ = -0.766664696327729...
x₁₈ = -0.766664695864979...
x₁₉ = -0.766664695987935...
x₂₀ = -0.766664695955265...
x₂₁ = -0.766664695963945...
x₂₂ = -0.766664695961639...
x₂₃ = -0.766664695962252...
x₂₄ = -0.766664695962089...
x₂₅ = -0.-66664695962132...
x₂₆ = -0.766664695962121...
x₂₇ = -0.766664695962124...
x₂₈ = -0.766664695962123...

x₂₉ = -0.766664695962123...

The value asimptotically converge quickly according the desired precision.

Another method to find a closed form using the Lambert function W(z) = z e^z,
which gives the solution in function of 

 

F. Prowedi

[bonanova]

x=2 and 4.
Proof:

2² = 2²

4² = (2²)² = 2⁴.

The third solution is x = -.76666468...., found numerically, looking for closed form.

[bonanova]

Using natural logarithms, the equation becomes

x = 2 ln(x)

1. x = 2 = 2 ln (2) = 2 x 1 = 2
2. x = 4 = 2 ln (4) = 2 x 2 = 4

The third root is negative and solves

x = -2 ln (x)

Which has no algebraic solution.
Numerically, it's

x = -0.766664695 ....

Interested to find out what you mean by formal proof.

[dark_magician_92]

roots are easy to find and 2 roots may be somehow proved. 3rd is difficult to prove.

Using log base e,

2 lnx = x ln 2
x/lnx = 2/ln2, By comparison, x=2 and also LHS= 4/2lnx, again compare, x=4.