How to solve a conditional inequality?

Question

I am trying to use Mathematica to solve a conditional inequality.

Find all (real) numbers $a$ and $b$ such that $|a| + |b| \ge 2/ \sqrt{3}$ and for any real $x$ the inequality $ |a\sin x + b \sin 2x| \le 1 $ holds

See here for more info.

I tried the expression

Reduce[{ForAll[{x}, Abs[a*Sin[x] + b*Sin[2 x]] <= 1] && 
  Abs[a] + Abs[b] >= 2/Sqrt[3]}, {a, b}, Reals]

Unfortunately, the above expression is running for a few hours without any output. Is there a better way to solve the problem?

Answer 1

Perhaps

sol = Reduce[ForAll[{u}, -1 <= u <= 1 \[Implies] 
   Abs[a*u + b*2 u Sqrt[1 - u^2]] <= 1 && 
    Abs[a*u - b*2 u Sqrt[1 - u^2]] <= 1 && 
    Abs[a] + Abs[b] >= 2/Sqrt[3]], {a, b}, Reals]
(*
  (a == -(4/(3 Sqrt[3])) && (b == -(2/(3 Sqrt[3])) || b == 2/(3 Sqrt[3]))) ||
   (a ==  4/(3 Sqrt[3])  && (b == -(2/(3 Sqrt[3])) || b == 2/(3 Sqrt[3])))
*)

Polynomial systems are usually easier and Sqrt can be often be converted. If the degree is not too high, you can get a result. Here we can replace Sin[x] -> u and Sin[2x] == 2 Sin[x] Cos[x] -> 2 u * (± Sqrt[1 - u^2]), where ± is to be interpreted such that both resulting inequalities must be satisfied. This is because all combinations of signs of sine and cosine are possible if x ranges over all real numbers.

[The simplicity of the answer suggests that perhaps a simple mathematical solution might exist, but I have to go. Someone else?]