# Theory L2_Norm

```(*  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)⇧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
done

lemma L2_set_left_distrib:
"0 ≤ r ⟹ L2_set f A * r = L2_set (λx. f x * r) A"
unfolding L2_set_def
done

lemma L2_set_eq_0_iff: "finite A ⟹ L2_set f A = 0 ⟷ (∀x∈A. f x = 0)"
unfolding L2_set_def

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)⇧2 + (L2_set (λi. f i + g i) F)⇧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
also have
"… ≤ sqrt ((f x)⇧2 + (L2_set f F)⇧2) + sqrt ((g x)⇧2 + (L2_set g F)⇧2)"
by (rule real_sqrt_sum_squares_triangle_ineq)
finally show ?case
using insert by simp
qed
qed

lemma L2_set_le_sum [rule_format]:
"(∀i∈A. 0 ≤ f i) ⟶ L2_set f A ≤ sum f A"
apply (cases "finite A")
apply (induct set: finite)
apply simp
apply clarsimp
apply (erule order_trans [OF sqrt_sum_squares_le_sum])
apply simp
apply simp
apply simp
done

lemma L2_set_le_sum_abs: "L2_set f A ≤ (∑i∈A. ¦f i¦)"
apply (cases "finite A")
apply (induct set: finite)
apply simp
apply simp
apply (rule order_trans [OF sqrt_sum_squares_le_sum_abs])
apply simp
apply simp
done

lemma L2_set_mult_ineq: "(∑i∈A. ¦f i¦ * ¦g i¦) ≤ L2_set f A * L2_set g A"
apply (cases "finite A")
apply (induct set: finite)
apply simp
apply (rule power2_le_imp_le, simp)
apply (rule order_trans)
apply (rule power_mono)