2012-02-20から1日間の記事一覧
先のJENSEN_LT_INFを用いて,変数の相加平均と相乗平均の不等式を証明します. let lemma0 = prove (`!n s x. (!i. i <= n ==> &0 <= s i) /\ sum (0..n) s = &1 /\ (!i. i <= n ==> &0 < x i) ==> sum (0..n) (\i. s i * ln (x i)) <= ln (sum (0..n) (\i. …
先のJENSEN_LT_INFを用いて,変数の相加平均と相乗平均の不等式を証明します. let lemma0 = prove (`!n s x. (!i. i <= n ==> &0 <= s i) /\ sum (0..n) s = &1 /\ (!i. i <= n ==> &0 < x i) ==> sum (0..n) (\i. s i * ln (x i)) <= ln (sum (0..n) (\i. …