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

Question

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.

Answer 1

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]

Answer 2

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}] /. 
     Thread[Join[ivar, params] -> Flatten@{x0, p0}];
   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[Internal`ProcessEquations`DifferentialOrder[{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  *)

Answer 3

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.