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

2018 年9月16日  Cabri研究会　生越　茂樹

QEのコマンド

§1．通過領域

[立体射影]

Qは直線AP上より,　(OverVector[AP])= t (OverVector[AQ])⇔(({{x}, {   y
z-1}})) = t (({{u}, {   v
-1}}))

ClearAll["Global`*"]; 
Exists[{x,y,z,t},x^2+y^2+z^2==1&&x≥1/3&&y≥1/3&&z≥1/3&&{x,y,z-1}==t{u,v,-1}];
pred=Reduce[%,{u,v},Reals]//FullSimplify(* v を u の式で表す*)

reg=ImplicitRegion[pred,{u,v}];
RegionPlot[reg]

[点射影]

a,b,cのままでは図示できないので，a = 2, b = 1, c = 3 として解答する. 
P(X,Y,c+1), R上の点をR’(x,y,c), 直線PR’とxy平面の交点をQ(u,v,0)とおくと,　(OverVector[QR'])= t (OverVector[QP])⇔(({{x-u}, {y-v
c}})) = t (({{X-u}, {Y-v
c+1}}))

ClearAll["Global`*"]; 
a=2;b=1;c=3;
Exists[{x,y,X,Y,t},Abs[x]≤a&&Abs[y]≤b&&{x-u,y-v,c}==t{X-u,Y-v,c+1}&&X^2/a^2+Y^2/b^2==1];
pred=Reduce[%,Reals](*Resolve では汚い結果になる*)

RegionPlot[pred,{u,-15,15},{v,-8,8},Axes->True,AspectRatio->Automatic]

面積は，文字のままで求まる. (14秒ほど掛かる)

ClearAll["Global`*"]; 
Exists[{x,y,X,Y,t},a>0&&b>0&&c>0&&Abs[x]≤a&&Abs[y]≤b&&{x-u,y-v,c}==t{X-u,Y-v,c+1}&&X^2/a^2+Y^2/b^2==1];
pred=Resolve[%,Reals];(*a,b,c のとき Reduce では非常に時間が掛かる*)
{time,area}=RegionMeasure[ImplicitRegion[pred,{u,v}]]//Timing//FullSimplify

§2．方程式

ForAll, Exists は入れ子にできる．

ClearAll["Global`*"]; 

g[x_]=x^2-(a+d)x+(a d-b c);
ForAll[{a,b,c,d,s,t},a>0&&b>0&&c>0&&d>0&&s>0&&t>0&&s (1-a)-t b>0&&-s c+t(1-d)>0\[Implies]
Exists[{x1,x2},g[x1]==g[x2]==0&&-1<x1<x2<1]]; 
Resolve[%,Reals]

虚数解を扱う時は Resolve[ 論理式 , Complexes] と  p ∈ Reals , (p|q) ∈ Reals などを組み合わせる．

ForAll[x,(p|q)∈Reals &&p x^2+(p^2-q)x-(2p-q-1)==0, Re[x]<0];
Reduce[%,Complexes]//FullSimplify
RegionPlot[%,{p,-2,2},{q,-2,4},PlotPoints->50,Axes->True]

(非常に不可解なことに ForAll[x,(p|q)∈Reals&&p x^2+(p^2-q)x-(2p-q-1)==0 => Re[x]<0] では駄目!)

ClearAll[a,b];
(*α が実数の場合と β が実数の場合に分けないと, 時間が非常に掛かる-少なくとも1日以上-*)
Exists[{α, β, γ},α^2+α β +β ^2==α-3β -6&&α ++β+γ==-a&&α β+β γ+γ α==b&&α β γ==-8&&(α|β|a|b)∈Reals];
Resolve[%,Complexes]
Exists[{α, β, γ},α^2+α β +β ^2==α-3β -6&&α ++β+γ==-a&&α β+β γ+γ α==b&&α β γ==-8&&(α|a|b)∈Reals];
Resolve[%,Complexes]
Exists[{α, β, γ},α^2+α β +β ^2==α-3β -6&&α ++β+γ==-a&&α β+β γ+γ α==b&&α β γ==-8&&(β|a|b)∈Reals];
Resolve[%,Complexes]

[注]α, βがともに虚数の場合は false は明らかだが，QEではうまく示せない.

(*(1)はExists{p,x1,x2}とする．x1 は最小の実数解, x2 は最大の実数解で x1=x2となる事もあり得る*)
ClearAll["Global`*"];  f[x_]=x^3-3x-p;
Exists[{x1,x2,p},f[x1]==f[x2]==0∧ForAll[y,y<x1||y>x2\[Implies]f[y]≠0]∧x1*x2==m];
Resolve[%,Reals]

(*(2)はExists{p,x1,x2}とする．*)
Exists[{x1,x2},f[x1]==f[x2]==0∧ForAll[y,y<x1||y>x2\[Implies]f[y]≠0]∧x1*x2==m];
Resolve[%,Reals]//FullSimplify;
RegionPlot[ImplicitRegion[%,{{p,-6,6},{m,-3,7}}],Axes->True]

【別解】 解と係数の関係の利用 (faster)

(*(1)はExists{x1,x2,x3,p}とする．前半は 実数解を3つ持つ時，後半は実数解を1つだけ持つ時*)
Exists[{x1,x2,x3,p},x1+x2+x3==0&&x1 x2+x2 x3+x3 x1==-3&&x1 x2 x3==p&&(x1|x2|p|m)∈Reals&&x1≤x2≤x3&&x1*x3==m]∨
Exists[{x1,x2,x3,p},x1+x2+x3==0&&x1 x2+x2 x3+x3 x1==-3&&x1 x2 x3==p&&(x1|p|m)∈Reals&&!x2∈Reals&&x1*x1==m];Resolve[%,Complexes]

(*(2)はExists{x1,x2,x3}とする*)
Exists[{x1,x2,x3},(x1|p|m)∈Reals,x1+x2+x3==0&&x1 x2+x2 x3+x3 x1==-3&&x1 x2 x3==p&&x1≤x2≤x3&&x1*x3==m]∨
Exists[{x1,x2,x3},(x1|p|m)∈Reals&&!x2∈Reals&&x1+x2+x3==0&&x1 x2+x2 x3+x3 x1==-3&&x1 x2 x3==p&&x1*x1==m];
Resolve[%,Complexes]//FullSimplify;
RegionPlot[ImplicitRegion[%,{{p,-6,6},{m,-3,7}}],Axes->True]

【付録】Mathematica は 東京医大に入学できるか？

ClearAll["Global`*"]
A1={a,0};A2={a3,a4};B1={b1,b2};B2={b3,b4};p={x,y};
cons=A1.B1==3&&A1.B2==4&&A2.B1==5&&A2.B2==7&&A1.p==14&&A2.p==23&&B1.p==22&&B2.p==35;

Exists[{a,a3,a4,b1,b2,b3,b4,x,y},cons&&(A2-A1).(B1-p)==k1];
Resolve[%,Reals]
Exists[{a,a3,a4,b1,b2,b3,b4,x,y},cons&&x^2+y^2==k2];
Resolve[%,Reals]

(*1*)
f[x_]:=x^5+ a x^4+b x^3+c x^2;
cons=f'[0]==0∧f[0]==0∧f''[0]<0∧f'[5]==0∧f[5]==0∧f''[5]>0;
Exists[{a,c},cons];
Resolve[%,Reals]//Simplify
Exists[{a,b,c,p},cons&&f'[p]==0&&f[p]==M&&f''[p]<0&&p≠0];
Resolve[%,Reals]//Simplify

(*2*) ClearAll["Global`*"]
f[x_]=((a x)^(-(b x)^(c x)/3))/.{a->8,b->1/E,c->-Log[2]};
f'[1]

ClearAll[a]

sol=RSolve[{a[n+1]==a[n]Cos[n^2 Pi/3],a[1]==1},a[n],n];
a[n_]=(a[n]/.sol)[[1]]//FullSimplify

(*1*)
a[6]
Sum[a[k],{k,1,6}]

(*2*)
Log[2,Abs[a[70]]]
Sum[a[6k+1],{k,1,Infinity}]

(*3*)
Sum[Sum[a[6k+r],{k,0,Infinity}],{r,1,6}]

ClearAll[f,x]
f[x_]=1/2x+1/8x^3;
F=ImplicitRegion[f[x]<y<2&&x>0,{x,y}];
Show[Plot[{f[x],2},{x,-1,3}],RegionPlot[F]]

(*1*)
RegionMeasure[F]

(*2*) ( InverseFunction は逆関数の枝のうち適当にひとつを選ぶので,出題者の意図した解答と符号が異なる)

f[x_]=1/2x+1/8x^3;
h[x_]=x^2;
g=Composition[h,InverseFunction[f]];(*g=((((f^(-1))))^2)*)
InverseFunction[g][2]

上では (h^(-1))[x]=-(Sqrt[x]) の枝を取っているので符合が異なる! そこで手動で解答する

Composition[f,Sqrt[#]&][2]

(*3*)
(*バウムクーヘン分割の利用*)
Integrate[2Pi x (2-f[x]),{x,0,2}]

(*RegionMeasure の利用. 答えは一致するが, ちょっと時間が掛かる*)

ImplicitRegion[2>z>f[Sqrt[x^2+y^2]],{x,y,z}];
RegionMeasure[%]

ContourPlot[(x^2+y^2)^2==x^3-3x y^2, {x,-0.7,1.1},{y,-1,1},PlotPoints->50,Axes->True]

(*[注意]次のようにすると a,b,c が f[x]=0 の3解となるとは限らない*)
f[x_]:=x^3-3x-p
Exists[{a,b,c,p},f[a]==f[b]==f[c]==0&&a<=b<=c&&a c==M];
Resolve[%,Reals]//FullSimplify

Exists[p,p∈Reals&&Max[Select[x/.Solve[x^3-3x-p==0,x],Im[#]==0&]]*Min[Select[x/.Solve[x^3-3x-p==0,x],Im[#]==0&]]==M]
Resolve[%,Reals]