先の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. …

HOL LightはOcamlのToplevel Loop上のプログラムですから，Ocamlが動くならOSは問いませんが，周辺プログラムとの連携という観点に立つなら何といってもUnixです． それはMaximaやPARI/GPを呼ぶmlファイル内のシステムコマンドによるものだけではなく，一般…

普通の数学ならTaylorの定理が簡単ですが，HOL Lightで書いてみると予想外に長くなりましたので，MVTを二重に使う方針にしました． (* f(x)<=f(p)+(x-p)*f'(p) *) let ass = ASM_SIMP_TAC[] THEN STRIP_TAC;; g`!a b:real f f' f'':real->real. a<b /\ (!x. a<=x /\ x<=b ==> (f diffl f</b>…

今回は私がHOL Lightで証明を書く際の環境？をご紹介します． OSはWindows，エディターは秀丸，OcamlはDOS窓内です． 秀丸はシェアウエアですが，軽快な作動と柔軟なカスタマイズ性，Cライクなマクロが特徴で，私は例えば，カーソルのある論理行をクリップボ…

かなり刹那的ですが，とりあえず２変数の場合です．MVT_ALTではなくMVTを参照すれば端点での可微分性は不要なのですが，その分contlを付さねばならず煩雑？なので，この形にしました（transc.mlのMCLAURINの証明にもWe could weaken the hypotheses slightly…

次回からは，一変数級関数上の数列についてのJensenの不等式を証明します．

ある論文で紹介されていた排中律によるトリック？です． # g `!p:A->bool. ?x:A. (p x ==> !y. p y)`;; val it : goalstack = 1 subgoal (1 total) `!p. ?x. p x ==> (!y. p y)` # e(GEN_TAC);; val it : goalstack = 1 subgoal (1 total) `?x. p x ==> (!y.…

これで積分の第一平均値定理が通常の形で証明できます． let CONT_ATTAINS3 = prove (`!f:real->real a b. a <= b /\ (!x. a <= x /\ x <= b ==> f contl x) ==> (?L. (!x. a <= x /\ x <= b ==> L <= f x) /\ (?x1. a <= x1 /\ x1 <= b /\ f x1 = L)) /\ (?…

落穂ひろい気味ですが，先のthm15から&0 積分の第一平均値定理を得るための補題の証明です． let INTEGRAL_CONST_LE = prove (`!c g a b. a <= b /\ integrable (a,b) g /\ (!x. a <= x /\ x <= b ==> c <= g x) ==> c * (b - a) <= integral (a,b) g`, GEN_…

以上をまとめると次のようになります． 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…

tagged division用のlemmaを幾つか用意すれば，区分求積の公式が証明できます． g`(!n. n < N ==> (if n < N then &n / &N else &1) < (if n + 1 < N then &(n + 1) / &N else &1)) /\ (!n. n >= N ==> (if n < N then &n / &N else &1) = &1)`;; e(REPEAT S…

そして，Kurzweil-Henstock積分ですので，区分求積の為に通常のRiemann積分の理論を自作します． let rdefint = new_definition `(!a b f k. rdefint (a,b) f k <=> (!e. &0 < e ==> (?g. &0 < g /\ (!D p. ((D 0 = a /\ (?N. (!n. n < N ==> D n < D (SUC n…

得られた結果をもとの式に適用します． g `!f n k. 1 <= n /\ 1 <= k /\ k <= n /\ (!x. &(k - 1) / &n <= x /\ x <= &k / &n ==> f contl x) ==> ?z. &(k - 1) / &n <= z /\ z <= &k / &n /\ integral (&(k - 1) / &n,&k / &n) (\x. f x * abs (sin (&n * p…

前回の結果とDIFF_CONV，更に微積分の基本定理（その１）FTC1を用いて，定積分の値を具体化します． let lemma01 = MESON[REAL_LE; REAL_ARITH `&1 <= &n ==> &0 < &n`; REAL_LE_LDIV_EQ; REAL_LE_RDIV_EQ; PI_POS; REAL_LE_LMUL_EQ; REAL_MUL_AC] `1 <= n =…