Simplify Log monotonicity

Why does:

FullSimplify[(n+1)^2>n^2,n>=2]


evaluate to True, but:

FullSimplify[Log[n+1]>Log[n],n>=2]


remains unchanged?

Thank you.

• Reduce[{Log[n + 1] > Log[n], n >=2}]. Jun 23 at 12:49
• Resolve[ForAll[n, n >= 1, Log[n + 1] > Log[n]]]
– Syed
Jun 23 at 12:52
• Okay, thank you both. Should it be obvious to me why FullSimplify works for the one, and not the other? And why Reduce succeeds with both? Do you in general shy away from FullSimply, in favor of Reduce? Asked differently: why would Resolve all of a sudden be necessary? Perhaps the key is that FullSimplify is pattern matching, whereas the other two are performing mathematical reduction/resolution? Thanx. Jun 23 at 12:53
• Well, Simplify is supposed to "simplify" an expression. Typically gives one with smaller leaf size. I am not sure it is supposed/required to return "True" or "False", even though it did that on the first example you gave it. That is why Reduce is there. Looking at help, I see no place where it says it will return "True" or "False" for inequality relation? May be for one that are "easy" to figure out, it return True or False and that is why it worked on your first example. Jun 23 at 13:04

Resolve[ForAll[n, n >= 1, Log[n + 1] > Log[n]]]


You can try:

FullSimplify[Log[n + 1] > Log[n], n >= 1,
TransformationFunctions -> {Automatic, Exp}]


True

• Since Exp[expr] is not equivalent to expr, I don't think I'd count it as a valid transformation. We could really take a short cut and use TransformationFunctions -> {Automatic, True &} in this case. :) Jun 23 at 18:18
• I guess this is okay: TransformationFunctions -> {Automatic, # /. r : _Greater :> ApplySides[Exp, r] &} Jun 23 at 18:57
• @MichaelE2 Thanks.
– Syed
Jun 24 at 6:02

Okay, thank you all for your input. I think the simplest approach for obtaining True is:

FullSimplify[Reduce[Log[n + 1] > Log[n], n], n >= 2]


i.e., allowing Reduce to do its mathematical reduction, and then FullSimplify "cleans up" with the assumptions. In (slightly?) more complex cases, Reduce may require the assumption as part of the list of expressions.

As @Nasser mentioned in a comment, simplification in Mathematica tries to minimize the "complexity" of an expression, which is predominantly measured by LeafCount[]. There are two difficulties with Full/Simplify: First, they have only a finite set of transformation functions available and a needed transformation may be missing. Second, they limit how far down rabbit trails they are willing to go in seeking a simpler expression. Consequently, as a discrete global minimization problem, one is not guaranteed to find the minimum.

One can add transformation functions, and if a Simplify is thrown into them, it might take the search further down a trail toward the minimum.

FullSimplify[Log[n + 1] > Log[n], n >= 2,
TransformationFunctions -> {Automatic,
# /. r : _Greater :> Simplify[SubtractSides[r, Last@r], n >= 2] &}]
(*  True  *)


If you throw in echo = (Print[#1]; #1) & as a TransformationFunction, you see some (maybe all) the expressions that are transformed. While both the OP's FullSimplify and mine try Log[1 + 1/n], only mine tries Log[1 + 1/n] > 0 (within the Simplify[] transformation function). And that makes the difference.