src/HOL/Analysis/L2_Norm.thy
author nipkow
Sat Dec 29 15:43:53 2018 +0100 (6 months ago)
changeset 69529 4ab9657b3257
parent 69164 74f1b0f10b2b
child 69546 27dae626822b
permissions -rw-r--r--
capitalize proper names in lemma names
hoelzl@63627
     1
(*  Title:      HOL/Analysis/L2_Norm.thy
huffman@36333
     2
    Author:     Brian Huffman, Portland State University
huffman@36333
     3
*)
huffman@36333
     4
nipkow@67143
     5
section \<open>L2 Norm\<close>
huffman@36333
     6
huffman@36333
     7
theory L2_Norm
wenzelm@67006
     8
imports Complex_Main
huffman@36333
     9
begin
huffman@36333
    10
nipkow@67156
    11
definition %important "L2_set f A = sqrt (\<Sum>i\<in>A. (f i)\<^sup>2)"
huffman@36333
    12
nipkow@67155
    13
lemma L2_set_cong:
nipkow@67155
    14
  "\<lbrakk>A = B; \<And>x. x \<in> B \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> L2_set f A = L2_set g B"
nipkow@67155
    15
  unfolding L2_set_def by simp
huffman@36333
    16
nipkow@69164
    17
lemma L2_set_cong_strong:
nipkow@67155
    18
  "\<lbrakk>A = B; \<And>x. x \<in> B =simp=> f x = g x\<rbrakk> \<Longrightarrow> L2_set f A = L2_set g B"
nipkow@67155
    19
  unfolding L2_set_def simp_implies_def by simp
huffman@36333
    20
nipkow@67155
    21
lemma L2_set_infinite [simp]: "\<not> finite A \<Longrightarrow> L2_set f A = 0"
nipkow@67155
    22
  unfolding L2_set_def by simp
nipkow@67155
    23
nipkow@67155
    24
lemma L2_set_empty [simp]: "L2_set f {} = 0"
nipkow@67155
    25
  unfolding L2_set_def by simp
huffman@36333
    26
nipkow@67155
    27
lemma L2_set_insert [simp]:
nipkow@67155
    28
  "\<lbrakk>finite F; a \<notin> F\<rbrakk> \<Longrightarrow>
nipkow@67155
    29
    L2_set f (insert a F) = sqrt ((f a)\<^sup>2 + (L2_set f F)\<^sup>2)"
nipkow@67155
    30
  unfolding L2_set_def by (simp add: sum_nonneg)
huffman@36333
    31
nipkow@67155
    32
lemma L2_set_nonneg [simp]: "0 \<le> L2_set f A"
nipkow@67155
    33
  unfolding L2_set_def by (simp add: sum_nonneg)
huffman@36333
    34
nipkow@67155
    35
lemma L2_set_0': "\<forall>a\<in>A. f a = 0 \<Longrightarrow> L2_set f A = 0"
nipkow@67155
    36
  unfolding L2_set_def by simp
huffman@36333
    37
nipkow@67155
    38
lemma L2_set_constant: "L2_set (\<lambda>x. y) A = sqrt (of_nat (card A)) * \<bar>y\<bar>"
nipkow@67155
    39
  unfolding L2_set_def by (simp add: real_sqrt_mult)
huffman@36333
    40
nipkow@67155
    41
lemma L2_set_mono:
huffman@36333
    42
  assumes "\<And>i. i \<in> K \<Longrightarrow> f i \<le> g i"
huffman@36333
    43
  assumes "\<And>i. i \<in> K \<Longrightarrow> 0 \<le> f i"
nipkow@67155
    44
  shows "L2_set f K \<le> L2_set g K"
nipkow@67155
    45
  unfolding L2_set_def
nipkow@64267
    46
  by (simp add: sum_nonneg sum_mono power_mono assms)
huffman@36333
    47
nipkow@67155
    48
lemma L2_set_strict_mono:
huffman@36333
    49
  assumes "finite K" and "K \<noteq> {}"
huffman@36333
    50
  assumes "\<And>i. i \<in> K \<Longrightarrow> f i < g i"
huffman@36333
    51
  assumes "\<And>i. i \<in> K \<Longrightarrow> 0 \<le> f i"
nipkow@67155
    52
  shows "L2_set f K < L2_set g K"
nipkow@67155
    53
  unfolding L2_set_def
nipkow@64267
    54
  by (simp add: sum_strict_mono power_strict_mono assms)
huffman@36333
    55
nipkow@67155
    56
lemma L2_set_right_distrib:
nipkow@67155
    57
  "0 \<le> r \<Longrightarrow> r * L2_set f A = L2_set (\<lambda>x. r * f x) A"
nipkow@67155
    58
  unfolding L2_set_def
huffman@36333
    59
  apply (simp add: power_mult_distrib)
nipkow@64267
    60
  apply (simp add: sum_distrib_left [symmetric])
nipkow@64267
    61
  apply (simp add: real_sqrt_mult sum_nonneg)
huffman@36333
    62
  done
huffman@36333
    63
nipkow@67155
    64
lemma L2_set_left_distrib:
nipkow@67155
    65
  "0 \<le> r \<Longrightarrow> L2_set f A * r = L2_set (\<lambda>x. f x * r) A"
nipkow@67155
    66
  unfolding L2_set_def
huffman@36333
    67
  apply (simp add: power_mult_distrib)
nipkow@64267
    68
  apply (simp add: sum_distrib_right [symmetric])
nipkow@64267
    69
  apply (simp add: real_sqrt_mult sum_nonneg)
huffman@36333
    70
  done
huffman@36333
    71
nipkow@67155
    72
lemma L2_set_eq_0_iff: "finite A \<Longrightarrow> L2_set f A = 0 \<longleftrightarrow> (\<forall>x\<in>A. f x = 0)"
nipkow@67155
    73
  unfolding L2_set_def
nipkow@64267
    74
  by (simp add: sum_nonneg sum_nonneg_eq_0_iff)
huffman@36333
    75
immler@68607
    76
proposition L2_set_triangle_ineq:
nipkow@67156
    77
  "L2_set (\<lambda>i. f i + g i) A \<le> L2_set f A + L2_set g A"
immler@68607
    78
proof (cases "finite A")
huffman@36333
    79
  case False
huffman@36333
    80
  thus ?thesis by simp
huffman@36333
    81
next
huffman@36333
    82
  case True
huffman@36333
    83
  thus ?thesis
huffman@36333
    84
  proof (induct set: finite)
huffman@36333
    85
    case empty
huffman@36333
    86
    show ?case by simp
huffman@36333
    87
  next
huffman@36333
    88
    case (insert x F)
nipkow@67155
    89
    hence "sqrt ((f x + g x)\<^sup>2 + (L2_set (\<lambda>i. f i + g i) F)\<^sup>2) \<le>
nipkow@67155
    90
           sqrt ((f x + g x)\<^sup>2 + (L2_set f F + L2_set g F)\<^sup>2)"
huffman@36333
    91
      by (intro real_sqrt_le_mono add_left_mono power_mono insert
nipkow@67155
    92
                L2_set_nonneg add_increasing zero_le_power2)
huffman@36333
    93
    also have
nipkow@67155
    94
      "\<dots> \<le> sqrt ((f x)\<^sup>2 + (L2_set f F)\<^sup>2) + sqrt ((g x)\<^sup>2 + (L2_set g F)\<^sup>2)"
huffman@36333
    95
      by (rule real_sqrt_sum_squares_triangle_ineq)
huffman@36333
    96
    finally show ?case
huffman@36333
    97
      using insert by simp
huffman@36333
    98
  qed
huffman@36333
    99
qed
huffman@36333
   100
nipkow@67155
   101
lemma L2_set_le_sum [rule_format]:
nipkow@67155
   102
  "(\<forall>i\<in>A. 0 \<le> f i) \<longrightarrow> L2_set f A \<le> sum f A"
huffman@36333
   103
  apply (cases "finite A")
huffman@36333
   104
  apply (induct set: finite)
huffman@36333
   105
  apply simp
huffman@36333
   106
  apply clarsimp
huffman@36333
   107
  apply (erule order_trans [OF sqrt_sum_squares_le_sum])
huffman@36333
   108
  apply simp
huffman@36333
   109
  apply simp
huffman@36333
   110
  apply simp
huffman@36333
   111
  done
huffman@36333
   112
nipkow@67155
   113
lemma L2_set_le_sum_abs: "L2_set f A \<le> (\<Sum>i\<in>A. \<bar>f i\<bar>)"
huffman@36333
   114
  apply (cases "finite A")
huffman@36333
   115
  apply (induct set: finite)
huffman@36333
   116
  apply simp
huffman@36333
   117
  apply simp
huffman@36333
   118
  apply (rule order_trans [OF sqrt_sum_squares_le_sum_abs])
huffman@36333
   119
  apply simp
huffman@36333
   120
  apply simp
huffman@36333
   121
  done
huffman@36333
   122
nipkow@67155
   123
lemma L2_set_mult_ineq: "(\<Sum>i\<in>A. \<bar>f i\<bar> * \<bar>g i\<bar>) \<le> L2_set f A * L2_set g A"
huffman@36333
   124
  apply (cases "finite A")
huffman@36333
   125
  apply (induct set: finite)
huffman@36333
   126
  apply simp
huffman@36333
   127
  apply (rule power2_le_imp_le, simp)
huffman@36333
   128
  apply (rule order_trans)
huffman@36333
   129
  apply (rule power_mono)
huffman@36333
   130
  apply (erule add_left_mono)
nipkow@64267
   131
  apply (simp add: sum_nonneg)
huffman@36333
   132
  apply (simp add: power2_sum)
huffman@36333
   133
  apply (simp add: power_mult_distrib)
webertj@49962
   134
  apply (simp add: distrib_left distrib_right)
huffman@36333
   135
  apply (rule ord_le_eq_trans)
nipkow@67155
   136
  apply (rule L2_set_mult_ineq_lemma)
nipkow@56536
   137
  apply simp_all
huffman@36333
   138
  done
huffman@36333
   139
nipkow@67155
   140
lemma member_le_L2_set: "\<lbrakk>finite A; i \<in> A\<rbrakk> \<Longrightarrow> f i \<le> L2_set f A"
nipkow@67155
   141
  unfolding L2_set_def
nipkow@64267
   142
  by (auto intro!: member_le_sum real_le_rsqrt)
huffman@36333
   143
huffman@36333
   144
end