(* Title: HOL/Analysis/L2_Norm.thy
Author: Brian Huffman, Portland State University
*)
chapter ‹Linear Algebra
›
theory L2_Norm
imports Complex_Main
begin
section ‹L2 Norm
›
definition🍋‹tag important
› L2_set ::
"('a \ real) \ 'a set \ real" where
"L2_set f A = sqrt (\i\A. (f i)\<^sup>2)"
lemma L2_set_cong:
"\A = B; \x. x \ B \ f x = g x\ \ L2_set f A = L2_set g B"
unfolding L2_set_def
by simp
lemma L2_set_cong_simp:
"\A = B; \x. x \ B =simp=> f x = g x\ \ L2_set f A = L2_set g B"
unfolding L2_set_def simp_implies_def
by simp
lemma L2_set_infinite [simp]:
"\ finite A \ L2_set f A = 0"
unfolding L2_set_def
by simp
lemma L2_set_empty [simp]:
"L2_set f {} = 0"
unfolding L2_set_def
by simp
lemma L2_set_insert [simp]:
"\finite F; a \ F\ \
L2_set f (insert a F) = sqrt ((f a)
🚫2 + (L2_set f F)
🚫2)
"
unfolding L2_set_def
by (simp add: sum_nonneg)
lemma L2_set_nonneg [simp]:
"0 \ L2_set f A"
unfolding L2_set_def
by (simp add: sum_nonneg)
lemma L2_set_0
': "\a\A. f a = 0 \ L2_set f A = 0"
unfolding L2_set_def
by simp
lemma L2_set_constant:
"L2_set (\x. y) A = sqrt (of_nat (card A)) * \y\"
unfolding L2_set_def
by (simp add: real_sqrt_mult)
lemma L2_set_mono:
assumes "\i. i \ K \ f i \ g i"
assumes "\i. i \ K \ 0 \ f i"
shows "L2_set f K \ L2_set g K"
unfolding L2_set_def
by (simp add: sum_nonneg sum_mono power_mono assms)
lemma L2_set_strict_mono:
assumes "finite K" and "K \ {}"
assumes "\i. i \ K \ f i < g i"
assumes "\i. i \ K \ 0 \ f i"
shows "L2_set f K < L2_set g K"
unfolding L2_set_def
by (simp add: sum_strict_mono power_strict_mono assms)
lemma L2_set_right_distrib:
"0 \ r \ r * L2_set f A = L2_set (\x. r * f x) A"
unfolding L2_set_def
by (simp add: power_mult_distrib real_sqrt_mult sum_nonneg flip: sum_distrib_left)
lemma L2_set_left_distrib:
"0 \ r \ L2_set f A * r = L2_set (\x. f x * r) A"
unfolding L2_set_def power_mult_distrib
by (simp add: real_sqrt_mult sum_nonneg flip: sum_distrib_right)
lemma L2_set_eq_0_iff:
"finite A \ L2_set f A = 0 \ (\x\A. f x = 0)"
unfolding L2_set_def
by (simp add: sum_nonneg sum_nonneg_eq_0_iff)
proposition L2_set_triangle_ineq:
"L2_set (\i. f i + g i) A \ L2_set f A + L2_set g A"
proof (cases
"finite A")
case False
thus ?thesis
by simp
next
case True
thus ?thesis
proof (induct set: finite)
case empty
show ?
case by simp
next
case (insert x F)
hence "sqrt ((f x + g x)\<^sup>2 + (L2_set (\i. f i + g i) F)\<^sup>2) \
sqrt ((f x + g x)
🚫2 + (L2_set f F + L2_set g F)
🚫2)
"
by (intro real_sqrt_le_mono add_left_mono power_mono insert
L2_set_nonneg add_increasing zero_le_power2)
also have
"\ \ sqrt ((f x)\<^sup>2 + (L2_set f F)\<^sup>2) + sqrt ((g x)\<^sup>2 + (L2_set g F)\<^sup>2)"
by (rule real_sqrt_sum_squares_triangle_ineq)
finally show ?
case
using insert
by simp
qed
qed
lemma L2_set_le_sum:
"(\i. i \ A \ 0 \ f i) \ L2_set f A \ sum f A"
proof (
induction A rule: infinite_finite_induct)
case (insert a A)
with order_trans [OF sqrt_sum_squares_le_sum]
show ?
case by force
qed auto
lemma L2_set_le_sum_abs:
"L2_set f A \ (\i\A. \f i\)"
proof (
induction A rule: infinite_finite_induct)
case (insert a A)
with order_trans [OF sqrt_sum_squares_le_sum_abs]
show ?
case by force
qed auto
lemma L2_set_mult_ineq:
"(\i\A. \f i\ * \g i\) \ L2_set f A * L2_set g A"
proof (
induction A rule: infinite_finite_induct)
case (insert a A)
have "(\f a\ * \g a\ + (\i\A. \f i\ * \g i\))\<^sup>2
≤ (
∣f a
∣ *
∣g a
∣ + L2_set f A * L2_set g A)
🚫2
"
by (simp add: insert.IH sum_nonneg)
also have "... \ ((f a)\<^sup>2 + (L2_set f A)\<^sup>2) * ((g a)\<^sup>2 + (L2_set g A)\<^sup>2)"
using L2_set_mult_ineq_lemma [of
"L2_set f A" "L2_set g A" "\f a\" "\g a\"]
by (simp add: power2_eq_square algebra_simps)
also have "... = (sqrt ((f a)\<^sup>2 + (L2_set f A)\<^sup>2) * sqrt ((g a)\<^sup>2 + (L2_set g A)\<^sup>2))\<^sup>2"
using real_sqrt_mult real_sqrt_sum_squares_mult_squared_eq
by presburger
finally have "(\f a\ * \g a\ + (\i\A. \f i\ * \g i\))\<^sup>2
≤ (sqrt ((f a)
🚫2 + (L2_set f A)
🚫2) * sqrt ((g a)
🚫2 + (L2_set g A)
🚫2))
🚫2
" .
then
show ?
case
using power2_le_imp_le insert.hyps
by fastforce
qed auto
lemma member_le_L2_set:
"\finite A; i \ A\ \ f i \ L2_set f A"
unfolding L2_set_def
by (auto intro!: member_le_sum real_le_rsqrt)
end
