Theory Lemmas_log

theory Lemmas_log
imports Complex_Main
begin

lemma ld_sum_inequality:
  assumes "x > 0" "y > 0"
  shows   "log 2 x + log 2 y + 2 ≤ 2 * log 2 (x + y)"
proof -
  have 0: "0 ≤ (x-y)^2" using assms by(simp)
  have "2 powr (2 + log 2 x + log 2 y) = 4 * x * y" using assms
    by(simp add: powr_add)
  also have "4*x*y ≤ (x+y)^2" using 0 by(simp add: algebra_simps numeral_eq_Suc)
  also have "… = 2 powr (log 2 (x + y) * 2)" using assms
    by(simp add: powr_powr[symmetric] powr_numeral)
  finally show ?thesis by (simp add: mult_ac)
qed

lemma ld_ld_1_less:
  "⟦x > 0; y > 0 ⟧ ⟹ 1 + log 2 x + log 2 y < 2 * log 2 (x+y)"
using ld_sum_inequality[of x y] by linarith
(*
proof -
  have 1: "2*x*y < (x+y)^2" using assms
    by(simp add: numeral_eq_Suc algebra_simps add_pos_pos)
  show ?thesis
    apply(rule powr_less_cancel_iff[of 2, THEN iffD1])
     apply simp
    using assms 1 by(simp add: powr_add log_powr[symmetric] powr_numeral)
qed
*)

lemma ld_le_2ld:
  assumes "x ≥ 0" "y ≥ 0" shows "log 2 (1+x+y) ≤ 1 + log 2 (1+x) + log 2 (1+y)"
proof -
  have 1: "1+x+y ≤ (x+1)*(y+1)" using assms
    by(simp add: algebra_simps)
  show ?thesis
    apply(rule powr_le_cancel_iff[of 2, THEN iffD1])
     apply simp
    using assms 1 by(simp add: powr_add algebra_simps)
qed

lemma ld_ld_less2: assumes "x ≥ 2" "y ≥ 2"
  shows "1 + log 2 x + log 2 y ≤ 2 * log 2 (x + y - 1)"
proof-
  from assms have "2*x ≤ x*x" "2*y ≤ y*y" by simp_all
  hence 1: "2 * x * y ≤ (x + y - 1)^2"
    by(simp add: numeral_eq_Suc algebra_simps)
  show ?thesis
    apply(rule powr_le_cancel_iff[of 2, THEN iffD1])
     apply simp
    using assms 1 by(simp add: powr_add log_powr[symmetric] powr_numeral)
qed

end