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