Theory Estimation

theory Estimation

imports Complex_Main

begin
section ‹Auxiliary lemma: Estimation›

text ‹For the proof of the mixed state O2H, we need an auxiliary lemma on the square roots of sums.›

lemma abc_ineq:
  assumes "a≥0" "b≥0" "c≥0" "¦sqrt a - sqrt b¦ ≤ sqrt c"
  shows "a + b ≤ c + 2 * sqrt (a * b)"
proof -
  have "¦sqrt a - sqrt b¦^2 ≤ sqrt c ^2" using assms by (simp add: sqrt_ge_absD)
  then show ?thesis by (auto simp add: algebra_simps power2_diff assms real_sqrt_mult)
qed

lemma two_ab_ineq:
  assumes "a≥0" "b≥0"
  shows "2 * sqrt (a * b) ≤ a + b"
proof -
  have "0 ≤ (sqrt a - sqrt b)^2" by auto
  then show ?thesis by (auto simp add: algebra_simps power2_diff assms real_sqrt_mult)
qed

lemma sqrt_estimate_real:
  assumes fin_M: "finite M" 
    and pos_t: "∀x∈M. t x ≥ (0::real)" 
    and pos_u: "∀x∈M. u x ≥ (0::real)" 
    and pos_v: "∀x∈M. v x ≥ (0::real)" 
    and pos_a: "∀x∈M. a x ≥ (0::real)"
    and ineq:  "∀x∈M. ¦ sqrt (t x) - sqrt (u x)¦ ≤ sqrt (v x)"
  shows "¦sqrt (∑x∈M. a x * t x) - sqrt (∑x∈M. a x * u x)¦ ≤ sqrt (∑x∈M. a x * v x)"
  using assms proof (induction M)
  case empty
  then show ?case by auto
next
  case (insert y N)
  define tN where "tN = (∑x∈N. a x * t x)"
  have pos_tN[simp]: "0 ≤ tN" unfolding tN_def by (simp add: insert.prems(1) insert.prems(4) sum_nonneg)
  define uN where "uN = (∑x∈N. a x * u x)"
  have pos_uN[simp]: "0 ≤ uN" unfolding uN_def by (simp add: insert.prems(2) insert.prems(4) sum_nonneg)
  define vN where "vN = (∑x∈N. a x * v x)"
  have pos_vN[simp]: "0 ≤ vN" unfolding vN_def by (simp add: insert.prems(3) insert.prems(4) sum_nonneg)
  have ineqN: "¦sqrt tN - sqrt uN¦ ≤ sqrt vN"
    by (simp add: insert.prems(1,4) insert(3,5,6,8) tN_def uN_def vN_def)
  have 2: "tN + uN ≤ vN + 2 * sqrt (tN * uN)" 
    by (intro abc_ineq)(auto simp add: ineqN)
  have "a y ≥ 0" using insert by auto
  have "3a": "t y + u y ≤ v y + 2 * sqrt (t y * u y)" by (intro abc_ineq) (auto simp add: insert)
  have 3: "a y * t y + a y * u y ≤ a y * v y + 2 * a y * sqrt (t y * u y)"
    by (use mult_left_mono[OF "3a" ‹a y ≥ 0›] in ‹auto simp add: algebra_simps›)
  have 5: "sqrt ((tN + a y * t y) * (uN + a y * u y)) ≥ sqrt (tN * uN) + a y * sqrt (t y * u y)"
  proof -
    have "(sqrt (tN * uN) + a y * sqrt (t y * u y)) ^2 = tN * uN + (a y)^2 * t y * u y 
      + 2 * a y * sqrt (tN * uN * t y * u y)"
      by (auto simp add: algebra_simps power2_sum insert real_sqrt_mult[symmetric])
    also have "… = tN * uN + (a y)^2 * t y * u y + 2 * sqrt ((a y)^2 * tN * uN * t y * u y)"
      by (auto simp add: real_sqrt_mult ‹a y ≥ 0›)
    also have "… = tN * uN + (a y)^2 * t y * u y + 2 * sqrt ((a y * tN * u y) * (a y * uN * t y))"
      by (auto simp add: algebra_simps power2_eq_square)
    also have "… ≤ tN * uN + (a y)^2 * t y * u y + a y * tN * u y + a y * uN * t y"
      using two_ab_ineq[of "a y * tN * u y" "a y * uN * t y"] by (auto simp add: insert)
    also have "… = sqrt ((tN + a y * t y) * (uN + a y * u y))^2" using real_sqrt_pow2 
      by (auto simp add: insert algebra_simps power2_eq_square)
    finally show ?thesis by (simp add: ‹0 ≤ a y› insert(4,5) real_le_rsqrt)
  qed
  have "¦sqrt (∑x∈insert y N. a x * t x) - sqrt (∑x∈insert y N. a x * u x)¦ = 
    ¦sqrt (tN + a y * t y) - sqrt (uN + a y * u y)¦"
    by (subst sum.insert[OF insert(1,2)])+ (auto simp add: tN_def uN_def algebra_simps)
  also have "… ≤ sqrt (vN + a y * v y)"
  proof -
    have "¦sqrt (tN + a y * t y) - sqrt (uN + a y * u y)¦^2 = 
      tN + a y * t y + uN + a y * u y - 2 * sqrt((tN + a y * t y) * (uN + a y * u y))" 
      by (auto simp add: algebra_simps power2_diff insert real_sqrt_mult[symmetric])
    also have "… ≤ vN + a y * v y + 2 * sqrt(tN * uN) + 2* a y * sqrt (t y * u y) - 
      2 * sqrt ((tN + a y * t y) * (uN + a y * u y))"
      using 2 3 by auto
    finally have "¦sqrt (tN + a y * t y) - sqrt (uN + a y * u y)¦^2 ≤ vN + a y * v y" 
      using 5 by auto
    then show ?thesis using real_le_rsqrt by blast
  qed
  also have "… = sqrt (∑x∈insert y N. a x * v x)"
    by (subst sum.insert[OF insert(1,2)]) (auto simp add: vN_def)
  finally show ?case by linarith
qed



end