amgm2

　この結果の右辺は引き続き用いるので

also

とすれば

calculation:
GM a m (2 ^ Suc N) = root 2 (GM a m (2 ^ N) * GM a (m + 2 ^ N) (2 ^ N))

のように記憶され，右辺が...で参照できます．

　従って，次は

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

を示すことになりますが，これには項数が２の場合の不等式が入用ですので，今回の定理に先立ち

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)

のように準備しておきます．方針は非負値である(root 2 x - root 2 y)^2を展開し，根号を整理するというもので，参照する定理は

thm zero_le_power2 power2_diff real_root_mult

0 ≤ ?a²
(?x - ?y)² = ?x² + ?y² - 2 * ?x * ?y
0 < ?n ⟹ root ?n (?x * ?y) = root ?n ?x * root ?n ?y

の３つです．大体のマッチングはsimpにもできますが，１つ目はさすがに無理なので ?a として "root 2 x - root 2 y" を明示してやります

thm zero_le_power2 [of "root 2 x - root 2 y"]

0 ≤ (root 2 x - root 2 y)²

指定の方法は

thm zero_le_power2 [where a = "root 2 x - root 2 y"]

などでも構いません．なお

NthRoot.real_root_pow_pos2: 0 < ?n ⟹ 0 ≤ ?x ⟹ root ?n ?x ^ ?n = ?x

はsimp属性を持っていますので，自動的に適用されます．