GMge0

　ということでamgm2は準備出来たのですが，今度はGMがその仮定を満たすこと，つまり

lemma GMge0:
"ALL k. 0 <= a k ==> 0 < n ==> 0 <= GM a m n"

が入用になります．例によって

proof simp

と試すと

goal (1 subgoal):
1. ∀k. 0 ≤ a k ⟹ 0 < n ⟹ 0 ≤ setprod a {Suc m..m + n}

までは出来ているので

find_theorems "0 <= setprod _ _ "

と探せば

searched for:
"0 ≤ setprod _ _"

found 2 theorem(s):

Big_Operators.setprod_nonneg:
(⋀x. x ∈ ?A ⟹ 0 ≤ ?f x) ⟹ 0 ≤ setprod ?f ?A
Nat_Transfer.transfer_nat_int_sum_prod_closure(2):
nat_set ?A ⟹ (⋀x. 0 ≤ x ⟹ 0 ≤ ?f x) ⟹ 0 ≤ setprod ?f ?A

なので，改めて

  by (simp add: setprod_nonneg)

と片付けます．

　なお，仮定に0 < nを付けているのは，rootに関わる定理の多くがこれを仮定していることに加え，root 0 x自体がIsabelle2013では未定義であることによります（実は最新版 http://isabelle.in.tum.de/repos/isabelle/rev/dc39d69774bb9524dbd732a871c6ab320101af07 では定義が改まり，結果 lemma root_0 [simp]: "root 0 x = 0" も実装されています）．

　以上，２つの補題と仮定により

using amgm2 GMge0 Suc.prems

proof (prove): step 20

using this:
0 ≤ ?x ⟹ 0 ≤ ?y ⟹ root 2 (?x * ?y) ≤ (?x + ?y) / 2
∀k. 0 ≤ ?a k ⟹ 0 < ?n ⟹ 0 ≤ GM ?a ?m ?n
∀k. 0 ≤ a k

goal (1 subgoal):
1. root 2 (GM a m (2 ^ N) * GM a (m + 2 ^ N) (2 ^ N))
≤ (GM a m (2 ^ N) + GM a (m + 2 ^ N) (2 ^ N)) / 2

となるので

by simp

で証明完了

also

で

calculation:
GM a m (2 ^ Suc N) ≤ (GM a m (2 ^ N) + GM a (m + 2 ^ N) (2 ^ N)) / 2

が得られます．