Quantifier Elimination with Mathematica #１
 ー東大入試を　１行で　解くー

2018 年4月8日   Cabri研究会  生越　茂樹

QEのコマンド

１．最大・最小

example1&example1’

Exists[{y}, 2*x^2 + 4*x*y + 3*y^2 + 4*x + 5*y - 4 == 0];
Resolve[%, Reals]

Exists[{x,y},2x^2+4x y+3y^2+4x+5y-4==0&&x+y==k];
Reduce[%,Reals]

example2

ForAll[{x,y},x>0&&y>0\[Implies]Sqrt[x]+Sqrt[y]≤k Sqrt[2x+y]];
Resolve[%,Reals]

example3

ForAll[{x,y},-1≤x≤1&&-1≤y≤1\[Implies]1-a x-b y-a x y>0];
Reduce[%,Reals]

RegionPlot[%,{a,-2,2},{b,-2,2},Axes->True]
Manipulate[Plot3D[1-a x-b y- a x y,{x,-1,1},{y,-1,1}],{a,-2,2},{b,-2,2}]

example4 (パラメータを含む場合)

Exists[{x,y},a>0&&y≥x^2&&y≤-2x^2+3 a x+6a^2&&k==x+y];
Reduce[%,Reals]

example5 (パラメーターが二つ以上あるときは結果が非常に複雑)

Clear[a,b]
Exists[{x,y},x^2+y^2≤25&&2x+y≤5&&k==x^2+y^2- 2 a x-2 b y];
Resolve[%,Reals]

● MinValue の方が時間がかかる(約10分) が，やや綺麗に出力される．

MinValue[{x^2+y^2-2a x-2 b y,x^2+y^2≤25&&2x+y≤5},{x,y}]//Timing

2．通過領域

example6

Exists[a,a>0&&y==a*x^2+(1-4a^2)/(4a)];
reg=Reduce[%,Reals]

RegionPlot[reg,{x,-5,5},{y,-5,5},Axes->True]

Manipulate[Plot[{a*x^2+(1-4a^2)/(4a),Sqrt[x^2-1],-Sqrt[x^2-1]},{x,-5,5},PlotRange->{{-5,5},{-20,20}}],{a,0.1,30}]

3．真偽判定

example7 (整数問題だが解ける)

ForAll[n,n>0\[Implies]n^3/26+100≥n^2];
Resolve[%,Integers]
ForAll[{n,m,l},5n+5m+3l==1\[Implies]10n m+3 m l+3 n l<0];
Resolve[%,Integers]

example8 (整数問題は通常解けない)

ForAll[m, m^2-(a-1)m+n^2/(2n+1)a>0&&a∈Reals&&n>0];
Reduce[%,Integers]

4．総合問題

example9 (最大・最小)

C上の点を(x,y,0),　l上の点を(a,0,0)+t(0,1,1)=(a,t,t)　とおく

Exists[{x,y,t},(a-x)^2+(t-y)^2+t^2==k^2&&x^2+y^2==1&&a≥0&&k≥0];
reg=Reduce[%,{a,k},Reals]
RegionPlot[reg,{a,0,3},{k,0,2}]

example10 (最大・最小)

Exists[{s,t},s^2+t^2==1,x^4-2(s+t)x^2+(s-t)^2==0];
Resolve[%,Reals]

example11 (通過領域)

A(p,q,0),B(x,y,z)とおくと,C(0,0,1)が線分AB上より　(OverVector[AB])=t(OverVector[AC])↔(({{x-p}, {y-q
z}}))=t(({{-p}, {-q
1}}))　(t>1).

ClearAll["Global`*"]

Exists[{p,q,t},{x-p,y-q,z}==t{-p,-q,1}&&z>1&&(x-p)^2+(y-q)^2+z^2==4];
surface=Resolve[%,Reals]

(*((上の式からx)^2)+(y^2)をzの式で表すと，x^2+y^2=(4-8z+3z^2+2z^3-z^4)/z^2 となるから体積と概形は*)
v=Integrate[Pi(4-8z+3z^2+2z^3-z^4)/z^2,{z,1,2}]

ContourPlot3D[-4+8 z-3 (z^2)+(x^2) (z^2)+(y^2) (z^2)-2 (z^3)+(z^4)==0,{x,-1/2,1/2},{y,-1/2,1/2},{z,1,2}]

もっと自動的にやってみる．領域を作り，RegionMeasure で計算する．変数の順序に注意!

線分CB上の点をR(X,Y,Z)とすると，(OverVector[CR])=u(OverVector[CB])↔(({{X}, {   Y
Z-1}}))=u(({{x}, {   y
z-1}}))(0<u<1) だから，

Clear[x,y,z,u];
Exists[{x,y,z,u},{X,Y,Z-1}==u{ x,y,z-1}&&0<u<1&&surface];
pred=Resolve[%,Reals]//FullSimplify
region=ImplicitRegion[pred,{Z,X,Y}];(*{X,Y,Z}では計算できない．{Z,Y,X}はOK*)
RegionMeasure[region]

最後に

■最大･最小値だけなら Maximize/Minimize, MaxValue/MinValue.
また変数の値が１つに決まるときはSolve を使った方が良いことが多い．


■一般にはQEは実数かつ多項式の系以外には使えないとされている． しかしMathematicaでは　使える場合もある. 
例えば複素数の場合は Resolve[%, Complexes] と,   a∈Reals, (a|b) ∈Reals  などを組み合わせると，使える事が多い.

(i)「 x>0 のとき (((1 + (1/x)))^x)<e<(((1+(1/x)))^(x+(1/2)))  を示せ 」   （2016年理)

ForAll[x,x>0\[Implies](1+1/x)^x<E<(1+1/x)^(x+1/2)]
Resolve[%,Reals]

(ii) 「　(x^2)+(2m+3i)x+(8-6i)=0　が実数解を持つような　実定数m の値を定めよ．」

Exists[x,x^2+(2m+3I)x+(8-6I)==0&&(m|x)∈Reals]
Resolve[%,Complexes]

■工学ではQEは「最適化問題」によく応用されている．
入試問題を解く道具としては，特に「最大･最小問題」，「図形と式」，「方程式・不等式」の分野に有効．
しかし「確率」ではまったく使えない．「整数」でもごく一部しか使えない．
このように万能ではないが，QEは「可視化」，「計算(特に微積分)」 にならぶ強力な武器になる．(3種の神器?)

5. （おまけ）これらも一行で解ける

【方程式の解】 正三角形PQRが放物線y = (x^2) に内接し，QRの傾きが(Sqrt[2])の時，１辺の長さを求めよ．(2004 年)  
これは Solve でも解ける.

P(p,(p^2)),Q(q,(q^2)),R(r,(r^2))とおくと QRの傾きは q+r. さらに１辺の長さを a とおく．

Exists[{p,q,r},p≠q&&q≠r&&r≠p&&(p-q)^2+(p^2-q^2)^2==(q-r)^2+(q^2-r^2)^2==(r-p)^2+(r^2-p^2)^2==a^2&&r+q==Sqrt[2]&&a>0]//Resolve

【最大・最小】 (x^3) - 2 (x^2) - 3 x + 4 (-(7/4)≦ x ≦ 3) の最大・最小値を求めよ．(1991 年)

Exists[x,x^3-2x^2-3x+4==k&&-7/4≤x≤3];
Resolve[%,Reals]

【軌跡】 z = (y^2), x = 0 上に動点Qをとる．さらに定点P (2, 0, 1) としたとき，直線PQ と xy平面との交点Rの軌跡を求めよ.(1991 年)

Q(0,t,(t^2)),R(x,y,0)とおくと  (OverVector[PR])=s(OverVector[PQ])

Exists[{t,s},{x-2,y,-1}==s{-2,t,t^2-1}];
curve=Resolve[%,Reals]
RegionPlot[ImplicitRegion[%,{x,y}],Axes->True]

【連立方程式が特定の解を持つ条件】 y = k (x - (x^3)), x = k (y - (y^3)) が第1象限内でy = x上にない交点を持つ正の数kの範囲を求めよ.(1989 年)

Exists[{x,y},y==k(x-x^3)&&x==k (y-y^3)&&x≠y&&k>0&&x>0&&y>0]
Resolve[%,Reals]

【円と放物線】 円：(x^2) + (((y - a))^2)=(r^2)(a, r>0) が y≥(x^2) に含まれるとき，rの範囲をaの式で表せ．(有名問題)

ForAll[{x,y},x^2+(y-a)^2≤r^2\[Implies]y≥x^2&&a>0&&r>0];
Resolve[%,{a,r},Reals]

【最小値】 長さl (l ≧ 1) の線分が その両端をy = (x^2) の上に置いている時，線分の中点Mがx軸に最も近い場合のMのy座標を求めよ.(1974 文理 改)

Exists[{p,q},(p-q)^2+(p^2-q^2)^2==l^2&&y==(p^2+q^2)/2&&l≥1]//Resolve[#,Reals]&

【存在条件】 f (x) = (ax^3) + (bx^2) + cx + d が 3条件
(イ) f (-1) = 0,　 (ロ) f (1) = 0,  (ハ)| x | ≦ 1の時 f (x) ≧ 1 - | x |　
をみたすのは，定数a, b, c, dがどのような条件をみたすときか？ (1981 理)

Clear[f,x,a,b,c,d];f[x_]=a x^3+b x^2+c x+d;
ForAll[x,(Abs[x]≤1\[Implies]f[x]≥1-Abs[x])&&f[1]==f[-1]==0]//Reduce[#,Reals]&

【通過領域】 A (((2((t^2)+t+1))/(3 (t+1))), -2),  B ((2/3)t, -2 t)  と定める．t が 0 ≦ t ≦ 1 を動くとき 直線AB の通過領域を求めよ． (1997 文)

(*AB:y=-2t^3+3xt^2-3x となるので*)
Exists[t,y==-2t^3+3 x t^2-3 x&&0≤t≤1]//Resolve[#,Reals]&//FullSimplify
RegionPlot[%,{x,-3,4},{y,-4,4}]

【通過領域】 P ((1/2), (1/4)), y = (x^2)上の2点Q (a, (a^2)), R (b, (b^2)) を PQ = PR となるように動かすとき △PQRの重心G (X, Y) の軌跡を求めよ． (2011 理)

Exists[{a,b},(a-1/2)^2+(a^2-1/4)^2==(b-1/2)^2+(b^2-1/4)^2&&X==1/3(a+b+1/2)&&Y==1/3(a^2+b^2+1/4)]//Resolve[#,Reals]&//FullSimplify
RegionPlot[ImplicitRegion[%,{X,Y}]]

【通過領域】 A (-1, 1), B (1, -1), P (x, y) (| x | ≦  1) に対し次の (1) または (2) をみたすP の存在範囲を求めよ．
(1) 頂点のx座標の絶対値が1以上の2次関数でA, B, P を通るものが存在する．
(2) A, P, B は一直線上にある (2015 年文）．

Clear[a,p,q,f,x]
f[x_]=a (x-p)^2+q;
Exists[{a,p,q},(1==f[-1]&&-1==f[1]&&Y==f[X]&&-1≤X≤1&&Abs[p]≥1)||Y==-X];
Resolve[%,Reals]//FullSimplify
RegionPlot[%,{X,-1,1},{Y,-1,1},Axes->True]

【条件付最大最小】

Vは底面が図の斜線部分，高さがbの柱体になるので volume(V)=((π/4)((a^2)+(c^2))+ac) b

Exists[{a,b,c},a+b+c==1&&a>0&&b>0&&c>0&&(Pi(a^2+c^2)/4+a c)b==k]//Resolve[#,Reals]&

【不等式の証明】

f[x_]=x^4+x^3+1/2x^2+1/6x+1/24;  g[x_]=x^5+x^4+1/2 x^3+1/6x^2+1/24x+1/120;
(*1*) ForAll[x,f[x]>0]//Resolve[#,Reals]&

(*2*)Exists[α,g[α]==0&&-1<α<0&&ForAll[x,g[x]==0\[Implies]x==α]]//Resolve[#,Reals]&