# Find a function for which an inequality is always true: performance problems

I have this inequality which compares paths of two motions against time $$t$$:

Machine-generated code:

Piecewise[{{Times[Divide[1, 2], Plus[Times[aRx, Power[t, 2]], Times[2, t, vR0]]], And[GreaterEqual[t, 0], LessEqual[t, rho]]}, {Times[Divide[1, 2], Plus[Times[-1, aRx, Power[rho, 2]], Times[-1, bRx, Power[rho, 2]], Times[2, aRx, rho, t], Times[2, bRx, rho, t], Times[-1, bRx, Power[t, 2]], Times[2, t, vR0]]], And[GreaterEqual[t, rho], LessEqual[t, Times[Power[bRx, -1], Plus[Times[aRx, rho], Times[bRx, rho], vR0]]]]}}] <= Times[Divide[1, 2], Plus[Times[2, d], Times[-1, bFx, Power[t, 2]], Times[2, t, vF0]]]


I am interested in relations between the constants $$\rho > 0, v^F_0 > 0, v^R_0 > 0,$$ $$b^F_x > 0, a^R_x > 0, b^R_x > 0, d > 0$$ (i.e. all variables in the equation except for the time $$t$$). Specifically, I want to find $$D(\rho, v^F_0, v^R_0, b^F_x, a^R_x, b^R_x)$$ such that $$d \ge D$$ is true iff the inequality above is always true in the time period

Code:

0 < t && t < Times[Power[bRx, -1], Plus[Times[aRx, rho], Times[bRx, rho], vR0]]


Using Wolfram Engine, I tried both solutions from Solution such that an inequality is true in the whole domain, i.e. Reduce[ForAll[]]:

Reduce[ForAll[t, 0 < t && t < Times[Power[bRx, -1], Plus[Times[aRx, rho], Times[bRx, rho], vR0]], Piecewise[{{Times[Divide[1, 2], Plus[Times[aRx, Power[t, 2]], Times[2, t, vR0]]], And[GreaterEqual[t, 0], LessEqual[t, rho]]}, {Times[Divide[1, 2], Plus[Times[-1, aRx, Power[rho, 2]], Times[-1, bRx, Power[rho, 2]], Times[2, aRx, rho, t], Times[2, bRx, rho, t], Times[-1, bRx, Power[t, 2]], Times[2, t, vR0]]], And[GreaterEqual[t, rho], LessEqual[t, Times[Power[bRx, -1], Plus[Times[aRx, rho], Times[bRx, rho], vR0]]]]}}] <= Times[Divide[1, 2], Plus[Times[2, d], Times[-1, bFx, Power[t, 2]], Times[2, t, vF0]]]] && vF0 > 0 && vR0 > 0 && bFx > 0 && rho > 0 && aRx > 0 && bRx > 0, d, Reals]


and Reduce[Minimize[]]:

Reduce[Minimize[{(Times[Divide[1, 2], Plus[Times[2, d], Times[-1, bFx, Power[t, 2]], Times[2, t, vF0]]]) - (Piecewise[{{Times[Divide[1, 2], Plus[Times[aRx, Power[t, 2]], Times[2, t, vR0]]], And[GreaterEqual[t, 0], LessEqual[t, rho]]}, {Times[Divide[1, 2], Plus[Times[-1, aRx, Power[rho, 2]], Times[-1, bRx, Power[rho, 2]], Times[2, aRx, rho, t], Times[2, bRx, rho, t], Times[-1, bRx, Power[t, 2]], Times[2, t, vR0]]], And[GreaterEqual[t, rho], LessEqual[t, Times[Power[bRx, -1], Plus[Times[aRx, rho], Times[bRx, rho], vR0]]]]}}]), 0 < t && t < Times[Power[bRx, -1], Plus[Times[aRx, rho], Times[bRx, rho], vR0]] && vF0 > 0 && vR0 > 0 && bFx > 0 && rho > 0 && aRx > 0 && bRx > 0}, t][[1]] >= 0 && vF0 > 0 && vR0 > 0 && bFx > 0 && rho > 0 && aRx > 0 && bRx > 0]


However, due to long computation times, I interrupted both calculations after about half an hour.

I wonder if there is a method of formalising the problem (for at least the case of piecewise quadratic functions as above) which does not cause such performance problems.

EDIT: I forgot to add one more constraint: $$b^F_x > b^R_x$$.

• Your piece-wise expression depending on 6 parameters is too complex for both approaches. If you put aRx = 2; vR0 = 1; bRx = 4; Fx = 1; rho = 3; bFx = 3;, then Reduce[ForAll...] produces d >= 1359/32 as well as REduce[Minimize...]. Jun 30, 2022 at 19:16
• The Reduce[Minimize...] approach works for R0 = 1; bRx = 4; Fx = 1; rho = 3;. The result is too long to be presented here. Jun 30, 2022 at 19:35

# Edit, Answer with $$b_x^F>b_x^R$$

Simplest solution. Redefine your inequality so it's $$f(t)\leq d$$

f[t_] = Piecewise[{{(aRx*t^2 + 2*t*vR0)/2 + (bFx*t^2)/2 - t*vF0,
t >= 0 && t <= rho},
{(-(aRx*rho^2) - bRx*rho^2 + 2*aRx*rho*t + 2*bRx*rho*t -
bRx*t^2 + 2*t*vR0)/2 + (bFx*t^2)/2 - t*vF0,
t >= rho && t <= (aRx*rho + bRx*rho + vR0)/bRx}}, 0];


Set up the constraints

tmax = (aRx*rho + bRx*rho + vR0)/bRx;
cons = And @@ Flatten[{Thread[vars > 0], bFx > bRx}];
const = 0 < t && t <= tmax;


Note that $$f$$ is strictly concave up under these constraints

Simplify[(D[f[t], {t, 2}] >= 0), cons && const] (*True*)


This means the maximum value of $$f(t)$$ is at one of the ends of your time interval, i.e. $$t=0$$ or $$t=t_{\max}$$, and you're done.

dbound = Max[Simplify[f[0], cons], Simplify[f[tmax], cons]]


Which matches the other solutions below and gives a tight bound on $$d$$.

## First Edit

The key is to simplify as much as possible before trying to call Reduce.

Clear[f, g, tmax]
f = Piecewise[{{(aRx*t^2 + 2*t*vR0)/2, t >= 0 && t <= rho}, {(-(aRx*rho^2) - bRx*rho^2 + 2*aRx*rho*t + 2*bRx*rho*t - bRx*t^2 + 2*t*vR0)/2,
t >= rho && t <= (aRx*rho + bRx*rho + vR0)/bRx}}, 0];
g = (2*d - bFx*t^2 + 2*t*vF0)/2;

ineq = f <= g;

tmax = (aRx*rho + bRx*rho + vR0)/bRx;
vars = {rho, aRx, vR0, bRx, bFx, vF0, d};


const = 0 < t && t <= tmax;
cons = And @@ Flatten[{Thread[vars > 0], bFx > bRx}];


"Solve" your inequality for $$d$$ given the constraints

dsol = Refine[Reduce[ineq, d], cons && const] (*0.2s on my machine*)


Resolve this solution for all times in the interval

resolve = Simplify[Resolve@ForAll[t, const, ineqd], cons] (*0.2s*)


Reduce again to get back to inequalities for $$d$$

reduce = Refine[Reduce[red, d], cons] (*6.5s*)


This gives 2 possibilities

Fortunately, we can show the 2nd possibility is never valid under our constraints. Let's split up the possibilities and check for solutions. Here's a hack way to do it

sols = reduce /. Or -> List /. GreaterEqual[d, x__] -> Equal[d, x]


Then we have

Reduce[Last[sols] && cons]==False


Note that this is not False if we remove the $$d\geq 0$$ constraint, so we can simply discard the final solution as long as we enforce $$d\geq 0$$ manually at the end, e.g. with Max. This then immediately gives the answer:

dbound = Max[0,Last@Last@First@sols];


Which is the same as in the original answer when $$b_x^F>b_x^R$$.

This is a lower bound, $$D=$$dbound, on $$d$$ which is tight. That is, $$d\geq D$$ iff your inequality holds true and furthermore, setting $$d=D$$ guarantees that the two sides of your inequality will be equal for some $$t$$ between $$0$$ and $$t_{\text{max}}$$ - actually at $$t=0\to D=0$$ or $$t=t_{\max}$$ since $$b_x^F>b_x^R$$ enforces a certain concavity as explained in the original answer below.

## TL;DR - use

d1[aRx_, vR0_, rho_, bRx_, bFx_, vF0_] = 1/2 (-aRx rho (rho - 2 t) - bRx (rho - t)^2 + t (bFx t - 2 vF0 + 2 vR0));
dbound[aRx_, vR0_, rho_, bRx_, bFx_, vF0_] := Block[{d1a, tmax, tm, t},
tmax = (aRx rho + bRx rho + vR0)/bRx;
d1a = d1[aRx, vR0, rho, bRx, bFx, vF0];
Max[0, If[bFx >= bRx, d1a /. t -> tmax,
tm = t /. First@Solve[D[d1a, t] == 0, t];
If[tm > tmax, d1a /. t -> tmax, d1a /. t -> tm]]]
]


How tight do you need this bound?

f=Piecewise[{{Times[Divide[1,2],Plus[Times[aRx,Power[t,2]],Times[2,t,vR0]]],And[GreaterEqual[t,0],LessEqual[t,rho]]},{Times[Divide[1,2],Plus[Times[-1,aRx,Power[rho,2]],Times[-1,bRx,Power[rho,2]],Times[2,aRx,rho,t],Times[2,bRx,rho,t],Times[-1,bRx,Power[t,2]],Times[2,t,vR0]]],And[GreaterEqual[t,rho],LessEqual[t,Times[Power[bRx,-1],Plus[Times[aRx,rho],Times[bRx,rho],vR0]]]]}}];
g=Times[Divide[1,2],Plus[Times[2,d],Times[-1,bFx,Power[t,2]],Times[2,t,vF0]]];
tmax=Times[Power[bRx,-1],Plus[Times[aRx,rho],Times[bRx,rho],vR0]];


and constraints (const is in that form because Mathematica reduces smarter that way, don't ask me why).

const = 0 < t && Refine[Reduce[t <= tmax, VR0], cons && t > 0];
cons = And @@ Thread[{rho, aRx, vR0, bRx, bFx, vF0, d} > 0];
ineq = f <= g;


We can immediately "solve" this for $$d$$

ineqd = Refine[Reduce[ineq, d], cons && const]


giving 2 possibilities for $$D$$ depending on if $$t<\rho$$ or $$t>\rho$$.

If $$t>\rho$$ we have $$d\geq\frac{1}{2} \left(t^2 b_x^F-\rho (\rho -2 t) a_x^R-(\rho -t)^2 b_x^R\right)=d_1(t)$$

If $$t<\rho$$ we have $$d\geq\frac{1}{2} t (t (a_x^R+b_x^F)-2 v_0^F+2 v_0^R)=d_2(t)$$

which we store as ds = Last[Last[#]] & /@ List @@ (ineqd)

If you don't need a tight bound, note that

FullSimplify[Reduce[First@ds <= Last@ds], cons && const] is True so $$d_2(t)\geq d_1(t)$$ for all $$t$$. Thus for a loose bound, we can simply ignore $$d_1(t)$$. Further note that FullSimplify[D[Last@ds, {t, 2}] > 0, cons] is True so $$d_2(t)$$ is concave up in $$t$$ meaning its maximum is either $$d_2(0)=0$$ or $$d_2(t_{\text{max}})$$ meaning we have

$$d\geq \max{0,\frac{\left(\rho \left(a_x^R+b_x^R\right)+v_0^R\right) \left(a_x^R \left(\rho \left(b_x^F+b_x^R\right)+v_0^R\right)+\rho \left(a_x^R\right)^2+b_x^F \left(\rho b_x^R+v_0^R\right)+2 \left(v_0^R-v_0^R\right) b_x^R\right)}{2 \left(b_x^R\right)^2}}.$$

However, this is less tight of a bound than is possible given your initial inequalities. It gets a bit ugly if you want to tighten it up.

Since $$d_1(t)\leq d_2(t)$$ and $$d_2(t)$$ stops being valid when $$t>\rho$$, you know the maximum of $$d_1(t)$$ in $$\rho is the "true" lower bound on $$d$$.

If $$d_1(t)$$ is concave up or linear, i.e. D[First@ds, {t, 2}] >= 0 or $$b_x^F\geq b_x^R$$, then the maximum of $$d_1(t)$$ in $$\rho is $$d_1(t_{\text{max}})$$ or $$d_1(t)$$ is strictly negative in this interval and we take $$d=0$$. This can be verified by the fact that Reduce[And[Flatten[{(First@ds /. t -> rho) > (First@ds /. t -> tmax), (First@ds /. t -> rho) >= 0, bFx > bRx, cons}]]] is False

If $$d_1(t)$$ is concave down, i.e. $$b_x^F, $$d_1(t)$$ has a maximum, call it $$t_m$$. Either $$t_m<\rho$$, $$t_m>t_{\text{max}}$$ or $$t_m$$ is somewhere between. If $$\rho\leq t_m \leq t_{\text{max}}$$ then $$d\geq\max{0,d_1(t_m)}$$ is your solution. If $$t_m<\rho$$, $$d>0$$ is your solution because

tm = t /. First@Solve[D[First@ds, t] == 0, t];
Reduce[And[Flatten[{(First@ds /. t -> rho) > (First@ds /. t -> tmax), (First@ds /. t -> rho) >= 0, bFx < bRx, cons, rho > tm > tmax}]]]


gives False tells you that $$d_1(t)$$ is strictly negative in this interval.

And finally if $$t_m > t_{\text{max}}$$ then $$d\geq\max{0,d_1(t_{\text{max}})}$$ is your solution.

So putting it all together

d1[aRx_, vR0_, rho_, bRx_, bFx_, vF0_] = First@ds;
dbound[aRx_, vR0_, rho_, bRx_, bFx_, vF0_] := Block[{d1a, tmax, tm, t},
tmax = (aRx rho + bRx rho + vR0)/bRx;
d1a = d1[aRx, vR0, rho, bRx, bFx, vF0];
Max[0, If[bFx >= bRx, d1a /. t -> tmax,
tm = t /. First@Solve[D[d1a, t] == 0, t];
If[tm > tmax, d1a /. t -> tmax, d1a /. t -> tm]]]
]


gives you a lower bound, $$D=$$dbound, on $$d$$ which is tight. That is, $$d\geq D$$ iff your inequality holds true and furthermore, setting $$d=D$$ guarantees that the two sides of your inequality will be equal for some $$t$$ between $$0$$ and $$t_{\text{max}}$$.

• When I typed ineqd into WE, I got a piecewise $d_1(t)$ depending on $v^R_0 < -(a^R_x \rho) - b^R_x \rho + b^R_x t$. How did you obtain such an equation of $d_1(t)$? Also, I forgot to add a constraint $b^F_x > b^R_x$. Jul 1, 2022 at 13:18
• Reduce should never return Piecewise. It should give you an expression with And and Or. Is that not what you get? Jul 1, 2022 at 13:31
• It's given in the answer. ds = Last[Last[#]] & /@ List @@ (ineqd). Then $d_1=$First@ds. I'm working on an update to the answer. With the constraint $b_x^F>b_x^R$ everything becomes simple. Jul 1, 2022 at 14:36
• @scriptfoo, realized with the new constraint the problem is even simpler than I thought. Final edit made, very simple answer :) Jul 1, 2022 at 15:46
• This is only one of many cases, the other may not have that constraint, so the original answer still contains useful information. Jul 1, 2022 at 15:51