2012-01-17から1日間の記事一覧
今回は,2重根号をexpを用いずに,4変数の相加相乗平均の大小関係を証明してみます. (* amgm4 *) (* まず,2変数の場合を証明します.*) g`!a b. &0 <= a /\ &0 <= b ==> (a + b) / &2 >= sqrt(a * b)`;; e(REPEAT GEN_TAC);; e(DISCH_THEN(fun t -> MP_…
今回は,2重根号をexpを用いずに,4変数の相加相乗平均の大小関係を証明してみます. (* amgm4 *) (* まず,2変数の場合を証明します.*) g`!a b. &0 <= a /\ &0 <= b ==> (a + b) / &2 >= sqrt(a * b)`;; e(REPEAT GEN_TAC);; e(DISCH_THEN(fun t -> MP_…