I'm trying to define the derivative of a function H to be positive. I'm using
But I get the error
TagSetDelayed::tagpos: Tag H in Positive[H'[x]] is too deep for an assigned rule to be found.
I also tried defining a new function Hp which is H':
Hp /: Positive[Hp[x]] := True
But then I get:
TagSetDelayed::tagnf: Tag Hp not found in Positive[H'[x]].
I also tried wrapping Hp in Hold, but I get the "too deep" error as before.
How can I declare it to be positive?