amgm_2 qed

　ということで，次は

have "... <= (AM a m (2 ^ N) + AM a (m + 2 ^ N) (2 ^ N)) / 2"

ですが，今回はsimpを試すまでももなく

Suc.hyps: ∀k. 0 ≤ a k ⟹ GM a ?m (2 ^ N) ≤ AM a ?m (2 ^ N)
Suc.prems: ∀k. 0 ≤ a k

を用いる訳で，そのためにthoremレベルのinst属性であるOF，および，termレベルのinst属性であるofにより

  using Suc.hyps[OF Suc.prems, of "m"]
        Suc.hyps[OF Suc.prems, of "m + 2 ^ N"]

とすれば

using this:
GM a m (2 ^ N) ≤ AM a m (2 ^ N)
GM a (m + 2 ^ N) (2 ^ N) ≤ AM a (m + 2 ^ N) (2 ^ N)

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

なので，あとは簡単な？有理計算なので

    by (simp add: field_simps)

で証明完了

  finally

でcalculationの先頭と末尾を繋ぐと

calculation:
GM a m (2 ^ Suc N) ≤ (AM a m (2 ^ N) + AM a (m + 2 ^ N) (2 ^ N)) / 2
proof (chain): step 26

picking this:
GM a m (2 ^ Suc N) ≤ (AM a m (2 ^ N) + AM a (m + 2 ^ N) (2 ^ N)) / 2

となるので

 show ?case
proof simp

とすると

goal (1 subgoal):
1. root (2 * 2 ^ N) (setprod a ({Suc m..m + 2 ^ N} ∪ {Suc (m + 2 ^ N)..m + 2 ^ N + 2 ^ N})) * 2
≤ setsum a {Suc m..m + 2 ^ N} / 2 ^ N + setsum a {Suc (m + 2 ^ N)..m + 2 ^ N + 2 ^ N} / 2 ^ N ⟹
root (2 * 2 ^ N) (setprod a ({Suc m..m + 2 ^ N} ∪ {Suc (m + 2 ^ N)..m + 2 ^ N + 2 ^ N}))
≤ setsum a ({Suc m..m + 2 ^ N} ∪ {Suc (m + 2 ^ N)..m + 2 ^ N + 2 ^ N}) / (2 * 2 ^ N)

なので

setsum a {Suc m..m + 2 ^ N} / 2 ^ N + setsum a {Suc (m + 2 ^ N)..m + 2 ^ N + 2 ^ N}
=setsum a ({Suc m..m + 2 ^ N} ∪ {Suc (m + 2 ^ N)..m + 2 ^ N + 2 ^ N})

が言えれば良さそうですが，これは積の場合と同様なので

apply (simp add: setsum_Un_disjoint)

とすると

goal (1 subgoal):
1. root (2 * 2 ^ N) (setprod a ({Suc m..m + 2 ^ N} ∪ {Suc (m + 2 ^ N)..m + 2 ^ N + 2 ^ N})) * 2
≤ setsum a {Suc m..m + 2 ^ N} / 2 ^ N + setsum a {Suc (m + 2 ^ N)..m + 2 ^ N + 2 ^ N} / 2 ^ N ⟹
root (2 * 2 ^ N) (setprod a ({Suc m..m + 2 ^ N} ∪ {Suc (m + 2 ^ N)..m + 2 ^ N + 2 ^ N}))
≤ (setsum a {Suc m..m + 2 ^ N} + setsum a {Suc (m + 2 ^ N)..m + 2 ^ N + 2 ^ N}) / (2 * 2 ^ N)

まで進むので，あとの計算に任せて，改めて

  by (simp add: setsum_Un_disjoint field_simps)

とすれば

show GM a m (2 ^ Suc N) ≤ AM a m (2 ^ Suc N)
Successful attempt to solve goal by exported rule:
(⋀m. ∀k. 0 ≤ a k ⟹ GM a m (2 ^ ?N2) ≤ AM a m (2 ^ ?N2)) ⟹
(∀k. 0 ≤ a k) ⟹ GM a ?ma2 (2 ^ Suc ?N2) ≤ AM a ?ma2 (2 ^ Suc ?N2)
proof (state): step 28

this:
GM a m (2 ^ Suc N) ≤ AM a m (2 ^ Suc N)

goal:
No subgoals!

となるので

qed

で amgm_2 の完成です．

　ここまでをまとめると

theory amgm imports Complex_Main begin

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})"

lemma GMge0:
  "ALL k. 0 <= a k ==> 0 < n ==> 0 <= GM a m n"
  by (simp add: setprod_nonneg)

lemma amgm2:
  "0 <= x ==> 0 <= y ==> root 2 (x * y) <= (x + y) / 2"
  using zero_le_power2 [of"root 2 x - root 2 y"]
  by (simp add: power2_diff real_root_mult)

lemma amgm_2:
  fixes a m n
  shows "ALL k. 0 <= a k ==> GM a m (2 ^ n) <= AM a m (2 ^ n)"
proof (induct n arbitrary: m)
  case 0 then show ?case by simp
next
  case (Suc N)
  have natseg [simp]:
  "{Suc m..m + 2 * 2 ^ N} = union {Suc m..m + 2 ^ N} {Suc (m + 2 ^ N)..m + 2 ^ N + 2 ^ N}"
    by auto
  have "GM a m (2 ^ Suc N) = root 2 (GM a m (2 ^ N) * GM a (m + 2 ^ N) (2 ^ N))"
    by (simp add: real_root_mult_exp real_root_mult setprod_Un_disjoint)
  also have "... <= (GM a m (2 ^ N) + GM a (m + 2 ^ N) (2 ^ N)) / 2"
    using amgm2 GMge0 Suc.prems by simp
  also have "... <= (AM a m (2 ^ N) + AM a (m + 2 ^ N) (2 ^ N)) / 2"
    using Suc.hyps[OF Suc.prems, of "m"] Suc.hyps[OF Suc.prems, of "m + 2 ^ N"]
    by (simp add: field_simps)
  finally show ?case
    by (simp add: setsum_Un_disjoint field_simps)
qed

print_statement GMge0 amgm2 amgm_2

theorem GMge0:
fixes a :: "nat ⇒ real"
and n :: "nat"
and m :: "nat"
assumes "∀k. 0 ≤ a k"
and "0 < n"
shows "0 ≤ GM a m n"

theorem amgm2:
fixes x :: "real"
and y :: "real"
assumes "0 ≤ x"
and "0 ≤ y"
shows "root 2 (x * y) ≤ (x + y) / 2"

theorem amgm_2:
fixes a :: "nat ⇒ real"
and m :: "nat"
and n :: "nat"
assumes "∀k. 0 ≤ a k"
shows "GM a m (2 ^ n) ≤ AM a m (2 ^ n)"

といった具合です．