# Theory L2_Norm

theory L2_Norm
imports NthRoot
```(*  Title:      HOL/Multivariate_Analysis/L2_Norm.thy
Author:     Brian Huffman, Portland State University
*)

section ‹Square root of sum of squares›

theory L2_Norm
imports NthRoot
begin

definition
"setL2 f A = sqrt (∑i∈A. (f i)⇧2)"

lemma setL2_cong:
"⟦A = B; ⋀x. x ∈ B ⟹ f x = g x⟧ ⟹ setL2 f A = setL2 g B"
unfolding setL2_def by simp

lemma strong_setL2_cong:
"⟦A = B; ⋀x. x ∈ B =simp=> f x = g x⟧ ⟹ setL2 f A = setL2 g B"
unfolding setL2_def simp_implies_def by simp

lemma setL2_infinite [simp]: "¬ finite A ⟹ setL2 f A = 0"
unfolding setL2_def by simp

lemma setL2_empty [simp]: "setL2 f {} = 0"
unfolding setL2_def by simp

lemma setL2_insert [simp]:
"⟦finite F; a ∉ F⟧ ⟹
setL2 f (insert a F) = sqrt ((f a)⇧2 + (setL2 f F)⇧2)"
unfolding setL2_def by (simp add: setsum_nonneg)

lemma setL2_nonneg [simp]: "0 ≤ setL2 f A"
unfolding setL2_def by (simp add: setsum_nonneg)

lemma setL2_0': "∀a∈A. f a = 0 ⟹ setL2 f A = 0"
unfolding setL2_def by simp

lemma setL2_constant: "setL2 (λx. y) A = sqrt (of_nat (card A)) * ¦y¦"
unfolding setL2_def by (simp add: real_sqrt_mult)

lemma setL2_mono:
assumes "⋀i. i ∈ K ⟹ f i ≤ g i"
assumes "⋀i. i ∈ K ⟹ 0 ≤ f i"
shows "setL2 f K ≤ setL2 g K"
unfolding setL2_def
by (simp add: setsum_nonneg setsum_mono power_mono assms)

lemma setL2_strict_mono:
assumes "finite K" and "K ≠ {}"
assumes "⋀i. i ∈ K ⟹ f i < g i"
assumes "⋀i. i ∈ K ⟹ 0 ≤ f i"
shows "setL2 f K < setL2 g K"
unfolding setL2_def
by (simp add: setsum_strict_mono power_strict_mono assms)

lemma setL2_right_distrib:
"0 ≤ r ⟹ r * setL2 f A = setL2 (λx. r * f x) A"
unfolding setL2_def
done

lemma setL2_left_distrib:
"0 ≤ r ⟹ setL2 f A * r = setL2 (λx. f x * r) A"
unfolding setL2_def
done

lemma setL2_eq_0_iff: "finite A ⟹ setL2 f A = 0 ⟷ (∀x∈A. f x = 0)"
unfolding setL2_def

lemma setL2_triangle_ineq:
shows "setL2 (λi. f i + g i) A ≤ setL2 f A + setL2 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 + (setL2 (λi. f i + g i) F)⇧2) ≤
sqrt ((f x + g x)⇧2 + (setL2 f F + setL2 g F)⇧2)"
by (intro real_sqrt_le_mono add_left_mono power_mono insert
also have
"… ≤ sqrt ((f x)⇧2 + (setL2 f F)⇧2) + sqrt ((g x)⇧2 + (setL2 g F)⇧2)"
by (rule real_sqrt_sum_squares_triangle_ineq)
finally show ?case
using insert by simp
qed
qed

lemma sqrt_sum_squares_le_sum:
"⟦0 ≤ x; 0 ≤ y⟧ ⟹ sqrt (x⇧2 + y⇧2) ≤ x + y"
apply (rule power2_le_imp_le)
apply simp
done

lemma setL2_le_setsum [rule_format]:
"(∀i∈A. 0 ≤ f i) ⟶ setL2 f A ≤ setsum 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 sqrt_sum_squares_le_sum_abs: "sqrt (x⇧2 + y⇧2) ≤ ¦x¦ + ¦y¦"
apply (rule power2_le_imp_le)
apply simp
done

lemma setL2_le_setsum_abs: "setL2 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 setL2_mult_ineq_lemma:
fixes a b c d :: real
shows "2 * (a * c) * (b * d) ≤ a⇧2 * d⇧2 + b⇧2 * c⇧2"
proof -
have "0 ≤ (a * d - b * c)⇧2" by simp
also have "… = a⇧2 * d⇧2 + b⇧2 * c⇧2 - 2 * (a * d) * (b * c)"
by (simp only: power2_diff power_mult_distrib)
also have "… = a⇧2 * d⇧2 + b⇧2 * c⇧2 - 2 * (a * c) * (b * d)"
by simp
finally show "2 * (a * c) * (b * d) ≤ a⇧2 * d⇧2 + b⇧2 * c⇧2"
by simp
qed

lemma setL2_mult_ineq: "(∑i∈A. ¦f i¦ * ¦g i¦) ≤ setL2 f A * setL2 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)
apply (rule ord_le_eq_trans)
apply (rule setL2_mult_ineq_lemma)
apply simp_all
done

lemma member_le_setL2: "⟦finite A; i ∈ A⟧ ⟹ f i ≤ setL2 f A"
apply (rule_tac s="insert i (A - {i})" and t="A" in subst)
apply fast
apply (subst setL2_insert)
apply simp
apply simp
apply simp
done

end
```