Quelle  L2_Norm.thy

(*  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
  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)🪙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:
  "(∧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∣))🪙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)🪙2 + (L2_set f A)🪙2) * ((g a)🪙2 + (L2_set g A)🪙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)🪙2 + (L2_set f A)🪙2) * sqrt ((g a)🪙2 + (L2_set g A)🪙2))🪙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∣))🪙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