前回の和と積，更に割り算と累乗根を用いると fun AM :: "(nat => real) => nat => nat => real" where "AM a m n = setsum a {Suc m..m + n} / n" fun GM :: "(nat => real) => nat => nat => real" where "GM a m n = root n (setprod a {Suc m..m + n})" …

Isarにおいて，数列の有限項の和，積を得るには，setsum，setprod を用います．引数として，数列と定義域を与えると，その値域の要素の和，積になります．例えば lemma "setsum (a::nat=>real) {0,2,3,100} = a 0 + a 2 + a 3 + a 100" by simp lemma "setpr…