本日のC.A.D.

今回は，第一種 Chebyshev 多項式 $T_4(x)=64x^7-112x^5+56x^3-7x$ に関する

$\exists a\ \exists b\ \exists c\ \forall x\ (\, -1\le x\le1 \to 64 x^7+a x^5+b x^3+c x\le m\,)\quad \cdots\quad (*)$

が $1\le m $ と等価であるという性質です．

まず

$\forall x\ (\, -1\le x\le1 \to 64 x^7+a x^5+b x^3+c x\le 1\,)$

が $a=-112\ \land\ b=56\ \land\ c=-7$ と等価であることは

? tst12([all],[c,a,b,x],imp,"x^2<=1,64*x^7+a*x^5+b*x^3+c*x<=1");Ans(1);
 *** using Lazard's method (MPP17).
[x,3]
[b,3]
[a,6]
[c,25]
time = 14,301 ms.
151 4461(14,161) 55129(267,4271) 11(36373,18580) 
 *** combined adjacent 10 cells.
1[c = [c+7,1],a = [a+112,1],b = [b-56,1],true]
time = 2min, 31,786 ms.

のように判るので，$1\le m $ ならば $(*)$ を得ます．そして

$\forall x\ (\, -1\le x\le1 \to 64 x^7+a x^5+b x^3+c x< 1\,)$

が false と等価であることも

? tst12([all],[c,a,b,x],imp,"x^2<=1,64*x^7+a*x^5+b*x^3+c*x<1");Ans();
 *** using Lazard's method (MPP17).
[x,3]
[b,3]
[a,6]
[c,25]
time = 14,440 ms.
151 4461(14,161) 55129(267,4271) 0(36373,18580) 
1[false]
time = 2min, 30,091 ms.

のように判るので，$(*)$ ならば $1\le m $ を得ます．また，前半の結果を用いるなら，後半は

? tst12([ex],[v,x],and,"x^2<=1,64*x^7-112*x^5+56*x^3-7*x==v");Ans();
 *** using Lazard's method (MPP17).
[x,3]
[v,2]
time = 42 ms.
5 3(12,4) 
 *** combined adjacent 2 cells.
1[[v+1,1] <= v <= [v-1,1],true]
time = 21 ms.

のように $1$ が値域に属することから容易に得られます．

Wolfram Language 12.3.0 Engine for Linux x86 (64-bit)
Copyright 1988-2021 Wolfram Research, Inc.

In[1]:= Resolve[ForAll[x,x^2<=1,64*x^7+a*x^5+b*x^3+c*x<=1],Reals,WorkingPrecision->50]//Timing                   

Resolve::cadpr: The cylindrical algebraic decomposition algorithm used by Resolve
     failed due to a too low WorkingPrecision. Increasing the value of WorkingPrecision may allow the algorithm
     to succeed.

Out[1]= {22.957144, ForAll[{x}, x^2 <= 1, c*x + b*x^3 + a*x^5 + 64*x^7 <= 1]}

In[2]:= Resolve[ForAll[x,x^2<=1,64*x^7+a*x^5+b*x^3+c*x<=1],Reals,WorkingPrecision->100]//Timing                  

Out[2]= {77.871964, a == -112 && b == 56 && c == -7}