# Need help in using Resolve to prove equality over specified domain

Posted 9 years ago
6240 Views
|
4 Replies
|
3 Total Likes
|
 I'm working on a problem from an old textbook that involves composite functions, domains, and equalities that are valid within a given domain. After being given f(x)=1/(1-x), I'm asked to find the domain of a composite function, as shown here: f[x_]:=1/(1-x);FunctionDomain[f@*f@*f@x, x] which gave x < 0 || 0 < x < 1 || x > 1 Then, I'm asked to prove that Composite[f,f,f][x] is equal to x for all x in the domain of Composite[f,f,f][x]. This is how I chose to prove it. Resolve[ForAll[x, Element[x, FunctionDomain[f@*f@*f@x, x]], f@*f@*f@x == x]] Instead of Mathematica returning a "True" or some kind of thumbs-up, it returned Resolve::elemc: Unable to resolve the domain or region membership condition x\[Element](x<0||01). >> So, I tried using Reals for the domain in Element, and Mathematica returned "True". In[17]:= f[x_] := 1/(1 - x); Resolve[ ForAll[x, Element[x, Reals], f@*f@*f@x == x]] Out[17]= True But how can that be? The composite function goes to infinity for x=0 and x=1.It's likely that I don't completely understand the data-types that Resolve, ForAll, Element, and FunctionDomain are using and returning. Or, maybe I completely missed something simple. That's likely, too. How can I make this yield what I expect to see? Thanks! (Notebook attached, too. Problem at the very bottom.) Attachments:
4 Replies
Sort By:
Posted 9 years ago
 Thanks again!
Posted 9 years ago
 That composite certainly does not "go to infinity" at the points 0 and 1. To do so would imply that the limiting values are infinite. Since the composite is the identity nearby, the limiting values are 0 and 1 respectively. Limit[f[f[f[x]]], x -> 0, Direction -> -1] Limit[f[f[f[x]]], x -> 0, Direction -> 1] (*Out[8]= 0 Out[9]= 0 *) Limit[f[f[f[x]]], x -> 1, Direction -> -1] Limit[f[f[f[x]]], x -> 1, Direction -> 1] (* Out[10]= 1 Out[11]= 1 *) 
Posted 9 years ago
 Okay. Quite right about the Limit of the composite going to zero for x->0 (and going to 1 for x->1, for that matter). And, a simple plot of the the composite shows a straight line up through zero and 1 with not even a hiccup. I should have looked a little more carefully before I spoke.However, what I noticed initially was that Mathematica encountered an infinite expression when I tried Composition[f,f,f][x]/.x->0 It still gave me zero as the output (which I didn't notice at first), but I was focused on the infinite expression message as the reason that FunctionDomain gave me a discontinuous domain.Well, obviously (perhaps), that's why "Reals" works as a domain quantifier in the above code. I think you gave me the answer to the problem I was working on. But why doesn't FunctionDomain work as a quantifier in this problem?
Posted 9 years ago
 It just isn't the way Element works. But specification of the desired predicate is easier than you might have thought: just give the inequalities Resolve[ ForAll[x, FunctionDomain[f@*f@*f@x, x], f@*f@*f@x == x]] (* Out[72]= True *)