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