On simplifying large exponential equations

Question

I'm working on undergrad research in fractal geometry and have to prove certain functions are decreasing, one of which is

$$g(x) = \frac{\left( \frac{2^m-2}{2^m-1}+ \frac{1}{2^m-1}\left(\frac{1}{2^m}\right)^x\right)^s}{\frac{3^m-5}{3^m-2}+ \frac{3}{3^m-2}\left(\frac{2}{3^m}\right)^x}$$

where $m\in\mathbb{Z},m\geq2$, $s= \log_2(3)$. (i.e. the Hausdorff dimension of the Sierpinski Gasket).

My issue is that trying to take the derivative by hand and showing that its less than 0 is really quite messy. From some plots on Desmos, I'm fairly confident that the function is decreasing after a certain value of $m$.

I've used mathematica to take the Derivative and repeatedly used simplify/fullsimplify on D[f[x],x]<0 and the results that come out. It's clear that at each stage of results, there's some "chunk" of the output that is ambiguous on sign, but my issue right now is that I don't really know whether or not to have confidence in what Mathematica is doing.

I would really like to be able to do some work by hand to reach some kind of result, so I was wondering if there are some "tricks of the trade" in analysis that are suitable for dealing with such cases.

I guess another big question is whether or not it's even a valuable use of my time to be attempting to do this by hand (as much as I'd like to). This problem involves a much more complicated function by replacing the "2" and "3" seen above with variables $A\in\mathbb{N}, A\geq2$ and $\sum_{i=1}^A i$ which I would have to deal with similarly.

I appreciate any tips, help, or advice and any reassurance that the community can provide.

Here's the code for this function specifically:

In[11]:= f2[x_] := ((2^m - 2)/(2^m - 1) + 1/(2^m - 1) (1/2^m)^x)^
  Log[2, 3]/((3^m - 5)/(3^m - 2) + 3/(3^m - 2) (2/3^m)^x);

In[12]:= D[f2[x], x]

Out[12]= ((2^-m)^
  x ((2^-m)^x/(-1 + 2^m) + (-2 + 2^m)/(-1 + 2^m))^(-1 + Log[3]/Log[2])
   Log[3] Log[
   2^-m])/((-1 + 2^m) ((
    3 2^x (3^-m)^x)/(-2 + 3^m) + (-5 + 3^m)/(-2 + 3^m)) Log[
   2]) - (((2^-m)^x/(-1 + 2^m) + (-2 + 2^m)/(-1 + 2^m))^(Log[3]/
    Log[2]) ((3 2^x (3^-m)^x Log[2])/(-2 + 3^m) + (
      3 2^x (3^-m)^x Log[3^-m])/(-2 + 3^m)))/((
    3 2^x (3^-m)^x)/(-2 + 3^m) + (-5 + 3^m)/(-2 + 3^m))^2

In[17]:= Assuming[{m >= 1}, Simplify[D[f2[x], x] < 0]]

Out[17]= (3/2)^(m x) ((-2 + 2^m + 2^(-m x))/(-1 + 2^m))^(Log[3/2]/
  Log[2]) (3 2^x - 5 3^(m x) + 3^(
    m + m x))^2 (3 2^x (1 - 2^(1 + m x) + 2^(m + m x)) Log[2]^2 + 
    m Log[3] (3^(m + m x) Log[2] - 2^((1 + m) x) (-2 + 2^m) Log[8] - 
       3^(m x) Log[32])) > 0

(*Grabbing the part that is sign-ambiguous*)

In[19]:= Assuming[{m >= 1}, 
 FullSimplify[(3 2^x (1 - 2^(1 + m x) + 2^(m + m x)) Log[2]^2 + 
     m Log[3] (3^(m + m x) Log[2] - 2^((1 + m) x) (-2 + 2^m) Log[8] - 
        3^(m x) Log[32])) > 0]]

Out[19]= 3^(m x) (-5 + 3^m) m Log[3] + 
  2^x (Log[8] + 2^(m x) (-2 + 2^m) (Log[8] - m Log[27])) > 0

(This seems to be simple enough to continue by hand. But is it really equivalent?*)
```

Answer 1

The following Wolfram language code

f[m_, x_] := ((2^m - 2)/(2^m - 1) + (1/2^m)^x/(2^m - 1))^(Log[3]/
  Log[2])/((3^m - 5)/(3^m - 2) + (3 (2/3^m)^x)/(3^m - 2));
Reduce[Exists[x, x > 0 && D[f[2, x], x] >= 0]]

Returns False, so for $m=2$ your function is decreasing. The same is true for $m=3,4,5,6$, which are the values I have tested. Unfortunately, I'm not sure how to get Mathematica to solve this problem for arbitrary integral $m\geq 2$; I tried naively

Reduce[Exists[{m, x}, Element[m, Integers] && m >= 2 && x > 0, D[f[m, x], x] >= 0]]

but this returns the error

Reduce: This system cannot be solved with the methods available to Reduce.

I should mention that if Reduce says that a statement is false, you can probably trust it. However, there is of course a tiny but nonzero chance that some bug in the program actually led to the false output, so it is not considered a rigorous proof.