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 =…