凸不等式

　これも HOL Light で書いた定理ですが，Isar では．．．

theory convex imports Complex_Main begin

theorem convex:
  fixes a b :: real and n :: nat
  assumes "0 <= a" and "0 <= b"
  shows "((a + b) / 2) ^ n <= (a ^ n + b ^ n) / 2" (is "?L n <= ?R n")
proof (induct n)
  case 0 show ?case by auto
next
  case (Suc n)
(*lemma*)
  have 1: "0 <= (a - b) * (a ^ n - b ^ n) / 4" (is "0 <= ?P")
    apply simp
find_theorems "0 <= ?x * ?y"
    apply (rule split_mult_pos_le)
find_theorems "?a ^ ?n <= ?b ^ ?n"
    using assms power_mono by smt
(*main*)
  have "?L (Suc n) = ?L (Suc 0) * ?L n"
    by auto
  also have "... <= ?L (Suc 0) * ?R n"
find_theorems "?a * ?x <= ?a * ?y"
    using Suc by (rule mult_left_mono) (simp add: assms)
  also have "... = ?R (Suc n) - ?P"
    by (simp add: field_simps)
  finally show ?case using 1 by arith
qed

print_statement convex

end

theorem convex:
fixes a :: "real"
and b :: "real"
and n :: "nat"
assumes "0 ≤ a"
and "0 ≤ b"
shows "((a + b) / 2) ^ n ≤ (a ^ n + b ^ n) / 2"

　?case を用いない方が見易い？

theorem convex2:
  fixes a b :: real and n :: nat
  assumes "0 <= a" and "0 <= b"
  shows "((a + b) / 2) ^ n <= (a ^ n + b ^ n) / 2" (is "?L n <= ?R n" is "?LR n")
proof (induct n)
  show "?LR 0" by auto
next
  fix n
(*lemma*)
  have "0 <= (a - b) * (a ^ n - b ^ n) / 4" (is "0 <= ?P")
    apply (simp, rule split_mult_pos_le)
    using assms power_mono by smt
(*main*)
  assume "?LR n"
  then have "?L (Suc n) <= (a + b) / 2 * ?R n"
    apply (subst power_Suc, rule mult_left_mono)
    using assms by auto
  also have "... = ?R (Suc n) - ?P"
    by (simp add: field_simps)
  finally show "?LR (Suc n)"
    using `0 <= ?P` by arith
qed