\( \DeclareMathOperator{\abs}{abs} \newcommand{\ensuremath}[1]{\mbox{$#1$}} \)

式と証明(Expressions and Certification)

1 式と計算(Expressions and calculations)

 1.1 3次式の展開と因数分解(expression of the third order)

 1.2 二項定理(binomial theorem)

\[(1) \sum_{k=0}^{n}\,_nC_k,\sum_{k=0}^{n}(-1)^k\,_nC_k,\sum_{k=0}^{n}(-2)^k\,_nC_k \]

$$(2) (a+b+c)^7の展開式におけるa^3b^2c^2の項の係数を求めよ。$$
例によってGeogebraの計算から。Sumも結構な計算をこなす。

図 1:
Diagram

和を計算する命令としては sum,simpsum,nusum,simplify_sum の順で強力になるらしい。

(%i1) sum(binomial(n,k),k,0,n);
\[(\%o1)\sum_{k=0}^{n}{\left. \left( \begin{pmatrix}n\\ k\end{pmatrix}\right) \right.}\]
(%i2) sum(binomial(n,k),k,0,n),simpsum;
\[(\%o2){{2}^{n}}\]
(%i3) sum((-1)^k*binomial(n,k),k,0,k),simpsum;
\[(\%o3)\sum_{k=0}^{k}{\left. {{\left( -1\right) }^{k}}\,\left( \begin{pmatrix}n\\ k\end{pmatrix}\right) \right.}\]
(%i4) nusum((-1)^k*binomial(n,k),k,0,n);
\[(\%o4)0\]
(%i5) nusum((-2)^k*binomial(n,k),k,0,n);
\[(\%o5)\sum_{k=0}^{n}{\left. {{\left( -2\right) }^{k}}\,\left( \begin{pmatrix}n\\ k\end{pmatrix}\right) \right.}\]
(%i6) load(simplify_sum)$
(%i7) simplify_sum(sum((-2)^k*binomial(n,k),k,0,n));
\[(\%o7){{\left( -1\right) }^{n}}\]
(%i8) coeff(coeff(coeff(expand((a+b+c)^7),a^3),b^2),c^2);
\[(\%o8)210\]

 1.3 整式の割り算

除法:division 商:quotient 余り:remainder 組立除法:Synthetic Division
割り切れる:divisible(without a remainder) 因数:factor

整式の割り算は数と同じで,商と余りが両方出るのはdivide,商だけならquotient,
数だと余りだけ出すmodというのがあったが,整式ではないようだ。

(%i9) divide(2*x^3+4*x^2+7,2*x^2-3);
\[(\%o9)[x+2,3x+13]\]
(%i10) quotient(2*x^3+4*x^2+7,2*x^2-3);
\[(\%o10)x+2\]
(%i11) divide(2*x^3-5*x^2*y+6*x*y^2-8*y^3,x-2*y);
\[(\%o11)[4{{y}^{2}}-xy+2{{x}^{2}},0]\]

 1.4 分数式とその計算

分数式:fraction 有理式:rational
約分:reduce 既約:irreducible 通分:reduce(to a common denominator)
昔,レデュースという数式ソフトがあったっけ。

通分にも combine とか xthru とか色々有ります。
分子は num(numerator),分母は denom(denominator)
ratsimp(rational simplyfy)で殆どの計算をしてくれる。

(%i12) combine(a/3+b/4);
\[(\%o12)\frac{3b+4a}{12}\]
(%i13) f:(2*x-3)/(x^2-4*x+3)-(2*x+3)/(x^2-9);
\[\tag{f}\label{f}\frac{2x-3}{{{x}^{2}}-4x+3}-\frac{2x+3}{{{x}^{2}}-9}\]
(%i14) g:xthru(f);
\[\tag{g}\label{g}\frac{\left( -2x-3\right) \,\left( {{x}^{2}}-4x+3\right) +\left( 2x-3\right) \,\left( {{x}^{2}}-9\right) }{\left( {{x}^{2}}-9\right) \,\left( {{x}^{2}}-4x+3\right) }\]
(%i16) factor(num(g));factor(denom(g));
\[(\%o15)2{{\left( x-3\right) }^{2}}\] \[(\%o16){{\left( x-3\right) }^{2}}\,\left( x-1\right) \,\left( x+3\right) \]
(%i17) ratsimp(f);
\[(\%o17)\frac{2}{{{x}^{2}}+2x-3}\]
(%i18) factor(%);
\[(\%o18)\frac{2}{\left( x-1\right) \,\left( x+3\right) }\]

 1.5 恒等式

恒等式:identity

\[ 次の等式が恒等式になるように,定数a,b,c,dの値を定めよ。\]
\[(1)a(x+1)^2+b(x+1)+c=x^2+x+1\]
\[(2)a(x+1)(x-1)+bx(x+1)+cx(x-1)=3x-1\]

恒等式は MATHEMATICA という高いソフトには,命令があってすぐ未定係数を求めてくれるんですが,
Maxima には同じものはなさそうなので,作ってみました。
話題をずらして,大体どこからこんな問題が出てくるのかを考えようか。
(1)はx+1をyつまり右辺をxをx-1に変えたときの係数とも思えるし,
x=-1のときのテイラー展開(taylor)すれば得られる。
(2)は両辺をx(x+1)(x-1)で割れば部分分数変換(partfrac)です。

(%i19) iden(f,x):=block(
g:expand(f),
h:g,[x=0],    
l:[],m:[a,b,c,d,e,f],n:[],
for i:1 thru hipow(g,x) do push(coeff(g,x^i),l),
push(h,l),
for j:1 thru length(l) do push(m[length(l)+1-j],n),
solve(l,n)
)$
(%i20) iden(a*(x+1)^2+b*(x+1)+c=x^2+x+1,x);
\[(\%o20)[[a=1,b=-1,c=1]]\]
(%i21) expand((x-1)^2+(x-1)+1);
\[(\%o21){{x}^{2}}-x+1\]
(%i22) taylor(x^2+x+1,x,-1,2);
\[(\%o22)/T, 1-\left( x+1\right) +{{\left( x+1\right) }^{2}}+\mbox{...}\]
(%i23) iden(a*(x+1)*(x-1)+b*x*(x+1)+c*x*(x-1)=3*x-1,x);
\[(\%o23)[[a=1,b=1,c=-2]]\]
(%i24) partfrac((3*x-1)/(x*(x-1)*(x+1)),x);
\[(\%o24)-\frac{2}{x+1}+\frac{1}{x}+\frac{1}{x-1}\]

2 等式と不等式の証明

比例式:proportional expression MS P明朝のP、勝手に文字幅が動くやつね
連比:continued ratio
相加平均と相乗平均:arithmetic,geometric mean 等差と等比の違いですね

 2.1 等式の証明

証明の部分はこんなことができるのか,という例として。
is()は括弧の中身の真偽を答える。assume()は括弧の中身を仮定する。

\[ 例題 a+b+c=0 のとき a^3+b^3+c^3=3abc \]

(%i25) c:-a-b$
(%i26) is(expand(a^3+b^3+c^3)=expand(3*a*b*c));
\[(\%o26)\mbox{true}\]

 2.2 不等式の証明

すべてがうまくいくとは限らないが,平方の形が負にはならないのは判断し,
それ以外は unknown(知ーラナイ)と返ってきます。

もっと驚いたのは,相加相乗平均も知っているようです。しかも,正という条件がつけば返事をしてくれます。
以下実験です。

例題 以下の不等式を証明せよ。
\[(1) a>c,b>d のとき ab+cd>ad+bc\]
\[(2) 2(x^2+y^2)\ge (x+y)^2  \hspace{3cm} (3) x^2+1>x \]
\[(4) a^2+b^2\ge ab  \hspace{3cm}(5) \frac{a}{b}+\frac{b}{a}-2\ge 0\]
\[(6) \sqrt{a}+\sqrt{b}>\sqrt{a+b} \hspace{3cm} (7) |a|+|b|>|a+b| \]

(%i27) kill(all)$
(%i1) assume(a>c and b>d);
\[(\%o1)[a>c,b>d]\]
(%i2) is(a*b+c*d>a*d+b*c);
\[(\%o2)\mbox{true}\]
(%i3) is(2*(x^2+y^2)>=(x+y)^2);
\[(\%o3)\mbox{true}\]
(%i4) solve(2*(x^2+y^2)=(x+y)^2,y);
\[(\%o4)[y=x]\]
(%i5) is(x^2+1>x);
\[(\%o5)\mathit{unknown}\]
(%i6) is(a^2+b^2>=a*b);
\[(\%o6)\mathit{unknown}\]
(%i7) assume(a>0 and b>0);
\[(\%o7)[a>0,b>0]\]
(%i8) is(a/b+b/a-2>=0);
\[(\%o8)\mbox{true}\]
(%i9) solve(a/b+b/a-2=0,b);
\[(\%o9)[b=a]\]
(%i10) is(c/d+d/c-2>=0);
\[(\%o10)\mathit{unknown}\]
(%i11) is(sqrt(a)+sqrt(b)>=sqrt(a+b));
\[(\%o11)\mathit{unknown}\]
(%i12) is(abs(a)+abs(b)>=abs(a+b));
\[(\%o12)\mbox{true}\]
(%i13) solve(abs(a)+abs(b)=abs(a+b),b);
\[(\%o13)\mathit{all}\]
(%i14) is(a^2+b^2+c^2>=a*b+b*c+c*a);
\[(\%o14)\mathit{unknown}\]
(%i15) is((a^2+b^2+c^2)*(x^2+y^2+z^2)>=(a*x+b*y+c*z)^2);
\[(\%o15)\mathit{unknown}\]
Created with wxMaxima. inserted by FC2 system