Email Gateway (Aug 18 2022 at 10:59): Email Gateway (Aug 18 2022 at 10:59):From: RF Todd <R.F.Todd@sms.ed.ac.uk>
Hi all,
I am trying to get the following code2run but it comes up with an
Illegal Command error at the 'hence' in the lemma double_sum_aux: and
i wonder if you know why? I am new to Isabelle/Isar so not too sure
how to make it work.
Rachel
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 "cx \<le> cy"
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 "xy \<le> xx" 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 "yy < xy" by auto
ultimately have "yy < xx" 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) = xy + x*z"
proof -
have "x(y+z) = (y+z)x" by simp
also have "\<dots> = yx + zx" by (rule real_add_mult_distrib)
also have "\<dots> = xy + xz" by simp
finally show ?thesis .
qed
lemma real_add_mult_distrib_ex:
fixes x::real
shows "(x+y)(z+w) = xz + xw + yz + y*w"
proof -
have "(x+y)(z+w) = x(z+w) + y*(z+w)" by (rule real_add_mult_distrib)
also have "\<dots> = xz + xw + yz + yw" 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) = xz - xw - yz + 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
also have "\<dots> = xz + x-w + -yz + -y-w" by (simp add:
real_add_mult_distrib2)
finally show ?thesis by simp
qed
lemma double_sum_expand:
fixes f::"nat \<Rightarrow> real"
shows "(\<Sum>j\<in>{1..n}. f j)*(\<Sum>j\<in>{1..n}. g j) =
(\<Sum>k\<in>{1..n}.(\<Sum>j\<in>{1..n}.f k*g j))"
proof (induct n)
case 0 show ?case by simp
next
case (Suc n) {
assume nz: "n = 0"
then have
"(\<Sum>j\<in>{1..Suc n}. f j)*(\<Sum>j\<in>{1..Suc n}. g j) =
f 1 * g 1" by simp
moreover from nz have
"(\<Sum>k\<in>{1..Suc n}.(\<Sum>j\<in>{1..Suc n}.(f k)*(g j)))
= f 1 * g 1" by auto
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"
from sn setsum_cl_ivl_Suc have "(\<Sum>j\<in>{1..Suc n}. f j) = ?f
f (Suc n)" by auto
moreover
from sn setsum_cl_ivl_Suc have "(\<Sum>j\<in>{1..Suc n}. g j) = ?g
g (Suc n)" by auto
ultimately have
"(\<Sum>j\<in>{1..Suc n}. f j)*(\<Sum>j\<in>{1..Suc n}. g j) =
(?f + f (Suc n))*(?g + g (Suc n))" by simp
also have
"\<dots> = ?f * ?g + ?f(g (Suc n)) + (f (Suc n))?g + (f (Suc
n))*(g (Suc n))"
by (auto simp add: real_add_mult_distrib_ex)
also have
"\<dots> = (\<Sum>k\<in>{1..n}.(\<Sum>j\<in>{1..n}.(f k)*(g j)))
?f(g (Suc n)) + (f (Suc n))?g + (f (Suc n))*(g (Suc n))" using Suc
by simp
also have
"\<dots> = (\<Sum>k\<in>{1..n}.(\<Sum>j\<in>{1..n}.(f k)*(g j)))
(\<Sum>j\<in>{1..n}. f j * g (Suc n)) + ?g * (f (Suc n)) + (f (Suc
n))*(g (Suc n))" by (auto simp add: setsum_mult real_mult_commute)
also have
"\<dots> = (\<Sum>k\<in>{1..n}.(\<Sum>j\<in>{1..n}.(f k)*(g j)) +
(f k * g (Suc n))) + (?g * f (Suc n)) + (f (Suc n))*(g (Suc n))" by
(auto simp add: setsum_addf [symmetric])
also have
"\<dots> = (\<Sum>k\<in>{1..n}.(\<Sum>j\<in>{1..(Suc n)}.(f k)*(g
j))) + (\<Sum>j\<in>{1..n}. g j)(f (Suc n)) + g(Suc n)(f (Suc n))"
by simp
also have
"\<dots> = (\<Sum>k\<in>{1..n}.(\<Sum>j\<in>{1..(Suc n)}.(f k)*(g
j))) + (\<Sum>j\<in>{1..n}.g j * f (Suc n)) + g(Suc n)*(f (Suc n))" by
(auto simp add: setsum_mult real_mult_commute)
also from sn setsum_cl_ivl_Suc have
"\<dots> = (\<Sum>k\<in>{1..n}.(\<Sum>j\<in>{1..(Suc n)}.(f k)*(g
j))) + (\<Sum>j\<in>{1..Suc n}.(g j)*(f (Suc n)))" by auto
also from sn setsum_cl_ivl_Suc have
"\<dots> = (\<Sum>k\<in>{1..Suc n}.(\<Sum>j\<in>{1..(Suc n)}.(f
k)*(g j)))" by (auto simp add: real_mult_commute)
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 = (xy)(x*y)" by (simp add: real_sq)
also have "\<dots> = (xx)(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 - 2xy"
proof -
have "(x-y)^2 = (x-y)*(x-y)" by (simp only: real_sq)
also from real_sub_mult_distrib_ex have "\<dots> = xx - xy - y*x
lemma double_sum_equiv:
fixes f::"nat \<Rightarrow> real"
shows "(\<Sum>k\<in>{1..n}.(\<Sum>j\<in>{1..n}. f k * g j)) =
(\<Sum>k\<in>{1..n}.(\<Sum>j\<in>{1..n}. f j * g k))"
proof -
have "(\<Sum>k\<in>{1..n}.(\<Sum>j\<in>{1..n}. (f k)*(g j))) =
(\<Sum>j\<in>{1..n}.f j)*(\<Sum>j\<in>{1..n}.g j)" by (simp only:
double_sum_expand)
also have "\<dots> = (\<Sum>j\<in>{1..n}. g j)*(\<Sum>j\<in>{1..n}.
f j)" by simp
also have "\<dots> = (\<Sum>k\<in>{1..n}.(\<Sum>j\<in>{1..n}. g k *
f j))" by (simp only: double_sum_expand)
finally show ?thesis by (simp add: real_mult_commute)
qed
text {* 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| \<le> \<parallel>a\<parallel> *
\<parallel>b\<parallel>"}. Specifically, in the Real case, the norm is
in the Euclidean length and the inner product is the standard dot
product. *}
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 -
have "sqrt(dot v v) = sqrt(\<Sum>j\<in>{1..(vlen v)}. (ith v
j)*(ith v j))" by (unfold dot_def, simp)
also with real_sq have "\<dots> = sqrt(\<Sum>j\<in>{1..(vlen
v)}.(ith v j)^2)" by simp
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" .
with real_sqrt_ge_zero have "sqrt(\<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"
shows "(\<Sum>k\<in>{1..n}.(\<Sum>j\<in>{1..n}. f k * g j)) =
(\<Sum>k\<in>{1..n}.(\<Sum>j\<in>{1..n}.(f k * g j + f j * g k)/2))"
proof -
have "2 * (\<Sum>k\<in>{1..n}.(\<Sum>j\<in>{1..n}. f k * g j)) =
(\<Sum>k\<in>{1..n}.(\<Sum>j\<in>{1..n}. f k * g j)) +
(\<Sum>k\<in>{1..n}.(\<Sum>j\<in>{1..n}. f k * g j))" by simp
also have "\<dots> = (\<Sum>k\<in>{1..n}.(\<Sum>j\<in>{1..n}. f k *
g j)) + (\<Sum>k\<in>{1..n}.(\<Sum>j\<in>{1..n}. f j * g k))" by (simp
only: double_sum_equiv)
also have "\<dots> = (\<Sum>k\<in>{1..n}.(\<Sum>j\<in>{1..n}. f k *
g j + f j * g k))" by (auto simp add: setsum_addf)
finally have "2 * (\<Sum>k\<in>{1..n}.(\<Sum>j\<in>{1..n}. f k * g
j)) = (\<Sum>k\<in>{1..n}.(\<Sum>j\<in>{1..n}. f k * g j + f j * g k))"
hence "(\<Sum>k\<in>{1..n}.(\<Sum>j\<in>{1..n}. f k * g j)) =
(\<Sum>k\<in>{1..n}.(\<Sum>j\<in>{1..n}.(f k * g j + f j * g
k)))*(1/2)" by auto
also have "\<dots> = (\<Sum>k\<in>{1..n}.(\<Sum>j\<in>{1..n}.(f k *
g j + f j* g k)*(1/2)))" by (simp add: setsum_mult real_mult_commute)
finally show ?thesis by (auto simp add: inverse_eq_divide)
qed
theorem CauchySchwarzReal:
fixes x::vector
assumes "vlen x = vlen y"
shows "|dot x y| \<le> (norm x)*(norm y)"
proof -
have "0 \<le> |dot x y|" by simp
moreover have "0 \<le> (norm x)*(norm y)" by (auto simp add:
norm_pos intro: mult_nonneg_nonneg)
moreover have "|dot x y|^2 \<le> ((norm x)*(norm y))^2"
proof -
txt {*
[message truncated]
Email Gateway (Aug 18 2022 at 10:59):From: Tobias Nipkow <nipkow@in.tum.de>
Looks like the justification for the previous line is missing.
Tobias
RF Todd schrieb:
Last updated: May 03 2024 at 04:19 UTC