src/HOL/Analysis/Inner_Product.thy
author paulson <lp15@cam.ac.uk>
Tue Jun 26 14:51:18 2018 +0100 (14 months ago)
changeset 68499 d4312962161a
parent 68073 fad29d2a17a5
child 68611 4bc4b5c0ccfc
permissions -rw-r--r--
Rationalisation of complex transcendentals, esp the Arg function
hoelzl@63971
     1
(*  Title:      HOL/Analysis/Inner_Product.thy
wenzelm@41959
     2
    Author:     Brian Huffman
huffman@29993
     3
*)
huffman@29993
     4
wenzelm@60500
     5
section \<open>Inner Product Spaces and the Gradient Derivative\<close>
huffman@29993
     6
huffman@29993
     7
theory Inner_Product
wenzelm@65513
     8
imports Complex_Main
huffman@29993
     9
begin
huffman@29993
    10
wenzelm@60500
    11
subsection \<open>Real inner product spaces\<close>
huffman@29993
    12
wenzelm@60500
    13
text \<open>
hoelzl@62101
    14
  Temporarily relax type constraints for @{term "open"}, @{term "uniformity"},
huffman@31492
    15
  @{term dist}, and @{term norm}.
wenzelm@60500
    16
\<close>
huffman@31492
    17
wenzelm@60500
    18
setup \<open>Sign.add_const_constraint
wenzelm@60500
    19
  (@{const_name "open"}, SOME @{typ "'a::open set \<Rightarrow> bool"})\<close>
huffman@31446
    20
wenzelm@60500
    21
setup \<open>Sign.add_const_constraint
wenzelm@60500
    22
  (@{const_name dist}, SOME @{typ "'a::dist \<Rightarrow> 'a \<Rightarrow> real"})\<close>
huffman@31446
    23
wenzelm@60500
    24
setup \<open>Sign.add_const_constraint
hoelzl@62101
    25
  (@{const_name uniformity}, SOME @{typ "('a::uniformity \<times> 'a) filter"})\<close>
hoelzl@62101
    26
hoelzl@62101
    27
setup \<open>Sign.add_const_constraint
wenzelm@60500
    28
  (@{const_name norm}, SOME @{typ "'a::norm \<Rightarrow> real"})\<close>
huffman@31446
    29
immler@67962
    30
class%important real_inner = real_vector + sgn_div_norm + dist_norm + uniformity_dist + open_uniformity +
huffman@29993
    31
  fixes inner :: "'a \<Rightarrow> 'a \<Rightarrow> real"
huffman@29993
    32
  assumes inner_commute: "inner x y = inner y x"
huffman@31590
    33
  and inner_add_left: "inner (x + y) z = inner x z + inner y z"
huffman@31590
    34
  and inner_scaleR_left [simp]: "inner (scaleR r x) y = r * (inner x y)"
huffman@29993
    35
  and inner_ge_zero [simp]: "0 \<le> inner x x"
huffman@29993
    36
  and inner_eq_zero_iff [simp]: "inner x x = 0 \<longleftrightarrow> x = 0"
huffman@29993
    37
  and norm_eq_sqrt_inner: "norm x = sqrt (inner x x)"
huffman@29993
    38
begin
huffman@29993
    39
huffman@29993
    40
lemma inner_zero_left [simp]: "inner 0 x = 0"
huffman@31590
    41
  using inner_add_left [of 0 0 x] by simp
huffman@29993
    42
huffman@29993
    43
lemma inner_minus_left [simp]: "inner (- x) y = - inner x y"
huffman@31590
    44
  using inner_add_left [of x "- x" y] by simp
huffman@29993
    45
huffman@29993
    46
lemma inner_diff_left: "inner (x - y) z = inner x z - inner y z"
haftmann@54230
    47
  using inner_add_left [of x "- y" z] by simp
huffman@29993
    48
nipkow@64267
    49
lemma inner_sum_left: "inner (\<Sum>x\<in>A. f x) y = (\<Sum>x\<in>A. inner (f x) y)"
huffman@44282
    50
  by (cases "finite A", induct set: finite, simp_all add: inner_add_left)
huffman@44282
    51
lp15@67986
    52
lemma all_zero_iff [simp]: "(\<forall>u. inner x u = 0) \<longleftrightarrow> (x = 0)"
lp15@67986
    53
  by auto (use inner_eq_zero_iff in blast)
lp15@67986
    54
wenzelm@60500
    55
text \<open>Transfer distributivity rules to right argument.\<close>
huffman@29993
    56
huffman@31590
    57
lemma inner_add_right: "inner x (y + z) = inner x y + inner x z"
huffman@31590
    58
  using inner_add_left [of y z x] by (simp only: inner_commute)
huffman@29993
    59
huffman@31590
    60
lemma inner_scaleR_right [simp]: "inner x (scaleR r y) = r * (inner x y)"
huffman@29993
    61
  using inner_scaleR_left [of r y x] by (simp only: inner_commute)
huffman@29993
    62
huffman@29993
    63
lemma inner_zero_right [simp]: "inner x 0 = 0"
huffman@29993
    64
  using inner_zero_left [of x] by (simp only: inner_commute)
huffman@29993
    65
huffman@29993
    66
lemma inner_minus_right [simp]: "inner x (- y) = - inner x y"
huffman@29993
    67
  using inner_minus_left [of y x] by (simp only: inner_commute)
huffman@29993
    68
huffman@29993
    69
lemma inner_diff_right: "inner x (y - z) = inner x y - inner x z"
huffman@29993
    70
  using inner_diff_left [of y z x] by (simp only: inner_commute)
huffman@29993
    71
nipkow@64267
    72
lemma inner_sum_right: "inner x (\<Sum>y\<in>A. f y) = (\<Sum>y\<in>A. inner x (f y))"
nipkow@64267
    73
  using inner_sum_left [of f A x] by (simp only: inner_commute)
huffman@44282
    74
huffman@31590
    75
lemmas inner_add [algebra_simps] = inner_add_left inner_add_right
huffman@31590
    76
lemmas inner_diff [algebra_simps]  = inner_diff_left inner_diff_right
huffman@31590
    77
lemmas inner_scaleR = inner_scaleR_left inner_scaleR_right
huffman@31590
    78
wenzelm@60500
    79
text \<open>Legacy theorem names\<close>
huffman@31590
    80
lemmas inner_left_distrib = inner_add_left
huffman@31590
    81
lemmas inner_right_distrib = inner_add_right
huffman@29993
    82
lemmas inner_distrib = inner_left_distrib inner_right_distrib
huffman@29993
    83
huffman@29993
    84
lemma inner_gt_zero_iff [simp]: "0 < inner x x \<longleftrightarrow> x \<noteq> 0"
huffman@29993
    85
  by (simp add: order_less_le)
huffman@29993
    86
wenzelm@53015
    87
lemma power2_norm_eq_inner: "(norm x)\<^sup>2 = inner x x"
huffman@29993
    88
  by (simp add: norm_eq_sqrt_inner)
huffman@29993
    89
paulson@61518
    90
text \<open>Identities involving real multiplication and division.\<close>
paulson@61518
    91
paulson@61518
    92
lemma inner_mult_left: "inner (of_real m * a) b = m * (inner a b)"
paulson@61518
    93
  by (metis real_inner_class.inner_scaleR_left scaleR_conv_of_real)
paulson@61518
    94
paulson@61518
    95
lemma inner_mult_right: "inner a (of_real m * b) = m * (inner a b)"
paulson@61518
    96
  by (metis real_inner_class.inner_scaleR_right scaleR_conv_of_real)
paulson@61518
    97
paulson@61518
    98
lemma inner_mult_left': "inner (a * of_real m) b = m * (inner a b)"
paulson@61518
    99
  by (simp add: of_real_def)
paulson@61518
   100
paulson@61518
   101
lemma inner_mult_right': "inner a (b * of_real m) = (inner a b) * m"
paulson@61518
   102
  by (simp add: of_real_def real_inner_class.inner_scaleR_right)
paulson@61518
   103
huffman@30046
   104
lemma Cauchy_Schwarz_ineq:
wenzelm@53015
   105
  "(inner x y)\<^sup>2 \<le> inner x x * inner y y"
huffman@29993
   106
proof (cases)
huffman@29993
   107
  assume "y = 0"
huffman@29993
   108
  thus ?thesis by simp
huffman@29993
   109
next
huffman@29993
   110
  assume y: "y \<noteq> 0"
huffman@29993
   111
  let ?r = "inner x y / inner y y"
huffman@29993
   112
  have "0 \<le> inner (x - scaleR ?r y) (x - scaleR ?r y)"
huffman@29993
   113
    by (rule inner_ge_zero)
huffman@29993
   114
  also have "\<dots> = inner x x - inner y x * ?r"
huffman@31590
   115
    by (simp add: inner_diff)
wenzelm@53015
   116
  also have "\<dots> = inner x x - (inner x y)\<^sup>2 / inner y y"
huffman@29993
   117
    by (simp add: power2_eq_square inner_commute)
wenzelm@53015
   118
  finally have "0 \<le> inner x x - (inner x y)\<^sup>2 / inner y y" .
wenzelm@53015
   119
  hence "(inner x y)\<^sup>2 / inner y y \<le> inner x x"
huffman@29993
   120
    by (simp add: le_diff_eq)
wenzelm@53015
   121
  thus "(inner x y)\<^sup>2 \<le> inner x x * inner y y"
huffman@29993
   122
    by (simp add: pos_divide_le_eq y)
huffman@29993
   123
qed
huffman@29993
   124
huffman@30046
   125
lemma Cauchy_Schwarz_ineq2:
huffman@29993
   126
  "\<bar>inner x y\<bar> \<le> norm x * norm y"
huffman@29993
   127
proof (rule power2_le_imp_le)
wenzelm@53015
   128
  have "(inner x y)\<^sup>2 \<le> inner x x * inner y y"
huffman@30046
   129
    using Cauchy_Schwarz_ineq .
wenzelm@53015
   130
  thus "\<bar>inner x y\<bar>\<^sup>2 \<le> (norm x * norm y)\<^sup>2"
huffman@29993
   131
    by (simp add: power_mult_distrib power2_norm_eq_inner)
huffman@29993
   132
  show "0 \<le> norm x * norm y"
huffman@29993
   133
    unfolding norm_eq_sqrt_inner
huffman@29993
   134
    by (intro mult_nonneg_nonneg real_sqrt_ge_zero inner_ge_zero)
huffman@29993
   135
qed
huffman@29993
   136
huffman@53938
   137
lemma norm_cauchy_schwarz: "inner x y \<le> norm x * norm y"
huffman@53938
   138
  using Cauchy_Schwarz_ineq2 [of x y] by auto
huffman@53938
   139
huffman@29993
   140
subclass real_normed_vector
huffman@29993
   141
proof
huffman@29993
   142
  fix a :: real and x y :: 'a
huffman@29993
   143
  show "norm x = 0 \<longleftrightarrow> x = 0"
huffman@29993
   144
    unfolding norm_eq_sqrt_inner by simp
huffman@29993
   145
  show "norm (x + y) \<le> norm x + norm y"
huffman@29993
   146
    proof (rule power2_le_imp_le)
huffman@29993
   147
      have "inner x y \<le> norm x * norm y"
huffman@53938
   148
        by (rule norm_cauchy_schwarz)
wenzelm@53015
   149
      thus "(norm (x + y))\<^sup>2 \<le> (norm x + norm y)\<^sup>2"
huffman@29993
   150
        unfolding power2_sum power2_norm_eq_inner
huffman@31590
   151
        by (simp add: inner_add inner_commute)
huffman@29993
   152
      show "0 \<le> norm x + norm y"
huffman@44126
   153
        unfolding norm_eq_sqrt_inner by simp
huffman@29993
   154
    qed
wenzelm@53015
   155
  have "sqrt (a\<^sup>2 * inner x x) = \<bar>a\<bar> * sqrt (inner x x)"
huffman@29993
   156
    by (simp add: real_sqrt_mult_distrib)
huffman@29993
   157
  then show "norm (a *\<^sub>R x) = \<bar>a\<bar> * norm x"
huffman@29993
   158
    unfolding norm_eq_sqrt_inner
haftmann@57512
   159
    by (simp add: power2_eq_square mult.assoc)
huffman@29993
   160
qed
huffman@29993
   161
huffman@29993
   162
end
huffman@29993
   163
immler@68072
   164
lemma square_bound_lemma:
immler@68072
   165
  fixes x :: real
immler@68072
   166
  shows "x < (1 + x) * (1 + x)"
immler@68072
   167
proof -
immler@68072
   168
  have "(x + 1/2)\<^sup>2 + 3/4 > 0"
immler@68072
   169
    using zero_le_power2[of "x+1/2"] by arith
immler@68072
   170
  then show ?thesis
immler@68072
   171
    by (simp add: field_simps power2_eq_square)
immler@68072
   172
qed
immler@68072
   173
immler@68072
   174
lemma square_continuous:
immler@68072
   175
  fixes e :: real
immler@68072
   176
  shows "e > 0 \<Longrightarrow> \<exists>d. 0 < d \<and> (\<forall>y. \<bar>y - x\<bar> < d \<longrightarrow> \<bar>y * y - x * x\<bar> < e)"
immler@68072
   177
  using isCont_power[OF continuous_ident, of x, unfolded isCont_def LIM_eq, rule_format, of e 2]
immler@68072
   178
  by (force simp add: power2_eq_square)
immler@68072
   179
immler@68072
   180
lemma norm_triangle_sub:
immler@68072
   181
  fixes x y :: "'a::real_normed_vector"
immler@68072
   182
  shows "norm x \<le> norm y + norm (x - y)"
immler@68072
   183
  using norm_triangle_ineq[of "y" "x - y"] by (simp add: field_simps)
immler@68072
   184
immler@68072
   185
lemma norm_le: "norm x \<le> norm y \<longleftrightarrow> inner x x \<le> inner y y"
immler@68072
   186
  by (simp add: norm_eq_sqrt_inner)
immler@68072
   187
immler@68072
   188
lemma norm_lt: "norm x < norm y \<longleftrightarrow> inner x x < inner y y"
immler@68072
   189
  by (simp add: norm_eq_sqrt_inner)
immler@68072
   190
immler@68072
   191
lemma norm_eq: "norm x = norm y \<longleftrightarrow> inner x x = inner y y"
immler@68072
   192
  apply (subst order_eq_iff)
immler@68072
   193
  apply (auto simp: norm_le)
immler@68072
   194
  done
immler@68072
   195
immler@68072
   196
lemma norm_eq_1: "norm x = 1 \<longleftrightarrow> inner x x = 1"
immler@68072
   197
  by (simp add: norm_eq_sqrt_inner)
immler@68072
   198
paulson@61518
   199
lemma inner_divide_left:
paulson@61518
   200
  fixes a :: "'a :: {real_inner,real_div_algebra}"
paulson@61518
   201
  shows "inner (a / of_real m) b = (inner a b) / m"
paulson@61518
   202
  by (metis (no_types) divide_inverse inner_commute inner_scaleR_right mult.left_neutral mult.right_neutral mult_scaleR_right of_real_inverse scaleR_conv_of_real times_divide_eq_left)
paulson@61518
   203
paulson@61518
   204
lemma inner_divide_right:
paulson@61518
   205
  fixes a :: "'a :: {real_inner,real_div_algebra}"
paulson@61518
   206
  shows "inner a (b / of_real m) = (inner a b) / m"
paulson@61518
   207
  by (metis inner_commute inner_divide_left)
paulson@61518
   208
wenzelm@60500
   209
text \<open>
hoelzl@62101
   210
  Re-enable constraints for @{term "open"}, @{term "uniformity"},
huffman@31492
   211
  @{term dist}, and @{term norm}.
wenzelm@60500
   212
\<close>
huffman@31492
   213
wenzelm@60500
   214
setup \<open>Sign.add_const_constraint
wenzelm@60500
   215
  (@{const_name "open"}, SOME @{typ "'a::topological_space set \<Rightarrow> bool"})\<close>
huffman@31446
   216
wenzelm@60500
   217
setup \<open>Sign.add_const_constraint
hoelzl@62101
   218
  (@{const_name uniformity}, SOME @{typ "('a::uniform_space \<times> 'a) filter"})\<close>
hoelzl@62101
   219
hoelzl@62101
   220
setup \<open>Sign.add_const_constraint
wenzelm@60500
   221
  (@{const_name dist}, SOME @{typ "'a::metric_space \<Rightarrow> 'a \<Rightarrow> real"})\<close>
huffman@31446
   222
wenzelm@60500
   223
setup \<open>Sign.add_const_constraint
wenzelm@60500
   224
  (@{const_name norm}, SOME @{typ "'a::real_normed_vector \<Rightarrow> real"})\<close>
huffman@31446
   225
huffman@44282
   226
lemma bounded_bilinear_inner:
huffman@44282
   227
  "bounded_bilinear (inner::'a::real_inner \<Rightarrow> 'a \<Rightarrow> real)"
huffman@29993
   228
proof
huffman@29993
   229
  fix x y z :: 'a and r :: real
huffman@29993
   230
  show "inner (x + y) z = inner x z + inner y z"
huffman@31590
   231
    by (rule inner_add_left)
huffman@29993
   232
  show "inner x (y + z) = inner x y + inner x z"
huffman@31590
   233
    by (rule inner_add_right)
huffman@29993
   234
  show "inner (scaleR r x) y = scaleR r (inner x y)"
huffman@29993
   235
    unfolding real_scaleR_def by (rule inner_scaleR_left)
huffman@29993
   236
  show "inner x (scaleR r y) = scaleR r (inner x y)"
huffman@29993
   237
    unfolding real_scaleR_def by (rule inner_scaleR_right)
huffman@29993
   238
  show "\<exists>K. \<forall>x y::'a. norm (inner x y) \<le> norm x * norm y * K"
huffman@29993
   239
  proof
huffman@29993
   240
    show "\<forall>x y::'a. norm (inner x y) \<le> norm x * norm y * 1"
huffman@30046
   241
      by (simp add: Cauchy_Schwarz_ineq2)
huffman@29993
   242
  qed
huffman@29993
   243
qed
huffman@29993
   244
huffman@44282
   245
lemmas tendsto_inner [tendsto_intros] =
huffman@44282
   246
  bounded_bilinear.tendsto [OF bounded_bilinear_inner]
huffman@44282
   247
huffman@44282
   248
lemmas isCont_inner [simp] =
huffman@44282
   249
  bounded_bilinear.isCont [OF bounded_bilinear_inner]
huffman@29993
   250
hoelzl@56381
   251
lemmas has_derivative_inner [derivative_intros] =
huffman@44282
   252
  bounded_bilinear.FDERIV [OF bounded_bilinear_inner]
huffman@29993
   253
huffman@44282
   254
lemmas bounded_linear_inner_left =
huffman@44282
   255
  bounded_bilinear.bounded_linear_left [OF bounded_bilinear_inner]
huffman@44282
   256
huffman@44282
   257
lemmas bounded_linear_inner_right =
huffman@44282
   258
  bounded_bilinear.bounded_linear_right [OF bounded_bilinear_inner]
huffman@44233
   259
immler@61915
   260
lemmas bounded_linear_inner_left_comp = bounded_linear_inner_left[THEN bounded_linear_compose]
immler@61915
   261
immler@61915
   262
lemmas bounded_linear_inner_right_comp = bounded_linear_inner_right[THEN bounded_linear_compose]
immler@61915
   263
hoelzl@56381
   264
lemmas has_derivative_inner_right [derivative_intros] =
hoelzl@56181
   265
  bounded_linear.has_derivative [OF bounded_linear_inner_right]
hoelzl@51642
   266
hoelzl@56381
   267
lemmas has_derivative_inner_left [derivative_intros] =
hoelzl@56181
   268
  bounded_linear.has_derivative [OF bounded_linear_inner_left]
hoelzl@51642
   269
hoelzl@51642
   270
lemma differentiable_inner [simp]:
hoelzl@56181
   271
  "f differentiable (at x within s) \<Longrightarrow> g differentiable at x within s \<Longrightarrow> (\<lambda>x. inner (f x) (g x)) differentiable at x within s"
hoelzl@56181
   272
  unfolding differentiable_def by (blast intro: has_derivative_inner)
huffman@29993
   273
wenzelm@60679
   274
wenzelm@60500
   275
subsection \<open>Class instances\<close>
huffman@29993
   276
immler@67962
   277
instantiation%important real :: real_inner
huffman@29993
   278
begin
huffman@29993
   279
nipkow@67399
   280
definition inner_real_def [simp]: "inner = ( * )"
huffman@29993
   281
wenzelm@60679
   282
instance
wenzelm@60679
   283
proof
huffman@29993
   284
  fix x y z r :: real
huffman@29993
   285
  show "inner x y = inner y x"
haftmann@57512
   286
    unfolding inner_real_def by (rule mult.commute)
huffman@29993
   287
  show "inner (x + y) z = inner x z + inner y z"
webertj@49962
   288
    unfolding inner_real_def by (rule distrib_right)
huffman@29993
   289
  show "inner (scaleR r x) y = r * inner x y"
haftmann@57512
   290
    unfolding inner_real_def real_scaleR_def by (rule mult.assoc)
huffman@29993
   291
  show "0 \<le> inner x x"
huffman@29993
   292
    unfolding inner_real_def by simp
huffman@29993
   293
  show "inner x x = 0 \<longleftrightarrow> x = 0"
huffman@29993
   294
    unfolding inner_real_def by simp
huffman@29993
   295
  show "norm x = sqrt (inner x x)"
huffman@29993
   296
    unfolding inner_real_def by simp
huffman@29993
   297
qed
huffman@29993
   298
huffman@29993
   299
end
huffman@29993
   300
hoelzl@63886
   301
lemma
hoelzl@63886
   302
  shows real_inner_1_left[simp]: "inner 1 x = x"
hoelzl@63886
   303
    and real_inner_1_right[simp]: "inner x 1 = x"
hoelzl@63886
   304
  by simp_all
hoelzl@63886
   305
immler@67962
   306
instantiation%important complex :: real_inner
huffman@29993
   307
begin
huffman@29993
   308
huffman@29993
   309
definition inner_complex_def:
huffman@29993
   310
  "inner x y = Re x * Re y + Im x * Im y"
huffman@29993
   311
wenzelm@60679
   312
instance
wenzelm@60679
   313
proof
huffman@29993
   314
  fix x y z :: complex and r :: real
huffman@29993
   315
  show "inner x y = inner y x"
haftmann@57512
   316
    unfolding inner_complex_def by (simp add: mult.commute)
huffman@29993
   317
  show "inner (x + y) z = inner x z + inner y z"
webertj@49962
   318
    unfolding inner_complex_def by (simp add: distrib_right)
huffman@29993
   319
  show "inner (scaleR r x) y = r * inner x y"
webertj@49962
   320
    unfolding inner_complex_def by (simp add: distrib_left)
huffman@29993
   321
  show "0 \<le> inner x x"
huffman@44126
   322
    unfolding inner_complex_def by simp
huffman@29993
   323
  show "inner x x = 0 \<longleftrightarrow> x = 0"
huffman@29993
   324
    unfolding inner_complex_def
lp15@68499
   325
    by (simp add: add_nonneg_eq_0_iff complex_eq_iff)
huffman@29993
   326
  show "norm x = sqrt (inner x x)"
lp15@68499
   327
    unfolding inner_complex_def norm_complex_def
huffman@29993
   328
    by (simp add: power2_eq_square)
huffman@29993
   329
qed
huffman@29993
   330
huffman@29993
   331
end
huffman@29993
   332
huffman@44902
   333
lemma complex_inner_1 [simp]: "inner 1 x = Re x"
huffman@44902
   334
  unfolding inner_complex_def by simp
huffman@44902
   335
huffman@44902
   336
lemma complex_inner_1_right [simp]: "inner x 1 = Re x"
huffman@44902
   337
  unfolding inner_complex_def by simp
huffman@44902
   338
lp15@65064
   339
lemma complex_inner_i_left [simp]: "inner \<i> x = Im x"
huffman@44902
   340
  unfolding inner_complex_def by simp
huffman@44902
   341
lp15@65064
   342
lemma complex_inner_i_right [simp]: "inner x \<i> = Im x"
huffman@44902
   343
  unfolding inner_complex_def by simp
huffman@44902
   344
huffman@29993
   345
eberlm@66486
   346
lemma dot_square_norm: "inner x x = (norm x)\<^sup>2"
eberlm@66486
   347
  by (simp only: power2_norm_eq_inner) (* TODO: move? *)
eberlm@66486
   348
eberlm@66486
   349
lemma norm_eq_square: "norm x = a \<longleftrightarrow> 0 \<le> a \<and> inner x x = a\<^sup>2"
eberlm@66486
   350
  by (auto simp add: norm_eq_sqrt_inner)
eberlm@66486
   351
eberlm@66486
   352
lemma norm_le_square: "norm x \<le> a \<longleftrightarrow> 0 \<le> a \<and> inner x x \<le> a\<^sup>2"
eberlm@66486
   353
  apply (simp add: dot_square_norm abs_le_square_iff[symmetric])
eberlm@66486
   354
  using norm_ge_zero[of x]
eberlm@66486
   355
  apply arith
eberlm@66486
   356
  done
eberlm@66486
   357
eberlm@66486
   358
lemma norm_ge_square: "norm x \<ge> a \<longleftrightarrow> a \<le> 0 \<or> inner x x \<ge> a\<^sup>2"
eberlm@66486
   359
  apply (simp add: dot_square_norm abs_le_square_iff[symmetric])
eberlm@66486
   360
  using norm_ge_zero[of x]
eberlm@66486
   361
  apply arith
eberlm@66486
   362
  done
eberlm@66486
   363
eberlm@66486
   364
lemma norm_lt_square: "norm x < a \<longleftrightarrow> 0 < a \<and> inner x x < a\<^sup>2"
eberlm@66486
   365
  by (metis not_le norm_ge_square)
eberlm@66486
   366
eberlm@66486
   367
lemma norm_gt_square: "norm x > a \<longleftrightarrow> a < 0 \<or> inner x x > a\<^sup>2"
eberlm@66486
   368
  by (metis norm_le_square not_less)
eberlm@66486
   369
eberlm@66486
   370
text\<open>Dot product in terms of the norm rather than conversely.\<close>
eberlm@66486
   371
eberlm@66486
   372
lemmas inner_simps = inner_add_left inner_add_right inner_diff_right inner_diff_left
eberlm@66486
   373
  inner_scaleR_left inner_scaleR_right
eberlm@66486
   374
eberlm@66486
   375
lemma dot_norm: "inner x y = ((norm (x + y))\<^sup>2 - (norm x)\<^sup>2 - (norm y)\<^sup>2) / 2"
eberlm@66486
   376
  by (simp only: power2_norm_eq_inner inner_simps inner_commute) auto
eberlm@66486
   377
eberlm@66486
   378
lemma dot_norm_neg: "inner x y = (((norm x)\<^sup>2 + (norm y)\<^sup>2) - (norm (x - y))\<^sup>2) / 2"
eberlm@66486
   379
  by (simp only: power2_norm_eq_inner inner_simps inner_commute)
eberlm@66486
   380
    (auto simp add: algebra_simps)
eberlm@66486
   381
eberlm@66486
   382
lemma of_real_inner_1 [simp]: 
eberlm@66486
   383
  "inner (of_real x) (1 :: 'a :: {real_inner, real_normed_algebra_1}) = x"
eberlm@66486
   384
  by (simp add: of_real_def dot_square_norm)
eberlm@66486
   385
  
eberlm@66486
   386
lemma summable_of_real_iff: 
eberlm@66486
   387
  "summable (\<lambda>x. of_real (f x) :: 'a :: {real_normed_algebra_1,real_inner}) \<longleftrightarrow> summable f"
eberlm@66486
   388
proof
eberlm@66486
   389
  assume *: "summable (\<lambda>x. of_real (f x) :: 'a)"
eberlm@66486
   390
  interpret bounded_linear "\<lambda>x::'a. inner x 1"
eberlm@66486
   391
    by (rule bounded_linear_inner_left)
eberlm@66486
   392
  from summable [OF *] show "summable f" by simp
eberlm@66486
   393
qed (auto intro: summable_of_real)
eberlm@66486
   394
eberlm@66486
   395
wenzelm@60500
   396
subsection \<open>Gradient derivative\<close>
huffman@29993
   397
immler@67962
   398
definition%important
huffman@29993
   399
  gderiv ::
huffman@29993
   400
    "['a::real_inner \<Rightarrow> real, 'a, 'a] \<Rightarrow> bool"
huffman@29993
   401
          ("(GDERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60)
huffman@29993
   402
where
huffman@29993
   403
  "GDERIV f x :> D \<longleftrightarrow> FDERIV f x :> (\<lambda>h. inner h D)"
huffman@29993
   404
huffman@29993
   405
lemma gderiv_deriv [simp]: "GDERIV f x :> D \<longleftrightarrow> DERIV f x :> D"
hoelzl@56181
   406
  by (simp only: gderiv_def has_field_derivative_def inner_real_def mult_commute_abs)
huffman@29993
   407
huffman@29993
   408
lemma GDERIV_DERIV_compose:
huffman@29993
   409
    "\<lbrakk>GDERIV f x :> df; DERIV g (f x) :> dg\<rbrakk>
huffman@29993
   410
     \<Longrightarrow> GDERIV (\<lambda>x. g (f x)) x :> scaleR dg df"
hoelzl@56181
   411
  unfolding gderiv_def has_field_derivative_def
hoelzl@56181
   412
  apply (drule (1) has_derivative_compose)
haftmann@57514
   413
  apply (simp add: ac_simps)
huffman@29993
   414
  done
huffman@29993
   415
hoelzl@56181
   416
lemma has_derivative_subst: "\<lbrakk>FDERIV f x :> df; df = d\<rbrakk> \<Longrightarrow> FDERIV f x :> d"
huffman@29993
   417
  by simp
huffman@29993
   418
huffman@29993
   419
lemma GDERIV_subst: "\<lbrakk>GDERIV f x :> df; df = d\<rbrakk> \<Longrightarrow> GDERIV f x :> d"
huffman@29993
   420
  by simp
huffman@29993
   421
huffman@29993
   422
lemma GDERIV_const: "GDERIV (\<lambda>x. k) x :> 0"
hoelzl@56181
   423
  unfolding gderiv_def inner_zero_right by (rule has_derivative_const)
huffman@29993
   424
huffman@29993
   425
lemma GDERIV_add:
huffman@29993
   426
    "\<lbrakk>GDERIV f x :> df; GDERIV g x :> dg\<rbrakk>
huffman@29993
   427
     \<Longrightarrow> GDERIV (\<lambda>x. f x + g x) x :> df + dg"
hoelzl@56181
   428
  unfolding gderiv_def inner_add_right by (rule has_derivative_add)
huffman@29993
   429
huffman@29993
   430
lemma GDERIV_minus:
huffman@29993
   431
    "GDERIV f x :> df \<Longrightarrow> GDERIV (\<lambda>x. - f x) x :> - df"
hoelzl@56181
   432
  unfolding gderiv_def inner_minus_right by (rule has_derivative_minus)
huffman@29993
   433
huffman@29993
   434
lemma GDERIV_diff:
huffman@29993
   435
    "\<lbrakk>GDERIV f x :> df; GDERIV g x :> dg\<rbrakk>
huffman@29993
   436
     \<Longrightarrow> GDERIV (\<lambda>x. f x - g x) x :> df - dg"
hoelzl@56181
   437
  unfolding gderiv_def inner_diff_right by (rule has_derivative_diff)
huffman@29993
   438
huffman@29993
   439
lemma GDERIV_scaleR:
huffman@29993
   440
    "\<lbrakk>DERIV f x :> df; GDERIV g x :> dg\<rbrakk>
huffman@29993
   441
     \<Longrightarrow> GDERIV (\<lambda>x. scaleR (f x) (g x)) x
huffman@29993
   442
      :> (scaleR (f x) dg + scaleR df (g x))"
hoelzl@56181
   443
  unfolding gderiv_def has_field_derivative_def inner_add_right inner_scaleR_right
hoelzl@56181
   444
  apply (rule has_derivative_subst)
hoelzl@56181
   445
  apply (erule (1) has_derivative_scaleR)
haftmann@57514
   446
  apply (simp add: ac_simps)
huffman@29993
   447
  done
huffman@29993
   448
huffman@29993
   449
lemma GDERIV_mult:
huffman@29993
   450
    "\<lbrakk>GDERIV f x :> df; GDERIV g x :> dg\<rbrakk>
huffman@29993
   451
     \<Longrightarrow> GDERIV (\<lambda>x. f x * g x) x :> scaleR (f x) dg + scaleR (g x) df"
huffman@29993
   452
  unfolding gderiv_def
hoelzl@56181
   453
  apply (rule has_derivative_subst)
hoelzl@56181
   454
  apply (erule (1) has_derivative_mult)
haftmann@57514
   455
  apply (simp add: inner_add ac_simps)
huffman@29993
   456
  done
huffman@29993
   457
huffman@29993
   458
lemma GDERIV_inverse:
huffman@29993
   459
    "\<lbrakk>GDERIV f x :> df; f x \<noteq> 0\<rbrakk>
wenzelm@53015
   460
     \<Longrightarrow> GDERIV (\<lambda>x. inverse (f x)) x :> - (inverse (f x))\<^sup>2 *\<^sub>R df"
lp15@67986
   461
  by (metis DERIV_inverse GDERIV_DERIV_compose numerals(2))
lp15@67986
   462
  
huffman@29993
   463
lemma GDERIV_norm:
huffman@29993
   464
  assumes "x \<noteq> 0" shows "GDERIV (\<lambda>x. norm x) x :> sgn x"
lp15@67986
   465
    unfolding gderiv_def norm_eq_sqrt_inner
lp15@67986
   466
    by (rule derivative_eq_intros | force simp add: inner_commute sgn_div_norm norm_eq_sqrt_inner assms)+
huffman@29993
   467
hoelzl@56181
   468
lemmas has_derivative_norm = GDERIV_norm [unfolded gderiv_def]
huffman@29993
   469
huffman@29993
   470
end