*To*: "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*Subject*: [isabelle] Help with Cauchy Schwarz*From*: RF Todd <R.F.Todd at sms.ed.ac.uk>*Date*: Wed, 28 Nov 2007 22:23:17 +0000

Hi,

theory CauchySchwarz imports Complex_Main begin lemma real_sq: "(a::real)*a = a^2" proof - have "2 = Suc 1" by simp hence "a^2 = a^(Suc 1)" apply - apply (erule subst) by simp also have "\<dots> = a*(a^1)" by simp also have "\<dots> = a*a" by simp finally have "a^2 = a*a" by auto thus ?thesis by simp qed lemma real_mult_wkorder: fixes x::real assumes xge0: "0 \<le> x" and yge0: "0 \<le> y" shows "0 \<le> x*y" proof cases assume "x = 0" thus ?thesis by simp next assume "x \<noteq> 0" with xge0 have xgt0: "x > 0" by simp show ?thesis proof cases assume "y = 0" thus ?thesis by simp next assume "y \<noteq> 0" with yge0 have "y > 0" by simp with xgt0 have "x*y > 0" by (rule real_mult_order) thus ?thesis by simp qed qed lemma real_mult_order2: fixes c::real assumes c0: "0 \<le> c" and xy: "x \<le> y" shows "c*x \<le> c*y" proof cases assume "0 = c" thus ?thesis by auto next assume "0 \<noteq> c" with c0 have "0 < c" by simp with xy show ?thesis by simp qed lemma real_sq_order: fixes x::real assumes xgt0: "0 \<le> x" and ygt0: "0 \<le> y" and sq: "x^2 \<le> y^2" shows "x \<le> y" proof (rule ccontr) assume "\<not>(x \<le> y)" then have ylx: "y < x" by simp hence "y \<le> x" by simp with xgt0 have "x*y \<le> x*x" by (rule real_mult_order2) moreover have "\<not>(y = 0)" proof assume "y = 0" with ylx have xg0: "0 < x" by simp from xg0 xg0 have "0 < x*x" by (rule real_mult_order) moreover have "y*y = 0" by simp ultimately show False using sq by auto qed with ygt0 have "0 < y" by simp with ylx have "y*y < x*y" by auto ultimately have "y*y < x*x" by simp with sq show False by (auto simp add: real_sq) qed 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 "\<dots> = y*x + z*x" by (rule real_add_mult_distrib) also have "\<dots> = 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 + x*w + y*z + y*w" proof - have "(x+y)*(z+w) = x*(z+w) + y*(z+w)" by (rule real_add_mult_distrib)

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

finally show ?thesis by simp qed lemma double_sum_expand: fixes f::"nat \<Rightarrow> real"

proof (induct n) case 0 show ?case by simp next case (Suc n) { assume nz: "n = 0" then have

moreover from nz have

ultimately have ?case by simp } moreover { assume "\<not>(n = 0)" then have nge1: "n \<ge> 1" by simp hence sn: "Suc n > 1" by simp let ?f = "\<Sum>j\<in>{1..n}. f j" and ?g = "\<Sum>j\<in>{1..n}. g j"

moreover

ultimately have

also have

by (auto simp add: real_add_mult_distrib_ex) also have

also have

also have

also have

also have

also from sn setsum_cl_ivl_Suc have

also from sn setsum_cl_ivl_Suc have

finally have ?case . } ultimately show ?case by (rule case_split_thm) qed lemma real_sq_exp: fixes x::real shows "(x*y)^2 = x^2 * y^2" proof - have "(x*y)^2 = (x*y)*(x*y)" by (simp add: real_sq) also have "\<dots> = (x*x)*(y*y)" by simp also have "\<dots> = x^2 * y^2" by (simp add: real_sq) finally show ?thesis . qed 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)

finally show ?thesis by (auto simp add: real_sq) qed lemma double_sum_equiv: fixes f::"nat \<Rightarrow> real"

proof -

finally show ?thesis by (simp add: real_mult_commute) qed

types vector = "(nat \<Rightarrow> real)*nat"; constdefs ith :: "vector \<Rightarrow> nat \<Rightarrow> real" "ith v i \<equiv> (fst v) i" vlen :: "vector \<Rightarrow> nat" "vlen v \<equiv> (snd v)" constdefs dot :: "vector \<Rightarrow> vector \<Rightarrow> real" "dot a b \<equiv> (\<Sum>j\<in>{1..(vlen a)}.(ith a j)*(ith b j))" norm :: "vector \<Rightarrow> real" "norm v \<equiv> sqrt (\<Sum>j\<in>{1..(vlen v)}.(ith v j)^2)" syntax(HTML output) "norm" :: "vector \<Rightarrow> real" lemma norm_dot: "norm(v)=sqrt(dot v v)" proof -

also have "\<dots> = norm v" by (unfold norm_def, simp) finally show ?thesis .. qed lemma norm_pos: "norm v \<ge> 0" proof - have "\<forall>j. (ith v j)^2 \<ge> 0" by (unfold ith_def, auto) hence "\<forall>j\<in>{1..(vlen v)}. (ith v j)^2 \<ge> 0" by simp with setsum_nonneg have "(\<Sum>j\<in>{1..(vlen v)}. (ith v j)^2) \<ge> 0" .

thus ?thesis by (unfold norm_def) qed lemma double_sum_aux: fixes f::"nat \<Rightarrow> real"

proof -

finally show ?thesis by (auto simp add: inverse_eq_divide) qed theorem CauchySchwarzReal: fixes x::vector assumes "vlen x = vlen y" shows "\<bar>dot x y\<bar> \<le> (norm x)*(norm y)" proof - have "0 \<le> \<bar>dot x y\<bar>" by simp

moreover have "\<bar>dot x y\<bar>^2 \<le> ((norm x)*(norm y))^2" proof - txt {* We can rewrite the goal in the following form \<dots> *} have "((norm x)*(norm y))^2 - \<bar>dot x y\<bar>^2 \<ge> 0" proof - obtain n where nx: "n = vlen x" by simp hence ny: "n = vlen y" by simp { txt {* Some preliminary simplification rules. *} have "\<forall>j\<in>{1..n}. (ith x j)^2 \<ge> 0" by simp

thm real_sqrt_pow2 have "\<forall>j\<in>{1..n}.(ith y j)^2 \<ge> 0" by simp hence "(\<Sum>j\<in>{1..n}.(ith y j)^2) \<ge> 0" by (rule setsum_nonneg)

} moreover {

have "\<bar>dot x y\<bar>^2 = (dot x y)^2" by simp

}

-- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.

**Follow-Ups**:**Re: [isabelle] Help with Cauchy Schwarz***From:*Lawrence Paulson

- Previous by Date: Re: [isabelle] ProofGeneral 3.7pre071112 gets out of sync with Isabelle process
- Next by Date: Re: [isabelle] converting a multiset to a list
- Previous by Thread: Re: [isabelle] converting a multiset to a list
- Next by Thread: Re: [isabelle] Help with Cauchy Schwarz
- Cl-isabelle-users November 2007 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list