amgm_0 qed

　以下は正数である分母 Suc i を払う，両辺から同じものを減ずる，そして，両辺を正数 i で割るといった代数計算です．この種の処理で参照すべき定理は，多くの場合，nat上の性質のreal上への書き換えであり，ここでも

thm real_of_nat_Suc

real (Suc ?n) = real ?n + 1

を用いますが，とりあえず

  then show ?case

とし，例によって

proof (simp add: field_simps del: GM.simps AM.simps)

と（GM,AMは書き換えないようdel）試すと

goal (1 subgoal):
1. real (Suc i) * GM a 0 i ≤ GM a 0 i + real i * AM a 0 i ⟹
GM a 0 i ≤ AM a 0 i

のように分母は払ってくれますので，先の real_of_nat_Suc を継いで

proof (simp add: field_simps real_of_nat_Suc del: GM.simps AM.simps)

とすれば

goal (1 subgoal):
1. real i * GM a 0 i ≤ real i * AM a 0 i ⟹ GM a 0 i ≤ AM a 0 i

まで進み，前件

thm step.prems(2)

0 < i

も加えて

proof (simp add: field_simps real_of_nat_Suc step.prems(2) del: GM.simps AM.simps)

とすれば通るので，改めて

    by (simp add: field_simps real_of_nat_Suc step.prems(2))

により

show GM a 0 i ≤ AM a 0 i
Successful attempt to solve goal by exported rule:
(?i2 < 2 ^ n) ⟹
(⋀a. ∀k. 0 ≤ a k ⟹
0 < Suc ?i2 ⟹ GM a 0 (Suc ?i2) ≤ AM a 0 (Suc ?i2)) ⟹
(∀k. 0 ≤ ?aa2 k) ⟹ (0 < ?i2) ⟹ GM ?aa2 0 ?i2 ≤ AM ?aa2 0 ?i2
proof (state): step 31

this:
GM a 0 i ≤ AM a 0 i

goal:
No subgoals!

に至り

qed

で完成です．

lemma amgm_0:
  fixes a :: "nat => real" and n
  assumes "0 < n"
  shows "ALL k. 0 <= a k ==> GM a 0 n <= AM a 0 n"
using exn2n assms
proof (induction n arbitrary: a rule: inc_induct)
  case base then show ?case
    using amgm_2 by metis
next
  case (step i a)
  let ?b = "%k. if k <= i then a k else GM a 0 i"
  have "setprod ?b {1..Suc i} = setprod a {1..i} * GM a 0 i"
    by (subgoal_tac "{1..Suc i} = insert (Suc i) {1..i}", auto)
  also have "... = GM a 0 i ^ Suc i"
    using step.prems
    by (simp add: setprod_nonneg)
  finally have "GM ?b 0 (Suc i) = GM a 0 i"
    using real_root_power_cancel [of "Suc i", OF _ GMge0 [OF step.prems, of 0]]
    by simp
  moreover have "ALL k. 0 <= ?b k"
    using step.prems GMge0
    by (metis (full_types))
  ultimately have "GM a 0 i <= (i * AM a 0 i + GM a 0 i) / Suc i"
    using step.IH [of ?b]
    by simp
  then show ?case
    by (simp add: field_simps real_of_nat_Suc step.prems(2))
qed

print_statement amgm_0

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