東ロボくんのこと（13）一変数化，下限上限の一致 by BOTTEMA

　http://d.hatena.ne.jp/ehito/20131208/1386496330 で述べた（４）は

　∃k( ∃x(x∈D∧k=f(x)) ∧ ∀x(x∈D→k≦f(x)) ∧ ∀x(x∈D→k≧f(x)) )

であり，これはDが空集合でないなら（５），つまり

　∃k( ∀x(x∈D→k≦f(x)) ∧ ∀x(x∈D→k≧f(x)) )

と等価です．

　しかも，∀x(x∈D→0≦p(x)) の形はQE向きであり，∀x(x∈D→k≦f(x))，∀x(x∈D→k≧f(x)) を個別に処理すれば良い点も好印象です．そこで，RedLog の後塵を拝した Mathematica に

Reduce[ForAll[{sq2, a, b, x, y, s, L1, L2, L3}, asm, k <= L1 + L2 + L3], Reals]

と問う訳ですが，やはり帰って来ません．

　．．．という訳で，BOTTEMA2009 on Maple (http://d.hatena.ne.jp/ehito/20111010/1318225575) の登壇となります．ただし，制約（定義域の条件）に等式は使えない（ことになっている）ので，A≧B∧A≦B といったコストの高い話になってしまいます．そこで今回は，線分の長さの和を a のみを用いて表し，0 <= a <= 1 のもとでその値域の下限，上限を求めてみます．

P = {0, -Sqrt[2]}; Q = {0, Sqrt[2]}; A = {a, Sqrt[a^2 + 1]};
{B, C2} = {{x, y}, {x, 2}} /. Solve[{{x, y} == (1 - s)*Q + s*A, y == Sqrt[2]/8*x^2}, {x, y, s}][[2]];
ca = Sqrt[(A - P).(A - P)] + Sqrt[(B - A).(B - A)] + Sqrt[(C2 - B).(C2 - B)];

この ca を Maple の書式にコンバートして

xmax(k<=ca,[0<=a,a<=1],k);

xmin(k>=ca,[0<=a,a<=1],k);

とすれば，見る間に処理が進み

`OUTPUT RESULT:`
`The best possible maximal const ` . k . ` is a root of the following polynomial :`
k^2-8*k+14
`which is between（`, 5, `，`, 17/3, `）`

`OUTPUT RESULT:`
`The best possible minimal const ` . k . ` is a root of the following polynomial :`
k^2-8*k+14
`which is between（`, 5, `，`, 17/3, `）`

に至ります．