Theory HOL-Analysis.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›

definitiontag important› L2_set :: "('a  real)  'a set  real" where
"L2_set f A = sqrt (iA. (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': "aA. 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
  apply (simp add: power_mult_distrib)
  apply (simp add: sum_distrib_left [symmetric])
  apply (simp add: real_sqrt_mult sum_nonneg)
  done

lemma L2_set_left_distrib:
  "0  r  L2_set f A * r = L2_set (λx. f x * r) A"
  unfolding L2_set_def
  apply (simp add: power_mult_distrib)
  apply (simp add: sum_distrib_right [symmetric])
  apply (simp add: real_sqrt_mult sum_nonneg)
  done

lemma L2_set_eq_0_iff: "finite A  L2_set f A = 0  (xA. 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)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
                L2_set_nonneg add_increasing zero_le_power2)
    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]:
  "(iA. 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  (iA. ¦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: "(iA. ¦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)
  apply (erule add_left_mono)
  apply (simp add: sum_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 L2_set_mult_ineq_lemma)
  apply simp_all
  done

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