QE で最大

　前回は最大値を求めるところを，値域まで求めてしまいましたので，今回は関数の最大値のみを求めます．と言っても方法はいつもと同じで，定義を論理式で表し，QE するだけです．
　まず最大値の定義ですが，集合 A を定義域とする実数値関数 f の最大値が M であるとは

∃x [ x ∈ A ∧ f(x) = M ] ∧ ∀x [ x ∈ A → f(x) ≦ M ]

ということでした．そこで

Reduce[
　Exists[ k, -4 < k < 4, Sqrt[(-(k - 4)^3)*(k + 4)]/(4*Sqrt[3]) == M ] &&
　ForAll[ k, -4 < k < 4, Sqrt[(-(k - 4)^3)*(k + 4)]/(4*Sqrt[3]) <= M ],
　Reals
]

のように QE すれば

M == 3

と出力されます．ここで Mathematica の特称，全称関数では
Exists[ V, P && Q ] を Exists[ V, P, Q ]
ForAll[ V, P ⇒ Q ] を ForAll[ V, P, Q ]
と略記できることに注意します．
　そして集合 A を定義域とする実数値関数 f の最大値を与える点が a であるとは

a ∈ A ∧ ∀x [ x ∈ A → f(x) ≦ f(a) ]

ということですから

Reduce[
　-4 < a < 4 &&
　ForAll[ k, -4 < k < 4, Sqrt[(-(k - 4)^3)*(k + 4)]/(4*Sqrt[3]) <= Sqrt[(-(a - 4)^3)*(a + 4)]/(4*Sqrt[3]) ],
　Reals
]

のように QE すれば

a == -2

と出力されます．