Theory CauchySchwarz
chapter ‹The Cauchy-Schwarz Inequality›
theory CauchySchwarz
imports Complex_Main
begin
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
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: ‹¦a⋅b¦ ≤ ∥a∥*∥b∥›. 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.›
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
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)}. a⇘j⇙*b⇘j⇙)"
definition
norm :: "vector ⇒ real" (‹∥_∥› 100) where
"norm v = sqrt (∑j∈{1..(vlen v)}. v⇘j⇙^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
proof that uses properties of double summation and the preceding
lemma.›
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⇘j⇙^2) ≥ 0" by (simp add: sum_nonneg)
hence xp: "(sqrt (∑j∈{1..n}. x⇘j⇙^2))^2 = (∑j∈{1..n}. x⇘j⇙^2)"
by (rule real_sqrt_pow2)
have "(∑j∈{1..n}. y⇘j⇙^2) ≥ 0" by (simp add: sum_nonneg)
hence yp: "(sqrt (∑j∈{1..n}. y⇘j⇙^2))^2 = (∑j∈{1..n}. y⇘j⇙^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⇘j⇙^2))^2 * (sqrt (∑j∈{1..n}. y⇘j⇙^2))^2"
unfolding norm_def by auto
also from xp yp have
"… = (∑j∈{1..n}. x⇘j⇙^2)*(∑j∈{1..n}. y⇘j⇙^2)"
by simp
also from sum_product have
"… = (∑k∈{1..n}. (∑j∈{1..n}. (x⇘k⇙^2)*(y⇘j⇙^2)))" .
finally have
"(∥x∥*∥y∥)^2 = (∑k∈{1..n}. (∑j∈{1..n}. (x⇘k⇙^2)*(y⇘j⇙^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⇘k⇙*y⇘k⇙)*(x⇘j⇙*y⇘j⇙)))"
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⇘k⇙^2)*(y⇘j⇙^2))) -
(∑k∈{1..n}. (∑j∈{1..n}. (x⇘k⇙*y⇘k⇙)*(x⇘j⇙*y⇘j⇙)))"
by simp
also have
"… =
(∑k∈{1..n}. (∑j∈{1..n}. ((x⇘k⇙^2*y⇘j⇙^2) + (x⇘j⇙^2*y⇘k⇙^2))/2)) -
(∑k∈{1..n}. (∑j∈{1..n}. (x⇘k⇙*y⇘k⇙)*(x⇘j⇙*y⇘j⇙)))"
by (simp only: double_sum_aux)
also have
"… =
(∑k∈{1..n}. (∑j∈{1..n}. ((x⇘k⇙^2*y⇘j⇙^2) + (x⇘j⇙^2*y⇘k⇙^2))/2 - (x⇘k⇙*y⇘k⇙)*(x⇘j⇙*y⇘j⇙)))"
by (auto simp add: sum_subtractf)
also have
"… =
(∑k∈{1..n}. (∑j∈{1..n}. (inverse 2)*2*
(((x⇘k⇙^2*y⇘j⇙^2) + (x⇘j⇙^2*y⇘k⇙^2))*(1/2) - (x⇘k⇙*y⇘k⇙)*(x⇘j⇙*y⇘j⇙))))"
by auto
also have
"… =
(∑k∈{1..n}. (∑j∈{1..n}. (inverse 2)*(2*
(((x⇘k⇙^2*y⇘j⇙^2) + (x⇘j⇙^2*y⇘k⇙^2))*(1/2) - (x⇘k⇙*y⇘k⇙)*(x⇘j⇙*y⇘j⇙)))))"
by (simp only: mult.assoc)
also have
"… =
(∑k∈{1..n}. (∑j∈{1..n}. (inverse 2)*
((((x⇘k⇙^2*y⇘j⇙^2) + (x⇘j⇙^2*y⇘k⇙^2))*2*(inverse 2) - 2*(x⇘k⇙*y⇘k⇙)*(x⇘j⇙*y⇘j⇙)))))"
by (auto simp add: distrib_right mult.assoc ac_simps)
also have
"… =
(∑k∈{1..n}. (∑j∈{1..n}. (inverse 2)*
((((x⇘k⇙^2*y⇘j⇙^2) + (x⇘j⇙^2*y⇘k⇙^2)) - 2*(x⇘k⇙*y⇘k⇙)*(x⇘j⇙*y⇘j⇙)))))"
unfolding mult.assoc by simp
also have
"… =
(inverse 2)*(∑k∈{1..n}. (∑j∈{1..n}.
(((x⇘k⇙^2*y⇘j⇙^2) + (x⇘j⇙^2*y⇘k⇙^2)) - 2*(x⇘k⇙*y⇘k⇙)*(x⇘j⇙*y⇘j⇙))))"
by (simp only: sum_distrib_left)
also have
"… =
(inverse 2)*(∑k∈{1..n}. (∑j∈{1..n}. (x⇘k⇙*y⇘j⇙ - x⇘j⇙*y⇘k⇙)^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