2012-02-06から1日間の記事一覧
以上をまとめると次のようになります. g `!f (z:num->num->real). (!x. &0 <= x /\ x <= &1 ==> f contl x) ==> (?z. !N. 1 <= N ==> (!n. if n < N then &n / &N <= z N n /\ z N n <= &(n + 1) / &N else z N n = &1) /\ integral (&0,&1) (\x. f x * abs…
以上をまとめると次のようになります. g `!f (z:num->num->real). (!x. &0 <= x /\ x <= &1 ==> f contl x) ==> (?z. !N. 1 <= N ==> (!n. if n < N then &n / &N <= z N n /\ z N n <= &(n + 1) / &N else z N n = &1) /\ integral (&0,&1) (\x. f x * abs…