# Verify that given expr is a general solution to a given ODE

As in the title, for example:

eq = y''[x] + 4 y[x] == 7;
sol = DSolveValue[{eq}, y[x], x]


7/4 + C[1] Cos[2 x] + C[2] Sin[2 x]

Now, to verify that sol is a solution I can do something along:

eq /. y -> Function[x, Evaluate[sol]] // Simplify


True

But that's true for any specific solution, e.g. sol = Sin[2 x] + 7/4.

I could find cases of symbols/constants and verify that there are n of them. But this is not enough because knowing that I could enter sol = Sin[2 x] + 7/4 + C[1] + C[2] so something more clever is needed.

Any ideas?

If your solution needs an assumption about a class of equations it applies to, so be it.

• "If your solution needs an assumption about a class of equations" - I would only say that the linear case is likely to be much easier than the nonlinear one. Feb 15, 2021 at 12:52
• sol = Sin[2 x] + 7/4 + C[1] + C[2] is definitely no solution for C[i] different from zero. MMA gave you the most general one. Feb 15, 2021 at 12:58
• @J.M. yes, I think I don't need more at the moment.
– Kuba
Feb 15, 2021 at 20:55
• @DanielHuber right, I had to leave quickly and didn't pay attention, thanks.
– Kuba
Feb 15, 2021 at 20:56

Assuming you have in mind linear differential equation of n-th order, you have to check two things:

1. That sol is indeed a solution. That you did already.
2. That there are exactly n homogeneous solutions which are linearly independent.

The key here is linear independence. In order to detect the linear dependence between functions you can calculate wronskian

So, the second point can be checked by, for example:

hsol = Coefficient[sol, Union[Cases[sol, _C, All]]];Length[hsol]
wro = FullSimplify[Det[NestList[D[#, x] &, hsol, Length[hsol] - 1]]]


When sol=7/4 + C[1] Cos[2 x] + C[2] Sin[2 x], Length[hsol] evaluates to 2, and wro is nonzero.

When, e.g., sol = (C[1] + C[2]) Sin[2 x] + 7/4, Length[hsol] is again 2, but wro is zero.

UPD: Thanks to Michael E2 comment, it appears that there is a dedicated function for Wronskian, so the second line in my solution can be rewritten as

wro=Wronskian[hsol,x]

• Have you seen Wronskian? Feb 16, 2021 at 15:14
• Can you give a reference to the definition of a general solution used by you, especially to "That there are exactly n homogeneous solutions which are linearly independent"? How these " n homogeneous solutions" are related to sol? TIA. Feb 17, 2021 at 6:05
• @user64494 Hmm, kind of my active knowledge. But why, just check en.wikipedia.org/wiki/Linear_differential_equation around of "In the case of an ordinary differential operator of order n, Carathéodory's existence theorem " Feb 17, 2021 at 8:41
• @RomaLee: Sorry, you still don't answer "How these " n homogeneous solutions" are related to sol?". Feb 17, 2021 at 11:08
• @user64494 Just read my code: they are assumed to enter sol as linear combination with coefficients of the form C[k]. Feb 18, 2021 at 1:10

The complete solution space to a system of ODEs can have a complicated structure, including singular components (e.g. Clairaut equations) and multiple branches. Let us call a solution $$y_{\bf C}$$ a locally general solution to an ODE system with smooth coefficients of dimension $$n$$ at $$(x,{\bf C})=(x_0,{\bf C}_0)$$ to a system of ODEs if the mapping that maps a parameter vector $${\bf C} = (c_1,\,c_2,\dots,\,c_n)$$ to a solution $$y_{\bf C}$$ has an injective derivative at $$(x_0,{\bf C}_0)$$. If a solution to a linear ODE is locally general, then it is the general solution and, furthermore, it is the complete solution in that it represents all possible solutions. Here's a not too well tested implementation of these ideas:

ClearAll[nLocallyInjective];
nLocallyInjective[eq_, sol_, {x_, x0_}, params_List -> p0_List] :=
Module[{ivar, dim, dvars, ics, res, der},
ivar = Flatten@{x};
dim = Length@params;(* Check: Length@p0==dim+1 *)
dvars = NestList[D[#, x] &, sol, dim - 1];
der = D[dvars, {params}] /.
If[Precision[der] == MachinePrecision,
res = Abs[First@Eigenvalues[der, -1]/
Norm[der, Infinity]/$MachineEpsilon/Length@der] > 10, res = Simplify[Det[der] != 0] ]; (* Alt: res=MatrixRank[der]==dim *) res ]; ClearAll[nLocallyGeneralSolution]; nLocallyGeneralSolution[eq_, sol_, y_, {x_, x0_}, p0_List] := Module[{ivar, dvar, dorder, params, dvars, ics, res, der}, ivar = Flatten@{x}; dvar = Flatten@{y}; dorder = Total[InternalProcessEquationsDifferentialOrder[{eq}, ivar, dvar], Infinity]; (* check dimensions *) params = Union@Cases[sol, _C, Infinity]; res = Length[params] == dorder; (* check sol is a solution *) res = res && FullSimplify[ Flatten@{eq} /. Thread[dvar -> (Function @@ {ivar, #} & /@ Flatten@{sol})] // Apply[And]]; (* check locally injective *) res = res && nLocallyInjective[eq, sol, {x, x0}, params -> p0] ];  Examples: eq = y''[x] + 4 y[x] == 7; sol = DSolveValue[{eq}, y[x], x]; nLocallyGeneralSolution[eq, sol, {y}, {x, 0}, {0, 0}] (* True *) eq = y''[x] + 4 y[x]^2 == 7; sol = DSolveValue[{eq}, y[x], x]; nLocallyGeneralSolution[eq, sol, {y}, {x, 0}, N@{1, 1}] (* True *)  • Can you give a reference to " Let us call a solution$y_{\bf C}$a locally general solution at$(x,{\bf C})=(x_0,{\bf C}_0)$to a system of ODEs if the mapping that maps a parameter vector${\bf C} = (c_1,\,c_2,\dots,\,c_n)$to a solution$y_{\bf C}$has an injective derivative at$(x_0,{\bf C}_0)\$"? TIA. Feb 17, 2021 at 6:03
• @user64494 It's an ad hoc def. See for instance V.I. Arnold's rectifiability theorem in his ODEs book. Feb 17, 2021 at 13:46
• " V.I. Arnold's rectifiability theorem in his ODEs book" is not a reference used by civilized people (no Chap, Par, and/or page). I will be waiting for a serious and solid reply of you. Your "ad hoc" also does not make a good impression. Feb 17, 2021 at 14:06
• Unfortunately, your approach fails with eq1 =x^2*y''[x]+x*y'[x]+(x^2-2^2)*y[x]==0;sol1 = DSolveValue[{eq1}, y[x], x];nLocallyGeneralSolution[eq1, sol1, {y}, {x, 0}, N@{1, 1}],whereas the approach from my answer works. Feb 17, 2021 at 15:10
• @user64494 The answer to your example should be failure (or False). If your method says it's locally general, then your method is wrong. Quit wasting people's time with frivolous nonexamples. Feb 17, 2021 at 15:38

According to Encyclopedia of Mathematics, in order to prove that sol from

eq = y''[x] + 4 y[x] == 7;sol = DSolveValue[{eq}, y[x], x]


is a general solution of eq one should prove that sol is a solution of eq for any C[1] and C[2] (done in the question) and any Cauchy problem has a (unique) solution, more exactly,

ForAll[{x0, d1, d2},  Exists[{C[1],   C[2]}, (sol /. x -> x0) == d1 &&
(D[sol, x] /. x -> x0) == d2]];


Unfortunately,

Resolve[%, Reals]


fails since nonalgebraic equations are under its consideration. However, we can directly check it in such a way.

Solve[7/4+C[1] Cos[2 x0] + C[2] Sin[2 x0] == d1 &&
2 C[2] Cos[2 x0] - 2 C[1] Sin[2 x0] == d2, {C[1],C[2]}] // FullSimplify


{{C[1] -> 1/4 ((-7 + 4 d1) Cos[2 x0] - 2 d2 Sin[2 x0]), C[2] -> 1/4 Cos[2 x0] (2 d2 + (-7 + 4 d1) Tan[2 x0])}}

Note that the deteminant of the above system equals 1 and the singularities in C[2], when Tan[2x0] does not exist, are removable.