Quelle L2_Norm.thy Sprache: Isabelle

(*  Title:      HOL/Analysis/L2_Norm.thy
    Author:     Brian Huffman, Portland State University
*)

chapter \<open>Linear Algebra\<close>

theory L2_Norm
imports Complex_Main
begin

section \<open>L2 Norm\<close>

definition\<^marker>\<open>tag important\<close> L2_set :: "('a \<Rightarrow> real) \<Rightarrow> 'a set \<Rightarrow> real" where
"L2_set f A = sqrt (\i\A. (f i)\<^sup>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)\<^sup>2 + (L2_set f F)\<^sup>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)\<^sup>2 + (L2_set (\i. f i + g i) F)\<^sup>2) \
           sqrt ((f x + g x)\<^sup>2 + (L2_set f F + L2_set g F)\<^sup>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)\<^sup>2 + (L2_set f F)\<^sup>2) + sqrt ((g x)\<^sup>2 + (L2_set g F)\<^sup>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\))\<^sup>2
      \<le> (\<bar>f a\<bar> * \<bar>g a\<bar> + L2_set f A * L2_set g A)\<^sup>2"
    by (simp add: insert.IH sum_nonneg)
  also have "... \ ((f a)\<^sup>2 + (L2_set f A)\<^sup>2) * ((g a)\<^sup>2 + (L2_set g A)\<^sup>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)\<^sup>2 + (L2_set f A)\<^sup>2) * sqrt ((g a)\<^sup>2 + (L2_set g A)\<^sup>2))\<^sup>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\))\<^sup>2
              \<le> (sqrt ((f a)\<^sup>2 + (L2_set f A)\<^sup>2) * sqrt ((g a)\<^sup>2 + (L2_set g A)\<^sup>2))\<^sup>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

quality100%

¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.