Theory L2_Norm

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

header {* 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
  apply (simp add: power_mult_distrib)
  apply (simp add: setsum_right_distrib [symmetric])
  apply (simp add: real_sqrt_mult setsum_nonneg)
  done

lemma setL2_left_distrib:
  "0 ≤ r ==> setL2 f A * r = setL2 (λx. f x * r) A"
  unfolding setL2_def
  apply (simp add: power_mult_distrib)
  apply (simp add: setsum_left_distrib [symmetric])
  apply (simp add: real_sqrt_mult setsum_nonneg)
  done

lemma setsum_nonneg_eq_0_iff:
  fixes f :: "'a => 'b::ordered_ab_group_add"
  shows "[|finite A; ∀x∈A. 0 ≤ f x|] ==> setsum f A = 0 <-> (∀x∈A. f x = 0)"
  apply (induct set: finite, simp)
  apply (simp add: add_nonneg_eq_0_iff setsum_nonneg)
  done

lemma setL2_eq_0_iff: "finite A ==> setL2 f A = 0 <-> (∀x∈A. f x = 0)"
  unfolding setL2_def
  by (simp add: setsum_nonneg setsum_nonneg_eq_0_iff)

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
                setL2_nonneg add_increasing zero_le_power2)
    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 (x2 + y2) ≤ x + y"
  apply (rule power2_le_imp_le)
  apply (simp add: power2_sum)
  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 (x2 + y2) ≤ ¦x¦ + ¦y¦"
  apply (rule power2_le_imp_le)
  apply (simp add: power2_sum)
  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) ≤ a2 * d2 + b2 * c2"
proof -
  have "0 ≤ (a * d - b * c)2" by simp
  also have "… = a2 * d2 + b2 * c2 - 2 * (a * d) * (b * c)"
    by (simp only: power2_diff power_mult_distrib)
  also have "… = a2 * d2 + b2 * c2 - 2 * (a * c) * (b * d)"
    by simp
  finally show "2 * (a * c) * (b * d) ≤ a2 * d2 + b2 * c2"
    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 (erule add_left_mono)
  apply (simp add: setsum_nonneg)
  apply (simp add: power2_sum)
  apply (simp add: power_mult_distrib)
  apply (simp add: distrib_left distrib_right)
  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