Theory CauchySchwarz

(*  Title:       The Cauchy-Schwarz Inequality
    ID:          $Id: CauchySchwarz.thy,v 1.5 2007/06/13 20:14:38 makarius Exp $
    Author:      Benjamin Porter <Benjamin.Porter at gmail.com>, 2006
    Maintainer:  Benjamin Porter <Benjamin.Porter at gmail.com>
*)

header {* The Cauchy-Schwarz Inequality *}

theory CauchySchwarz
imports Complex_Main
begin

(*<*)

(* Some basic results that don't need to be in the final doc ..*)


lemmas real_sq = power2_eq_square [where 'a = real, symmetric]
lemmas real_mult_wkorder = mult_nonneg_nonneg [where 'a = real]

lemma real_add_mult_distrib2:
  fixes x::real
  shows "x*(y+z) = x*y + x*z"
proof -
  have "x*(y+z) = (y+z)*x" by simp
  also have "… = y*x + z*x" by (rule real_add_mult_distrib)
  also have "… = x*y + x*z" by simp
  finally show ?thesis .
qed

lemma real_add_mult_distrib_ex:
  fixes x::real
  shows "(x+y)*(z+w) = x*z + y*z + x*w + y*w"
proof -
  have "(x+y)*(z+w) = x*(z+w) + y*(z+w)" by (rule real_add_mult_distrib)
  also have "… = x*z + x*w + y*z + y*w" by (simp add: real_add_mult_distrib2)
  finally show ?thesis by simp
qed

lemma real_sub_mult_distrib_ex:
  fixes x::real
  shows "(x-y)*(z-w) = x*z - y*z - x*w + y*w"
proof -
  have zw: "(z-w) = (z+ -w)" by simp
  have "(x-y)*(z-w) = (x + -y)*(z-w)" by simp
  also have "… = x*(z-w) + -y*(z-w)" by (rule real_add_mult_distrib)
  also from zw have "… = x*(z+ -w) + -y*(z+ -w)"
    apply -
    apply (erule subst)
    by simp
  also have "… = x*z + x*-w + -y*z + -y*-w" by (simp add: real_add_mult_distrib2)
  finally show ?thesis by simp
qed

lemma setsum_product_expand:
  fixes f::"nat => real"
  shows "(∑j∈{1..n}. f j)*(∑j∈{1..n}. g j) = (∑k∈{1..n}. (∑j∈{1..n}. f k * g j))"
  by (simp add: setsum_right_distrib setsum_left_distrib) (rule setsum_commute)

lemmas real_sq_exp = power_mult_distrib [where 'a = real and ?n = 2]

lemma real_diff_exp:
  fixes x::real
  shows "(x - y)^2 = x^2 + y^2 - 2*x*y"
proof -
  have "(x - y)^2 = (x-y)*(x-y)" by (simp only: real_sq)
  also from real_sub_mult_distrib_ex have "… = x*x - x*y - y*x + y*y" by simp
  finally show ?thesis by (auto simp add: real_sq)
qed

lemma double_sum_equiv:
  fixes f::"nat => real"
  shows
  "(∑k∈{1..n}. (∑j∈{1..n}. f k * g j)) =
   (∑k∈{1..n}. (∑j∈{1..n}. f j * g k))"
  by (rule setsum_commute)

(*>*)



section {* Abstract *}

text {* The following document presents a formalised proof of the
Cauchy-Schwarz Inequality for the specific case of $R^n$. The system
used is Isabelle/Isar. 

{\em Theorem:} Take $V$ to be some vector space possessing a norm and
inner product, then for all $a,b \in V$ the following inequality
holds: @{text "¦a·b¦ ≤ \<parallel>a\<parallel>*\<parallel>b\<parallel>"}. Specifically, in the Real case, the
norm is the Euclidean length and the inner product is the standard dot
product. *}


section {* Formal Proof *}

subsection {* Vector, Dot and Norm definitions. *}

text {* This section presents definitions for a real vector type, a
dot product function and a norm function. *}

subsubsection {* Vector *}

text {* We now define a vector type to be a tuple of (function,
length). Where the function is of type @{typ "nat=>real"}. We also
define some accessor functions and appropriate notation. *}

types vector = "(nat=>real) * nat";

definition
  ith :: "vector => nat => real" ("((_)_)" [80,100] 100) where
  "ith v i = fst v i"

definition
  vlen :: "vector => nat" where
  "vlen v = snd v"

text {* Now to access the second element of some vector $v$ the syntax
is $v_2$. *}

subsubsection {* Dot and Norm *}

text {* We now define the dot product and norm operations. *}

definition
  dot :: "vector => vector => real" (infixr "·" 60) where
  "dot a b = (∑j∈{1..(vlen a)}. aj*bj)"

definition
  norm :: "vector => real"                  ("\<parallel>_\<parallel>" 100) where
  "norm v = sqrt (∑j∈{1..(vlen v)}. vj^2)"

notation (HTML output)
  "norm"  ("||_||" 100)

text {* Another definition of the norm is @{term "\<parallel>v\<parallel> = sqrt
(v·v)"}. We show that our definition leads to this one. *}

lemma norm_dot:
 "\<parallel>v\<parallel> = sqrt (v·v)"
proof -
  have "sqrt (v·v) = sqrt (∑j∈{1..(vlen v)}. vj*vj)" unfolding dot_def by simp
  also with real_sq have "… = sqrt (∑j∈{1..(vlen v)}. vj^2)" by simp
  also have "… = \<parallel>v\<parallel>" unfolding norm_def by simp
  finally show ?thesis ..
qed

text {* A further important property is that the norm is never negative. *}

lemma norm_pos:
  "\<parallel>v\<parallel> ≥ 0"
proof -
  have "∀j. vj^2 ≥ 0" unfolding ith_def by auto
  hence "∀j∈{1..(vlen v)}. vj^2 ≥ 0" by simp
  with setsum_nonneg have "(∑j∈{1..(vlen v)}. vj^2) ≥ 0" .
  with real_sqrt_ge_zero have "sqrt (∑j∈{1..(vlen v)}. vj^2) ≥ 0" .
  thus ?thesis unfolding norm_def .
qed

text {* We now prove an intermediary lemma regarding double summation. *}

lemma double_sum_aux:
  fixes f::"nat => real"
  shows
  "(∑k∈{1..n}. (∑j∈{1..n}. f k * g j)) =
   (∑k∈{1..n}. (∑j∈{1..n}. (f k * g j + f j * g k) / 2))"
proof -
  have
    "2 * (∑k∈{1..n}. (∑j∈{1..n}. f k * g j)) =
    (∑k∈{1..n}. (∑j∈{1..n}. f k * g j)) +
    (∑k∈{1..n}. (∑j∈{1..n}. f k * g j))"
    by simp
  also have
    "… =
    (∑k∈{1..n}. (∑j∈{1..n}. f k * g j)) +
    (∑k∈{1..n}. (∑j∈{1..n}. f j * g k))"
    by (simp only: double_sum_equiv)
  also have
    "… =
    (∑k∈{1..n}. (∑j∈{1..n}. f k * g j + f j * g k))"
    by (auto simp add: setsum_addf)
  finally have
    "2 * (∑k∈{1..n}. (∑j∈{1..n}. f k * g j)) =
    (∑k∈{1..n}. (∑j∈{1..n}. f k * g j + f j * g k))" .
  hence
    "(∑k∈{1..n}. (∑j∈{1..n}. f k * g j)) =
     (∑k∈{1..n}. (∑j∈{1..n}. (f k * g j + f j * g k)))*(1/2)"
    by auto
  also have
    "… =
     (∑k∈{1..n}. (∑j∈{1..n}. (f k * g j + f j * g k)*(1/2)))"
    by (simp add: setsum_right_distrib real_mult_commute)
  finally show ?thesis by (auto simp add: inverse_eq_divide)
qed

text {* The final theorem can now be proven. It is a simple forward
proof that uses properties of double summation and the preceding
lemma.  *}

theorem CauchySchwarzReal:
  fixes x::vector
  assumes "vlen x = vlen y"
  shows "¦x·y¦ ≤ \<parallel>x\<parallel>*\<parallel>y\<parallel>"
proof -
  have "0 ≤ ¦x·y¦" by simp
  moreover have "0 ≤ \<parallel>x\<parallel>*\<parallel>y\<parallel>"
    by (auto simp add: norm_pos intro: mult_nonneg_nonneg)
  moreover have "¦x·y¦^2 ≤ (\<parallel>x\<parallel>*\<parallel>y\<parallel>)^2"
  proof -
    txt {* We can rewrite the goal in the following form ...*}
    have "(\<parallel>x\<parallel>*\<parallel>y\<parallel>)^2 - ¦x·y¦^2 ≥ 0"
    proof -
      obtain n where nx: "n = vlen x" by simp
      with `vlen x = vlen y` have ny: "n = vlen y" by simp
      {
        txt {* Some preliminary simplification rules. *}
        have "∀j∈{1..n}. xj^2 ≥ 0" by simp
        hence "(∑j∈{1..n}. xj^2) ≥ 0" by (rule setsum_nonneg)
        hence xp: "(sqrt (∑j∈{1..n}. xj^2))^2 = (∑j∈{1..n}. xj^2)"
          by (rule real_sqrt_pow2)

        have "∀j∈{1..n}. yj^2 ≥ 0" by simp
        hence "(∑j∈{1..n}. yj^2) ≥ 0" by (rule setsum_nonneg)
        hence yp: "(sqrt (∑j∈{1..n}. yj^2))^2 = (∑j∈{1..n}. yj^2)"
          by (rule real_sqrt_pow2)

        txt {* The main result of this section is that @{text
        "(\<parallel>x\<parallel>*\<parallel>y\<parallel>)^2"} can be written as a double sum. *}
        have
          "(\<parallel>x\<parallel>*\<parallel>y\<parallel>)^2 = \<parallel>x\<parallel>^2 * \<parallel>y\<parallel>^2"
          by (simp add: real_sq_exp)
        also from nx ny have
          "… = (sqrt (∑j∈{1..n}. xj^2))^2 * (sqrt (∑j∈{1..n}. yj^2))^2"
          unfolding norm_def by auto
        also from xp yp have
          "… = (∑j∈{1..n}. xj^2)*(∑j∈{1..n}. yj^2)"
          by simp
        also from setsum_product_expand have
          "… = (∑k∈{1..n}. (∑j∈{1..n}. (xk^2)*(yj^2)))" .
        finally have
          "(\<parallel>x\<parallel>*\<parallel>y\<parallel>)^2 = (∑k∈{1..n}. (∑j∈{1..n}. (xk^2)*(yj^2)))" .
      }
      moreover
      {
        txt {* We also show that @{text "¦x·y¦^2"} can be expressed as a double sum.*}
        have
          "¦x·y¦^2 = (x·y)^2"
          by simp
        also from nx have
          "… = (∑j∈{1..n}. xj*yj)^2"
          unfolding dot_def by simp
        also from real_sq have
          "… = (∑j∈{1..n}. xj*yj)*(∑j∈{1..n}. xj*yj)"
          by simp
        also from setsum_product_expand have
          "… = (∑k∈{1..n}. (∑j∈{1..n}. (xk*yk)*(xj*yj)))"
          by simp
        finally have
          "¦x·y¦^2 = (∑k∈{1..n}. (∑j∈{1..n}. (xk*yk)*(xj*yj)))" .
      }
      txt {* We now manipulate the double sum expressions to get the
      required inequality. *}
      ultimately have
        "(\<parallel>x\<parallel>*\<parallel>y\<parallel>)^2 - ¦x·y¦^2 =
         (∑k∈{1..n}. (∑j∈{1..n}. (xk^2)*(yj^2))) -
         (∑k∈{1..n}. (∑j∈{1..n}. (xk*yk)*(xj*yj)))"
        by simp
      also have
        "… =
         (∑k∈{1..n}. (∑j∈{1..n}. ((xk^2*yj^2) + (xj^2*yk^2))/2)) -
         (∑k∈{1..n}. (∑j∈{1..n}. (xk*yk)*(xj*yj)))"
        by (simp only: double_sum_aux)
      also have
        "… =
         (∑k∈{1..n}.  (∑j∈{1..n}. ((xk^2*yj^2) + (xj^2*yk^2))/2 - (xk*yk)*(xj*yj)))"
        by (auto simp add: setsum_subtractf)
      also have
        "… =
         (∑k∈{1..n}.  (∑j∈{1..n}. (inverse 2)*2*
         (((xk^2*yj^2) + (xj^2*yk^2))*(1/2) - (xk*yk)*(xj*yj))))"
        by auto
      also have
        "… =
         (∑k∈{1..n}.  (∑j∈{1..n}. (inverse 2)*(2*
        (((xk^2*yj^2) + (xj^2*yk^2))*(1/2) - (xk*yk)*(xj*yj)))))"
        by (simp only: real_mult_assoc)
      also have
        "… =
         (∑k∈{1..n}.  (∑j∈{1..n}. (inverse 2)*
        ((((xk^2*yj^2) + (xj^2*yk^2))*2*(inverse 2) - 2*(xk*yk)*(xj*yj)))))"
        by (auto simp add: real_add_mult_distrib real_mult_assoc mult_ac)
      also have
        "… =
        (∑k∈{1..n}.  (∑j∈{1..n}. (inverse 2)*
        ((((xk^2*yj^2) + (xj^2*yk^2)) - 2*(xk*yk)*(xj*yj)))))"
        by (simp only: real_mult_assoc, simp)
      also have
        "… =
         (inverse 2)*(∑k∈{1..n}. (∑j∈{1..n}.
         (((xk^2*yj^2) + (xj^2*yk^2)) - 2*(xk*yk)*(xj*yj))))"
        by (simp only: setsum_right_distrib)
      also have
        "… =
         (inverse 2)*(∑k∈{1..n}. (∑j∈{1..n}. (xk*yj - xj*yk)^2))"
        by (simp only: real_diff_exp real_sq_exp, auto simp add: mult_ac)
      also have "… ≥ 0"
      proof -
        {
          fix k::nat
          have "∀j∈{1..n}. (xk*yj - xj*yk)^2 ≥ 0" by simp
          hence "(∑j∈{1..n}. (xk*yj - xj*yk)^2) ≥ 0" by (rule setsum_nonneg)
        }
        hence "∀k∈{1..n}. (∑j∈{1..n}. (xk*yj - xj*yk)^2) ≥ 0" by simp
        hence "(∑k∈{1..n}. (∑j∈{1..n}. (xk*yj - xj*yk)^2)) ≥ 0"
          by (rule setsum_nonneg)
        thus ?thesis by simp
      qed
      finally show "(\<parallel>x\<parallel>*\<parallel>y\<parallel>)^2 - ¦x·y¦^2 ≥ 0" .
    qed
    thus ?thesis by simp
  qed
  ultimately show ?thesis by (rule real_sq_order)
qed

end