Hi @AlbertRich , I was told (by @halirutan ) that you could probably give me a hint to a problem I have.
The question is:
How to verify that something is a general solution to a diff equation? Automatically, in WL, of course.
I know that I can substitute and simplify to verify a specific solution.
But the problem with general is that it has n symbolic constants.
A Sin[t] + B Cos[t] is a general solution, how to verify that
A1 Sin[t] + A2 Cos[t] is too and
A Sin[t] + A Cos[t] is not?
The point is, is there a standard method to do so? If not, I will try to cook something up
Probably based on
Simplify[ exampleGeneralSol - giveGeneralSol] and analyzing
constant - otherConstant terms. Not sure how easy it will be.
I am not an expert on ODE's either other than what I learned from classes I took on the subject and from writing a program that solves ODE's step by step for 2 years now, which is still in progress.
But this is what I think could be done: First determine the order of the ODE.
Next, count the number of unique constants of integrations in the candidate solution. If number of unique constants is not the same as the order of the ODE, then reject it right away. To do this one must use convention as to what the constant of integrations are.
In Mathematica, it uses
C, C, etc... in Maple, it looks for
_C1, _C2, etc.... (It needs to know this, so not to confuse the constant of integrations with other parameters).
Next, if the number of constants of integrations is the same as the order, then the standard way, is as you said. Replace and simplify:
Replace the candidate solution (and all needed derivatives) in the ODE. If you get zero, then it is a general solution. If not, then one would need to simplify the difference to see if the difference is equivalent to zero or not.
Sometimes if the solution is complicated, this simplification could fail to give zero, even though the solution could be correct and it is actually zero.
This is a hard problem. This now becomes a problem of simplification to determine if an expression is zero or not. This is known problem in computer algebra. To determine the equivalence of expressions.
I made a post about many such cases in Maple, where it can't verify its own solution is a general solution to an ODE, even though the solution is actually correct. In Mathematica one can use
FullSimplify and other tricks to check more if it is not zero.
DSolve[y'[x] == Sqrt[x + y[x]] - 1, y, x]
1/4 (-4 x + x^2 + 2 x A + B)
If the solution is a linear combination of the constants
Int[Surd[x_, -1], x_] := Simp[Log[x], x] Int[Surd[x_, n_Integer], x_] := If[n>0, (n/(n+1))*x*Surd[x,n], ((-n/(-n-1))*x)/Surd[x, -n]] /; FreeQ[n, x] && NeQ[n, -1]
x^m Surd[x,n]^pwhere m is a positive integer, and n and p can be numeric or symbolic. Then you could post this add-on package to Rubi making it available to the Rubi community.
_.pattern object for
pto unify your first two rules.
symja_android_library's rule dump in their repo and that seems attractive.
MathematicaSyntaxTestSuitewould also help loads.