src/HOL/Library/Inner_Product.thy
author huffman
Thu Jun 04 16:11:36 2009 -0700 (2009-06-04)
changeset 31446 2d91b2416de8
parent 31417 c12b25b7f015
child 31492 5400beeddb55
permissions -rw-r--r--
add extra type constraints for dist, norm
huffman@29993
     1
(* Title:      Inner_Product.thy
huffman@29993
     2
   Author:     Brian Huffman
huffman@29993
     3
*)
huffman@29993
     4
huffman@29993
     5
header {* Inner Product Spaces and the Gradient Derivative *}
huffman@29993
     6
huffman@29993
     7
theory Inner_Product
haftmann@30663
     8
imports Complex_Main FrechetDeriv
huffman@29993
     9
begin
huffman@29993
    10
huffman@29993
    11
subsection {* Real inner product spaces *}
huffman@29993
    12
huffman@31446
    13
text {* Temporarily relax constraints for @{term dist} and @{term norm}. *}
huffman@31446
    14
huffman@31446
    15
setup {* Sign.add_const_constraint
huffman@31446
    16
  (@{const_name dist}, SOME @{typ "'a::dist \<Rightarrow> 'a \<Rightarrow> real"}) *}
huffman@31446
    17
huffman@31446
    18
setup {* Sign.add_const_constraint
huffman@31446
    19
  (@{const_name norm}, SOME @{typ "'a::norm \<Rightarrow> real"}) *}
huffman@31446
    20
huffman@31417
    21
class real_inner = real_vector + sgn_div_norm + dist_norm + topo_dist +
huffman@29993
    22
  fixes inner :: "'a \<Rightarrow> 'a \<Rightarrow> real"
huffman@29993
    23
  assumes inner_commute: "inner x y = inner y x"
huffman@29993
    24
  and inner_left_distrib: "inner (x + y) z = inner x z + inner y z"
huffman@29993
    25
  and inner_scaleR_left: "inner (scaleR r x) y = r * (inner x y)"
huffman@29993
    26
  and inner_ge_zero [simp]: "0 \<le> inner x x"
huffman@29993
    27
  and inner_eq_zero_iff [simp]: "inner x x = 0 \<longleftrightarrow> x = 0"
huffman@29993
    28
  and norm_eq_sqrt_inner: "norm x = sqrt (inner x x)"
huffman@29993
    29
begin
huffman@29993
    30
huffman@29993
    31
lemma inner_zero_left [simp]: "inner 0 x = 0"
huffman@30067
    32
  using inner_left_distrib [of 0 0 x] by simp
huffman@29993
    33
huffman@29993
    34
lemma inner_minus_left [simp]: "inner (- x) y = - inner x y"
huffman@30067
    35
  using inner_left_distrib [of x "- x" y] by simp
huffman@29993
    36
huffman@29993
    37
lemma inner_diff_left: "inner (x - y) z = inner x z - inner y z"
huffman@29993
    38
  by (simp add: diff_minus inner_left_distrib)
huffman@29993
    39
huffman@29993
    40
text {* Transfer distributivity rules to right argument. *}
huffman@29993
    41
huffman@29993
    42
lemma inner_right_distrib: "inner x (y + z) = inner x y + inner x z"
huffman@29993
    43
  using inner_left_distrib [of y z x] by (simp only: inner_commute)
huffman@29993
    44
huffman@29993
    45
lemma inner_scaleR_right: "inner x (scaleR r y) = r * (inner x y)"
huffman@29993
    46
  using inner_scaleR_left [of r y x] by (simp only: inner_commute)
huffman@29993
    47
huffman@29993
    48
lemma inner_zero_right [simp]: "inner x 0 = 0"
huffman@29993
    49
  using inner_zero_left [of x] by (simp only: inner_commute)
huffman@29993
    50
huffman@29993
    51
lemma inner_minus_right [simp]: "inner x (- y) = - inner x y"
huffman@29993
    52
  using inner_minus_left [of y x] by (simp only: inner_commute)
huffman@29993
    53
huffman@29993
    54
lemma inner_diff_right: "inner x (y - z) = inner x y - inner x z"
huffman@29993
    55
  using inner_diff_left [of y z x] by (simp only: inner_commute)
huffman@29993
    56
huffman@29993
    57
lemmas inner_distrib = inner_left_distrib inner_right_distrib
huffman@29993
    58
lemmas inner_diff = inner_diff_left inner_diff_right
huffman@29993
    59
lemmas inner_scaleR = inner_scaleR_left inner_scaleR_right
huffman@29993
    60
huffman@29993
    61
lemma inner_gt_zero_iff [simp]: "0 < inner x x \<longleftrightarrow> x \<noteq> 0"
huffman@29993
    62
  by (simp add: order_less_le)
huffman@29993
    63
huffman@29993
    64
lemma power2_norm_eq_inner: "(norm x)\<twosuperior> = inner x x"
huffman@29993
    65
  by (simp add: norm_eq_sqrt_inner)
huffman@29993
    66
huffman@30046
    67
lemma Cauchy_Schwarz_ineq:
huffman@29993
    68
  "(inner x y)\<twosuperior> \<le> inner x x * inner y y"
huffman@29993
    69
proof (cases)
huffman@29993
    70
  assume "y = 0"
huffman@29993
    71
  thus ?thesis by simp
huffman@29993
    72
next
huffman@29993
    73
  assume y: "y \<noteq> 0"
huffman@29993
    74
  let ?r = "inner x y / inner y y"
huffman@29993
    75
  have "0 \<le> inner (x - scaleR ?r y) (x - scaleR ?r y)"
huffman@29993
    76
    by (rule inner_ge_zero)
huffman@29993
    77
  also have "\<dots> = inner x x - inner y x * ?r"
huffman@29993
    78
    by (simp add: inner_diff inner_scaleR)
huffman@29993
    79
  also have "\<dots> = inner x x - (inner x y)\<twosuperior> / inner y y"
huffman@29993
    80
    by (simp add: power2_eq_square inner_commute)
huffman@29993
    81
  finally have "0 \<le> inner x x - (inner x y)\<twosuperior> / inner y y" .
huffman@29993
    82
  hence "(inner x y)\<twosuperior> / inner y y \<le> inner x x"
huffman@29993
    83
    by (simp add: le_diff_eq)
huffman@29993
    84
  thus "(inner x y)\<twosuperior> \<le> inner x x * inner y y"
huffman@29993
    85
    by (simp add: pos_divide_le_eq y)
huffman@29993
    86
qed
huffman@29993
    87
huffman@30046
    88
lemma Cauchy_Schwarz_ineq2:
huffman@29993
    89
  "\<bar>inner x y\<bar> \<le> norm x * norm y"
huffman@29993
    90
proof (rule power2_le_imp_le)
huffman@29993
    91
  have "(inner x y)\<twosuperior> \<le> inner x x * inner y y"
huffman@30046
    92
    using Cauchy_Schwarz_ineq .
huffman@29993
    93
  thus "\<bar>inner x y\<bar>\<twosuperior> \<le> (norm x * norm y)\<twosuperior>"
huffman@29993
    94
    by (simp add: power_mult_distrib power2_norm_eq_inner)
huffman@29993
    95
  show "0 \<le> norm x * norm y"
huffman@29993
    96
    unfolding norm_eq_sqrt_inner
huffman@29993
    97
    by (intro mult_nonneg_nonneg real_sqrt_ge_zero inner_ge_zero)
huffman@29993
    98
qed
huffman@29993
    99
huffman@29993
   100
subclass real_normed_vector
huffman@29993
   101
proof
huffman@29993
   102
  fix a :: real and x y :: 'a
huffman@29993
   103
  show "0 \<le> norm x"
huffman@29993
   104
    unfolding norm_eq_sqrt_inner by simp
huffman@29993
   105
  show "norm x = 0 \<longleftrightarrow> x = 0"
huffman@29993
   106
    unfolding norm_eq_sqrt_inner by simp
huffman@29993
   107
  show "norm (x + y) \<le> norm x + norm y"
huffman@29993
   108
    proof (rule power2_le_imp_le)
huffman@29993
   109
      have "inner x y \<le> norm x * norm y"
huffman@30046
   110
        by (rule order_trans [OF abs_ge_self Cauchy_Schwarz_ineq2])
huffman@29993
   111
      thus "(norm (x + y))\<twosuperior> \<le> (norm x + norm y)\<twosuperior>"
huffman@29993
   112
        unfolding power2_sum power2_norm_eq_inner
huffman@29993
   113
        by (simp add: inner_distrib inner_commute)
huffman@29993
   114
      show "0 \<le> norm x + norm y"
huffman@29993
   115
        unfolding norm_eq_sqrt_inner
huffman@29993
   116
        by (simp add: add_nonneg_nonneg)
huffman@29993
   117
    qed
huffman@29993
   118
  have "sqrt (a\<twosuperior> * inner x x) = \<bar>a\<bar> * sqrt (inner x x)"
huffman@29993
   119
    by (simp add: real_sqrt_mult_distrib)
huffman@29993
   120
  then show "norm (a *\<^sub>R x) = \<bar>a\<bar> * norm x"
huffman@29993
   121
    unfolding norm_eq_sqrt_inner
huffman@29993
   122
    by (simp add: inner_scaleR power2_eq_square mult_assoc)
huffman@29993
   123
qed
huffman@29993
   124
huffman@29993
   125
end
huffman@29993
   126
huffman@31446
   127
text {* Re-enable constraints for @{term dist} and @{term norm}. *}
huffman@31446
   128
huffman@31446
   129
setup {* Sign.add_const_constraint
huffman@31446
   130
  (@{const_name dist}, SOME @{typ "'a::metric_space \<Rightarrow> 'a \<Rightarrow> real"}) *}
huffman@31446
   131
huffman@31446
   132
setup {* Sign.add_const_constraint
huffman@31446
   133
  (@{const_name norm}, SOME @{typ "'a::real_normed_vector \<Rightarrow> real"}) *}
huffman@31446
   134
wenzelm@30729
   135
interpretation inner:
huffman@29993
   136
  bounded_bilinear "inner::'a::real_inner \<Rightarrow> 'a \<Rightarrow> real"
huffman@29993
   137
proof
huffman@29993
   138
  fix x y z :: 'a and r :: real
huffman@29993
   139
  show "inner (x + y) z = inner x z + inner y z"
huffman@29993
   140
    by (rule inner_left_distrib)
huffman@29993
   141
  show "inner x (y + z) = inner x y + inner x z"
huffman@29993
   142
    by (rule inner_right_distrib)
huffman@29993
   143
  show "inner (scaleR r x) y = scaleR r (inner x y)"
huffman@29993
   144
    unfolding real_scaleR_def by (rule inner_scaleR_left)
huffman@29993
   145
  show "inner x (scaleR r y) = scaleR r (inner x y)"
huffman@29993
   146
    unfolding real_scaleR_def by (rule inner_scaleR_right)
huffman@29993
   147
  show "\<exists>K. \<forall>x y::'a. norm (inner x y) \<le> norm x * norm y * K"
huffman@29993
   148
  proof
huffman@29993
   149
    show "\<forall>x y::'a. norm (inner x y) \<le> norm x * norm y * 1"
huffman@30046
   150
      by (simp add: Cauchy_Schwarz_ineq2)
huffman@29993
   151
  qed
huffman@29993
   152
qed
huffman@29993
   153
wenzelm@30729
   154
interpretation inner_left:
huffman@29993
   155
  bounded_linear "\<lambda>x::'a::real_inner. inner x y"
huffman@29993
   156
  by (rule inner.bounded_linear_left)
huffman@29993
   157
wenzelm@30729
   158
interpretation inner_right:
huffman@29993
   159
  bounded_linear "\<lambda>y::'a::real_inner. inner x y"
huffman@29993
   160
  by (rule inner.bounded_linear_right)
huffman@29993
   161
huffman@29993
   162
huffman@29993
   163
subsection {* Class instances *}
huffman@29993
   164
huffman@29993
   165
instantiation real :: real_inner
huffman@29993
   166
begin
huffman@29993
   167
huffman@29993
   168
definition inner_real_def [simp]: "inner = op *"
huffman@29993
   169
huffman@29993
   170
instance proof
huffman@29993
   171
  fix x y z r :: real
huffman@29993
   172
  show "inner x y = inner y x"
huffman@29993
   173
    unfolding inner_real_def by (rule mult_commute)
huffman@29993
   174
  show "inner (x + y) z = inner x z + inner y z"
huffman@29993
   175
    unfolding inner_real_def by (rule left_distrib)
huffman@29993
   176
  show "inner (scaleR r x) y = r * inner x y"
huffman@29993
   177
    unfolding inner_real_def real_scaleR_def by (rule mult_assoc)
huffman@29993
   178
  show "0 \<le> inner x x"
huffman@29993
   179
    unfolding inner_real_def by simp
huffman@29993
   180
  show "inner x x = 0 \<longleftrightarrow> x = 0"
huffman@29993
   181
    unfolding inner_real_def by simp
huffman@29993
   182
  show "norm x = sqrt (inner x x)"
huffman@29993
   183
    unfolding inner_real_def by simp
huffman@29993
   184
qed
huffman@29993
   185
huffman@29993
   186
end
huffman@29993
   187
huffman@29993
   188
instantiation complex :: real_inner
huffman@29993
   189
begin
huffman@29993
   190
huffman@29993
   191
definition inner_complex_def:
huffman@29993
   192
  "inner x y = Re x * Re y + Im x * Im y"
huffman@29993
   193
huffman@29993
   194
instance proof
huffman@29993
   195
  fix x y z :: complex and r :: real
huffman@29993
   196
  show "inner x y = inner y x"
huffman@29993
   197
    unfolding inner_complex_def by (simp add: mult_commute)
huffman@29993
   198
  show "inner (x + y) z = inner x z + inner y z"
huffman@29993
   199
    unfolding inner_complex_def by (simp add: left_distrib)
huffman@29993
   200
  show "inner (scaleR r x) y = r * inner x y"
huffman@29993
   201
    unfolding inner_complex_def by (simp add: right_distrib)
huffman@29993
   202
  show "0 \<le> inner x x"
huffman@29993
   203
    unfolding inner_complex_def by (simp add: add_nonneg_nonneg)
huffman@29993
   204
  show "inner x x = 0 \<longleftrightarrow> x = 0"
huffman@29993
   205
    unfolding inner_complex_def
huffman@29993
   206
    by (simp add: add_nonneg_eq_0_iff complex_Re_Im_cancel_iff)
huffman@29993
   207
  show "norm x = sqrt (inner x x)"
huffman@29993
   208
    unfolding inner_complex_def complex_norm_def
huffman@29993
   209
    by (simp add: power2_eq_square)
huffman@29993
   210
qed
huffman@29993
   211
huffman@29993
   212
end
huffman@29993
   213
huffman@29993
   214
huffman@29993
   215
subsection {* Gradient derivative *}
huffman@29993
   216
huffman@29993
   217
definition
huffman@29993
   218
  gderiv ::
huffman@29993
   219
    "['a::real_inner \<Rightarrow> real, 'a, 'a] \<Rightarrow> bool"
huffman@29993
   220
          ("(GDERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60)
huffman@29993
   221
where
huffman@29993
   222
  "GDERIV f x :> D \<longleftrightarrow> FDERIV f x :> (\<lambda>h. inner h D)"
huffman@29993
   223
huffman@29993
   224
lemma deriv_fderiv: "DERIV f x :> D \<longleftrightarrow> FDERIV f x :> (\<lambda>h. h * D)"
huffman@29993
   225
  by (simp only: deriv_def field_fderiv_def)
huffman@29993
   226
huffman@29993
   227
lemma gderiv_deriv [simp]: "GDERIV f x :> D \<longleftrightarrow> DERIV f x :> D"
huffman@29993
   228
  by (simp only: gderiv_def deriv_fderiv inner_real_def)
huffman@29993
   229
huffman@29993
   230
lemma GDERIV_DERIV_compose:
huffman@29993
   231
    "\<lbrakk>GDERIV f x :> df; DERIV g (f x) :> dg\<rbrakk>
huffman@29993
   232
     \<Longrightarrow> GDERIV (\<lambda>x. g (f x)) x :> scaleR dg df"
huffman@29993
   233
  unfolding gderiv_def deriv_fderiv
huffman@29993
   234
  apply (drule (1) FDERIV_compose)
huffman@29993
   235
  apply (simp add: inner_scaleR_right mult_ac)
huffman@29993
   236
  done
huffman@29993
   237
huffman@29993
   238
lemma FDERIV_subst: "\<lbrakk>FDERIV f x :> df; df = d\<rbrakk> \<Longrightarrow> FDERIV f x :> d"
huffman@29993
   239
  by simp
huffman@29993
   240
huffman@29993
   241
lemma GDERIV_subst: "\<lbrakk>GDERIV f x :> df; df = d\<rbrakk> \<Longrightarrow> GDERIV f x :> d"
huffman@29993
   242
  by simp
huffman@29993
   243
huffman@29993
   244
lemma GDERIV_const: "GDERIV (\<lambda>x. k) x :> 0"
huffman@29993
   245
  unfolding gderiv_def inner_right.zero by (rule FDERIV_const)
huffman@29993
   246
huffman@29993
   247
lemma GDERIV_add:
huffman@29993
   248
    "\<lbrakk>GDERIV f x :> df; GDERIV g x :> dg\<rbrakk>
huffman@29993
   249
     \<Longrightarrow> GDERIV (\<lambda>x. f x + g x) x :> df + dg"
huffman@29993
   250
  unfolding gderiv_def inner_right.add by (rule FDERIV_add)
huffman@29993
   251
huffman@29993
   252
lemma GDERIV_minus:
huffman@29993
   253
    "GDERIV f x :> df \<Longrightarrow> GDERIV (\<lambda>x. - f x) x :> - df"
huffman@29993
   254
  unfolding gderiv_def inner_right.minus by (rule FDERIV_minus)
huffman@29993
   255
huffman@29993
   256
lemma GDERIV_diff:
huffman@29993
   257
    "\<lbrakk>GDERIV f x :> df; GDERIV g x :> dg\<rbrakk>
huffman@29993
   258
     \<Longrightarrow> GDERIV (\<lambda>x. f x - g x) x :> df - dg"
huffman@29993
   259
  unfolding gderiv_def inner_right.diff by (rule FDERIV_diff)
huffman@29993
   260
huffman@29993
   261
lemma GDERIV_scaleR:
huffman@29993
   262
    "\<lbrakk>DERIV f x :> df; GDERIV g x :> dg\<rbrakk>
huffman@29993
   263
     \<Longrightarrow> GDERIV (\<lambda>x. scaleR (f x) (g x)) x
huffman@29993
   264
      :> (scaleR (f x) dg + scaleR df (g x))"
huffman@29993
   265
  unfolding gderiv_def deriv_fderiv inner_right.add inner_right.scaleR
huffman@29993
   266
  apply (rule FDERIV_subst)
huffman@29993
   267
  apply (erule (1) scaleR.FDERIV)
huffman@29993
   268
  apply (simp add: mult_ac)
huffman@29993
   269
  done
huffman@29993
   270
huffman@29993
   271
lemma GDERIV_mult:
huffman@29993
   272
    "\<lbrakk>GDERIV f x :> df; GDERIV g x :> dg\<rbrakk>
huffman@29993
   273
     \<Longrightarrow> GDERIV (\<lambda>x. f x * g x) x :> scaleR (f x) dg + scaleR (g x) df"
huffman@29993
   274
  unfolding gderiv_def
huffman@29993
   275
  apply (rule FDERIV_subst)
huffman@29993
   276
  apply (erule (1) FDERIV_mult)
huffman@29993
   277
  apply (simp add: inner_distrib inner_scaleR mult_ac)
huffman@29993
   278
  done
huffman@29993
   279
huffman@29993
   280
lemma GDERIV_inverse:
huffman@29993
   281
    "\<lbrakk>GDERIV f x :> df; f x \<noteq> 0\<rbrakk>
huffman@29993
   282
     \<Longrightarrow> GDERIV (\<lambda>x. inverse (f x)) x :> - (inverse (f x))\<twosuperior> *\<^sub>R df"
huffman@29993
   283
  apply (erule GDERIV_DERIV_compose)
huffman@29993
   284
  apply (erule DERIV_inverse [folded numeral_2_eq_2])
huffman@29993
   285
  done
huffman@29993
   286
huffman@29993
   287
lemma GDERIV_norm:
huffman@29993
   288
  assumes "x \<noteq> 0" shows "GDERIV (\<lambda>x. norm x) x :> sgn x"
huffman@29993
   289
proof -
huffman@29993
   290
  have 1: "FDERIV (\<lambda>x. inner x x) x :> (\<lambda>h. inner x h + inner h x)"
huffman@29993
   291
    by (intro inner.FDERIV FDERIV_ident)
huffman@29993
   292
  have 2: "(\<lambda>h. inner x h + inner h x) = (\<lambda>h. inner h (scaleR 2 x))"
huffman@29993
   293
    by (simp add: expand_fun_eq inner_scaleR inner_commute)
huffman@29993
   294
  have "0 < inner x x" using `x \<noteq> 0` by simp
huffman@29993
   295
  then have 3: "DERIV sqrt (inner x x) :> (inverse (sqrt (inner x x)) / 2)"
huffman@29993
   296
    by (rule DERIV_real_sqrt)
huffman@29993
   297
  have 4: "(inverse (sqrt (inner x x)) / 2) *\<^sub>R 2 *\<^sub>R x = sgn x"
huffman@29993
   298
    by (simp add: sgn_div_norm norm_eq_sqrt_inner)
huffman@29993
   299
  show ?thesis
huffman@29993
   300
    unfolding norm_eq_sqrt_inner
huffman@29993
   301
    apply (rule GDERIV_subst [OF _ 4])
huffman@29993
   302
    apply (rule GDERIV_DERIV_compose [where g=sqrt and df="scaleR 2 x"])
huffman@29993
   303
    apply (subst gderiv_def)
huffman@29993
   304
    apply (rule FDERIV_subst [OF _ 2])
huffman@29993
   305
    apply (rule 1)
huffman@29993
   306
    apply (rule 3)
huffman@29993
   307
    done
huffman@29993
   308
qed
huffman@29993
   309
huffman@29993
   310
lemmas FDERIV_norm = GDERIV_norm [unfolded gderiv_def]
huffman@29993
   311
huffman@29993
   312
end