src/HOL/Analysis/L2_Norm.thy
author wenzelm
Sat Nov 04 19:17:19 2017 +0100 (20 months ago)
changeset 67006 b1278ed3cd46
parent 66453 cc19f7ca2ed6
child 67143 db609ac2c307
permissions -rw-r--r--
prefer main entry points of HOL;
hoelzl@63627
     1
(*  Title:      HOL/Analysis/L2_Norm.thy
huffman@36333
     2
    Author:     Brian Huffman, Portland State University
huffman@36333
     3
*)
huffman@36333
     4
wenzelm@60420
     5
section \<open>Square root of sum of squares\<close>
huffman@36333
     6
huffman@36333
     7
theory L2_Norm
wenzelm@67006
     8
imports Complex_Main
huffman@36333
     9
begin
huffman@36333
    10
huffman@36333
    11
definition
wenzelm@53015
    12
  "setL2 f A = sqrt (\<Sum>i\<in>A. (f i)\<^sup>2)"
huffman@36333
    13
huffman@36333
    14
lemma setL2_cong:
huffman@36333
    15
  "\<lbrakk>A = B; \<And>x. x \<in> B \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> setL2 f A = setL2 g B"
huffman@36333
    16
  unfolding setL2_def by simp
huffman@36333
    17
huffman@36333
    18
lemma strong_setL2_cong:
huffman@36333
    19
  "\<lbrakk>A = B; \<And>x. x \<in> B =simp=> f x = g x\<rbrakk> \<Longrightarrow> setL2 f A = setL2 g B"
huffman@36333
    20
  unfolding setL2_def simp_implies_def by simp
huffman@36333
    21
huffman@36333
    22
lemma setL2_infinite [simp]: "\<not> finite A \<Longrightarrow> setL2 f A = 0"
huffman@36333
    23
  unfolding setL2_def by simp
huffman@36333
    24
huffman@36333
    25
lemma setL2_empty [simp]: "setL2 f {} = 0"
huffman@36333
    26
  unfolding setL2_def by simp
huffman@36333
    27
huffman@36333
    28
lemma setL2_insert [simp]:
huffman@36333
    29
  "\<lbrakk>finite F; a \<notin> F\<rbrakk> \<Longrightarrow>
wenzelm@53015
    30
    setL2 f (insert a F) = sqrt ((f a)\<^sup>2 + (setL2 f F)\<^sup>2)"
nipkow@64267
    31
  unfolding setL2_def by (simp add: sum_nonneg)
huffman@36333
    32
huffman@36333
    33
lemma setL2_nonneg [simp]: "0 \<le> setL2 f A"
nipkow@64267
    34
  unfolding setL2_def by (simp add: sum_nonneg)
huffman@36333
    35
huffman@36333
    36
lemma setL2_0': "\<forall>a\<in>A. f a = 0 \<Longrightarrow> setL2 f A = 0"
huffman@36333
    37
  unfolding setL2_def by simp
huffman@36333
    38
huffman@36333
    39
lemma setL2_constant: "setL2 (\<lambda>x. y) A = sqrt (of_nat (card A)) * \<bar>y\<bar>"
huffman@36333
    40
  unfolding setL2_def by (simp add: real_sqrt_mult)
huffman@36333
    41
huffman@36333
    42
lemma setL2_mono:
huffman@36333
    43
  assumes "\<And>i. i \<in> K \<Longrightarrow> f i \<le> g i"
huffman@36333
    44
  assumes "\<And>i. i \<in> K \<Longrightarrow> 0 \<le> f i"
huffman@36333
    45
  shows "setL2 f K \<le> setL2 g K"
huffman@36333
    46
  unfolding setL2_def
nipkow@64267
    47
  by (simp add: sum_nonneg sum_mono power_mono assms)
huffman@36333
    48
huffman@36333
    49
lemma setL2_strict_mono:
huffman@36333
    50
  assumes "finite K" and "K \<noteq> {}"
huffman@36333
    51
  assumes "\<And>i. i \<in> K \<Longrightarrow> f i < g i"
huffman@36333
    52
  assumes "\<And>i. i \<in> K \<Longrightarrow> 0 \<le> f i"
huffman@36333
    53
  shows "setL2 f K < setL2 g K"
huffman@36333
    54
  unfolding setL2_def
nipkow@64267
    55
  by (simp add: sum_strict_mono power_strict_mono assms)
huffman@36333
    56
huffman@36333
    57
lemma setL2_right_distrib:
huffman@36333
    58
  "0 \<le> r \<Longrightarrow> r * setL2 f A = setL2 (\<lambda>x. r * f x) A"
huffman@36333
    59
  unfolding setL2_def
huffman@36333
    60
  apply (simp add: power_mult_distrib)
nipkow@64267
    61
  apply (simp add: sum_distrib_left [symmetric])
nipkow@64267
    62
  apply (simp add: real_sqrt_mult sum_nonneg)
huffman@36333
    63
  done
huffman@36333
    64
huffman@36333
    65
lemma setL2_left_distrib:
huffman@36333
    66
  "0 \<le> r \<Longrightarrow> setL2 f A * r = setL2 (\<lambda>x. f x * r) A"
huffman@36333
    67
  unfolding setL2_def
huffman@36333
    68
  apply (simp add: power_mult_distrib)
nipkow@64267
    69
  apply (simp add: sum_distrib_right [symmetric])
nipkow@64267
    70
  apply (simp add: real_sqrt_mult sum_nonneg)
huffman@36333
    71
  done
huffman@36333
    72
huffman@36333
    73
lemma setL2_eq_0_iff: "finite A \<Longrightarrow> setL2 f A = 0 \<longleftrightarrow> (\<forall>x\<in>A. f x = 0)"
huffman@36333
    74
  unfolding setL2_def
nipkow@64267
    75
  by (simp add: sum_nonneg sum_nonneg_eq_0_iff)
huffman@36333
    76
huffman@36333
    77
lemma setL2_triangle_ineq:
huffman@36333
    78
  shows "setL2 (\<lambda>i. f i + g i) A \<le> setL2 f A + setL2 g A"
huffman@36333
    79
proof (cases "finite A")
huffman@36333
    80
  case False
huffman@36333
    81
  thus ?thesis by simp
huffman@36333
    82
next
huffman@36333
    83
  case True
huffman@36333
    84
  thus ?thesis
huffman@36333
    85
  proof (induct set: finite)
huffman@36333
    86
    case empty
huffman@36333
    87
    show ?case by simp
huffman@36333
    88
  next
huffman@36333
    89
    case (insert x F)
wenzelm@53015
    90
    hence "sqrt ((f x + g x)\<^sup>2 + (setL2 (\<lambda>i. f i + g i) F)\<^sup>2) \<le>
wenzelm@53015
    91
           sqrt ((f x + g x)\<^sup>2 + (setL2 f F + setL2 g F)\<^sup>2)"
huffman@36333
    92
      by (intro real_sqrt_le_mono add_left_mono power_mono insert
huffman@36333
    93
                setL2_nonneg add_increasing zero_le_power2)
huffman@36333
    94
    also have
wenzelm@53015
    95
      "\<dots> \<le> sqrt ((f x)\<^sup>2 + (setL2 f F)\<^sup>2) + sqrt ((g x)\<^sup>2 + (setL2 g F)\<^sup>2)"
huffman@36333
    96
      by (rule real_sqrt_sum_squares_triangle_ineq)
huffman@36333
    97
    finally show ?case
huffman@36333
    98
      using insert by simp
huffman@36333
    99
  qed
huffman@36333
   100
qed
huffman@36333
   101
huffman@36333
   102
lemma sqrt_sum_squares_le_sum:
wenzelm@53015
   103
  "\<lbrakk>0 \<le> x; 0 \<le> y\<rbrakk> \<Longrightarrow> sqrt (x\<^sup>2 + y\<^sup>2) \<le> x + y"
huffman@36333
   104
  apply (rule power2_le_imp_le)
nipkow@56536
   105
  apply (simp add: power2_sum)
huffman@44142
   106
  apply simp
huffman@36333
   107
  done
huffman@36333
   108
nipkow@64267
   109
lemma setL2_le_sum [rule_format]:
nipkow@64267
   110
  "(\<forall>i\<in>A. 0 \<le> f i) \<longrightarrow> setL2 f A \<le> sum f A"
huffman@36333
   111
  apply (cases "finite A")
huffman@36333
   112
  apply (induct set: finite)
huffman@36333
   113
  apply simp
huffman@36333
   114
  apply clarsimp
huffman@36333
   115
  apply (erule order_trans [OF sqrt_sum_squares_le_sum])
huffman@36333
   116
  apply simp
huffman@36333
   117
  apply simp
huffman@36333
   118
  apply simp
huffman@36333
   119
  done
huffman@36333
   120
wenzelm@53015
   121
lemma sqrt_sum_squares_le_sum_abs: "sqrt (x\<^sup>2 + y\<^sup>2) \<le> \<bar>x\<bar> + \<bar>y\<bar>"
huffman@36333
   122
  apply (rule power2_le_imp_le)
nipkow@56536
   123
  apply (simp add: power2_sum)
huffman@44142
   124
  apply simp
huffman@36333
   125
  done
huffman@36333
   126
nipkow@64267
   127
lemma setL2_le_sum_abs: "setL2 f A \<le> (\<Sum>i\<in>A. \<bar>f i\<bar>)"
huffman@36333
   128
  apply (cases "finite A")
huffman@36333
   129
  apply (induct set: finite)
huffman@36333
   130
  apply simp
huffman@36333
   131
  apply simp
huffman@36333
   132
  apply (rule order_trans [OF sqrt_sum_squares_le_sum_abs])
huffman@36333
   133
  apply simp
huffman@36333
   134
  apply simp
huffman@36333
   135
  done
huffman@36333
   136
huffman@36333
   137
lemma setL2_mult_ineq_lemma:
huffman@36333
   138
  fixes a b c d :: real
wenzelm@53015
   139
  shows "2 * (a * c) * (b * d) \<le> a\<^sup>2 * d\<^sup>2 + b\<^sup>2 * c\<^sup>2"
huffman@36333
   140
proof -
wenzelm@53015
   141
  have "0 \<le> (a * d - b * c)\<^sup>2" by simp
wenzelm@53015
   142
  also have "\<dots> = a\<^sup>2 * d\<^sup>2 + b\<^sup>2 * c\<^sup>2 - 2 * (a * d) * (b * c)"
huffman@36333
   143
    by (simp only: power2_diff power_mult_distrib)
wenzelm@53015
   144
  also have "\<dots> = a\<^sup>2 * d\<^sup>2 + b\<^sup>2 * c\<^sup>2 - 2 * (a * c) * (b * d)"
huffman@36333
   145
    by simp
wenzelm@53015
   146
  finally show "2 * (a * c) * (b * d) \<le> a\<^sup>2 * d\<^sup>2 + b\<^sup>2 * c\<^sup>2"
huffman@36333
   147
    by simp
huffman@36333
   148
qed
huffman@36333
   149
huffman@36333
   150
lemma setL2_mult_ineq: "(\<Sum>i\<in>A. \<bar>f i\<bar> * \<bar>g i\<bar>) \<le> setL2 f A * setL2 g A"
huffman@36333
   151
  apply (cases "finite A")
huffman@36333
   152
  apply (induct set: finite)
huffman@36333
   153
  apply simp
huffman@36333
   154
  apply (rule power2_le_imp_le, simp)
huffman@36333
   155
  apply (rule order_trans)
huffman@36333
   156
  apply (rule power_mono)
huffman@36333
   157
  apply (erule add_left_mono)
nipkow@64267
   158
  apply (simp add: sum_nonneg)
huffman@36333
   159
  apply (simp add: power2_sum)
huffman@36333
   160
  apply (simp add: power_mult_distrib)
webertj@49962
   161
  apply (simp add: distrib_left distrib_right)
huffman@36333
   162
  apply (rule ord_le_eq_trans)
huffman@36333
   163
  apply (rule setL2_mult_ineq_lemma)
nipkow@56536
   164
  apply simp_all
huffman@36333
   165
  done
huffman@36333
   166
huffman@36333
   167
lemma member_le_setL2: "\<lbrakk>finite A; i \<in> A\<rbrakk> \<Longrightarrow> f i \<le> setL2 f A"
lp15@63938
   168
  unfolding setL2_def
nipkow@64267
   169
  by (auto intro!: member_le_sum real_le_rsqrt)
huffman@36333
   170
huffman@36333
   171
end