(*  Title:       The Cauchy-Schwarz Inequality
    Author:      Benjamin Porter <Benjamin.Porter at gmail.com>, 2006
    Maintainer:  Benjamin Porter <Benjamin.Porter at gmail.com>
*)

chapter ‹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_sq_exp = power_mult_distrib [where 'a = real and ?n = 2]

(*>*)



section ‹Abstract›

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

 \em Theorem:} Take $V$ to be some vector space possessing a norm and
  product, then for all $a,b \in V$ the following inequality
 : ‹∣a⋅b∣ ≤ ∥a∥*∥b∥›. Specifically, in the Real case, the
  is the Euclidean length and the inner product is the standard dot
 .›


section ‹Formal Proof›

subsection ‹Vector, Dot and Norm definitions.›

text ‹This section presents definitions for a real vector type, a
  product function and a norm function.›

subsubsection ‹Vector›

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

type_synonym 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
  $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)}. a*b)"

definition
  norm :: "vector → real"                  (‹∥_∥› 100) where
  "norm v = sqrt (∑j∈{1..(vlen v)}. v^2)"

text ‹Another definition of the norm is @{term "∥v∥ = sqrt
 v⋅v)"}. We show that our definition leads to this one.›

lemma norm_dot: "∥v∥ = sqrt (v⋅v)"
  using dot_def norm_def real_sq by presburger

text ‹A further important property is that the norm is never negative.›

lemma norm_pos:
  "∥v∥ ≥ 0"
  by (simp add: norm_def sum_nonneg)

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))"
    using sum.swap by force 
  also have
    "… =
    (∑k∈{1..n}. (∑j∈{1..n}. f k * g j + f j * g k))"
    by (auto simp add: sum.distrib)
  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: sum_distrib_left 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
  that uses properties of double summation and the preceding
 .›

theorem CauchySchwarzReal:
  fixes x::vector
  assumes "vlen x = vlen y"
  shows "∣x⋅y∣ ≤ ∥x∥*∥y∥"
proof -
  have "∣x⋅y∣^2 ≤ (∥x∥*∥y∥)^2"
  proof -
    txt ‹We can rewrite the goal in the following form ...›
    have "(∥x∥*∥y∥)^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}. x^2) ≥ 0" by (simp add: sum_nonneg)
        hence xp: "(sqrt (∑j∈{1..n}. x^2))^2 = (∑j∈{1..n}. x^2)"
          by (rule real_sqrt_pow2)

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

        txt ‹The main result of this section is that ‹(∥x∥*∥y∥)^2› can be written as a double sum.›
        have "(∥x∥*∥y∥)^2 = ∥x∥^2 * ∥y∥^2"
          by (simp add: real_sq_exp)
        also from nx ny have
          "… = (sqrt (∑j∈{1..n}. x^2))^2 * (sqrt (∑j∈{1..n}. y^2))^2"
          unfolding norm_def by auto
        also from xp yp have
          "… = (∑j∈{1..n}. x^2)*(∑j∈{1..n}. y^2)"
          by simp
        also from sum_product have
          "… = (∑k∈{1..n}. (∑j∈{1..n}. (x^2)*(y^2)))" .
        finally have
          "(∥x∥*∥y∥)^2 = (∑k∈{1..n}. (∑j∈{1..n}. (x^2)*(y^2)))" .
      }
      moreover
      txt ‹We also show that ‹∣x⋅y∣^2› can be expressed as a double sum.›
      have "∣x⋅y∣^2 = (∑k∈{1..n}. (∑j∈{1..n}. (x*y)*(x*y)))"
        by (metis (no_types) dot_def nx power2_abs real_sq sum_product) 
      txt ‹We now manipulate the double sum expressions to get the
 required inequality.›
      ultimately have
        "(∥x∥*∥y∥)^2 - ∣x⋅y∣^2 =
         (∑k∈{1..n}. (∑j∈{1..n}. (x^2)*(y^2))) -
         (∑k∈{1..n}. (∑j∈{1..n}. (x*y)*(x*y)))"
        by simp
      also have
        "… =
         (∑k∈{1..n}. (∑j∈{1..n}. ((x^2*y^2) + (x^2*y^2))/2)) -
         (∑k∈{1..n}. (∑j∈{1..n}. (x*y)*(x*y)))"
        by (simp only: double_sum_aux)
      also have
        "… =
         (∑k∈{1..n}. (∑j∈{1..n}. ((x^2*y^2) + (x^2*y^2))/2 - (x*y)*(x*y)))"
        by (auto simp add: sum_subtractf)
      also have
        "… =
         (∑k∈{1..n}. (∑j∈{1..n}. (inverse 2)*2*
         (((x^2*y^2) + (x^2*y^2))*(1/2) - (x*y)*(x*y))))"
        by auto
      also have
        "… =
         (∑k∈{1..n}. (∑j∈{1..n}. (inverse 2)*(2*
        (((x^2*y^2) + (x^2*y^2))*(1/2) - (x*y)*(x*y)))))"
        by (simp only: mult.assoc)
      also have
        "… =
         (∑k∈{1..n}. (∑j∈{1..n}. (inverse 2)*
        ((((x^2*y^2) + (x^2*y^2))*2*(inverse 2) - 2*(x*y)*(x*y)))))"
        by (auto simp add: distrib_right mult.assoc ac_simps)
      also have
        "… =
        (∑k∈{1..n}. (∑j∈{1..n}. (inverse 2)*
        ((((x^2*y^2) + (x^2*y^2)) - 2*(x*y)*(x*y)))))"
        unfolding mult.assoc by simp
      also have
        "… =
         (inverse 2)*(∑k∈{1..n}. (∑j∈{1..n}.
         (((x^2*y^2) + (x^2*y^2)) - 2*(x*y)*(x*y))))"
        by (simp only: sum_distrib_left)
      also have
        "… =
         (inverse 2)*(∑k∈{1..n}. (∑j∈{1..n}. (x*y - x*y)^2))"
        by (simp only: power2_diff real_sq_exp, auto simp add: ac_simps)
      also have "… ≥ 0"
        by (simp add: sum_nonneg)
      finally show "(∥x∥*∥y∥)^2 - ∣x⋅y∣^2 ≥ 0" .
    qed
    thus ?thesis by simp
  qed
  moreover have "0 ≤ ∥x∥*∥y∥"
    by (auto simp add: norm_pos)
  ultimately show ?thesis by (rule power2_le_imp_le)
qed

end