wneuper/isa: src/HOL/Library/Inner_Product.thy@571cb1df0768

     1 (*  Title:      HOL/Library/Inner_Product.thy

     2     Author:     Brian Huffman

     3 *)

     5 header {* Inner Product Spaces and the Gradient Derivative *}

     7 theory Inner_Product

     8 imports FrechetDeriv

     9 begin

    11 subsection {* Real inner product spaces *}

    13 text {*

    14   Temporarily relax type constraints for @{term "open"},

    15   @{term dist}, and @{term norm}.

    16 *}

    18 setup {* Sign.add_const_constraint

    19   (@{const_name "open"}, SOME @{typ "'a::open set \<Rightarrow> bool"}) *}

    21 setup {* Sign.add_const_constraint

    22   (@{const_name dist}, SOME @{typ "'a::dist \<Rightarrow> 'a \<Rightarrow> real"}) *}

    24 setup {* Sign.add_const_constraint

    25   (@{const_name norm}, SOME @{typ "'a::norm \<Rightarrow> real"}) *}

    27 class real_inner = real_vector + sgn_div_norm + dist_norm + open_dist +

    28   fixes inner :: "'a \<Rightarrow> 'a \<Rightarrow> real"

    29   assumes inner_commute: "inner x y = inner y x"

    30   and inner_add_left: "inner (x + y) z = inner x z + inner y z"

    31   and inner_scaleR_left [simp]: "inner (scaleR r x) y = r * (inner x y)"

    32   and inner_ge_zero [simp]: "0 \<le> inner x x"

    33   and inner_eq_zero_iff [simp]: "inner x x = 0 \<longleftrightarrow> x = 0"

    34   and norm_eq_sqrt_inner: "norm x = sqrt (inner x x)"

    35 begin

    37 lemma inner_zero_left [simp]: "inner 0 x = 0"

    38   using inner_add_left [of 0 0 x] by simp

    40 lemma inner_minus_left [simp]: "inner (- x) y = - inner x y"

    41   using inner_add_left [of x "- x" y] by simp

    43 lemma inner_diff_left: "inner (x - y) z = inner x z - inner y z"

    44   by (simp add: diff_minus inner_add_left)

    46 lemma inner_setsum_left: "inner (\<Sum>x\<in>A. f x) y = (\<Sum>x\<in>A. inner (f x) y)"

    47   by (cases "finite A", induct set: finite, simp_all add: inner_add_left)

    49 text {* Transfer distributivity rules to right argument. *}

    51 lemma inner_add_right: "inner x (y + z) = inner x y + inner x z"

    52   using inner_add_left [of y z x] by (simp only: inner_commute)

    54 lemma inner_scaleR_right [simp]: "inner x (scaleR r y) = r * (inner x y)"

    55   using inner_scaleR_left [of r y x] by (simp only: inner_commute)

    57 lemma inner_zero_right [simp]: "inner x 0 = 0"

    58   using inner_zero_left [of x] by (simp only: inner_commute)

    60 lemma inner_minus_right [simp]: "inner x (- y) = - inner x y"

    61   using inner_minus_left [of y x] by (simp only: inner_commute)

    63 lemma inner_diff_right: "inner x (y - z) = inner x y - inner x z"

    64   using inner_diff_left [of y z x] by (simp only: inner_commute)

    66 lemma inner_setsum_right: "inner x (\<Sum>y\<in>A. f y) = (\<Sum>y\<in>A. inner x (f y))"

    67   using inner_setsum_left [of f A x] by (simp only: inner_commute)

    69 lemmas inner_add [algebra_simps] = inner_add_left inner_add_right

    70 lemmas inner_diff [algebra_simps]  = inner_diff_left inner_diff_right

    71 lemmas inner_scaleR = inner_scaleR_left inner_scaleR_right

    73 text {* Legacy theorem names *}

    74 lemmas inner_left_distrib = inner_add_left

    75 lemmas inner_right_distrib = inner_add_right

    76 lemmas inner_distrib = inner_left_distrib inner_right_distrib

    78 lemma inner_gt_zero_iff [simp]: "0 < inner x x \<longleftrightarrow> x \<noteq> 0"

    79   by (simp add: order_less_le)

    81 lemma power2_norm_eq_inner: "(norm x)\<twosuperior> = inner x x"

    82   by (simp add: norm_eq_sqrt_inner)

    84 lemma Cauchy_Schwarz_ineq:

    85   "(inner x y)\<twosuperior> \<le> inner x x * inner y y"

    86 proof (cases)

    87   assume "y = 0"

    88   thus ?thesis by simp

    89 next

    90   assume y: "y \<noteq> 0"

    91   let ?r = "inner x y / inner y y"

    92   have "0 \<le> inner (x - scaleR ?r y) (x - scaleR ?r y)"

    93     by (rule inner_ge_zero)

    94   also have "\<dots> = inner x x - inner y x * ?r"

    95     by (simp add: inner_diff)

    96   also have "\<dots> = inner x x - (inner x y)\<twosuperior> / inner y y"

    97     by (simp add: power2_eq_square inner_commute)

    98   finally have "0 \<le> inner x x - (inner x y)\<twosuperior> / inner y y" .

    99   hence "(inner x y)\<twosuperior> / inner y y \<le> inner x x"

   100     by (simp add: le_diff_eq)

   101   thus "(inner x y)\<twosuperior> \<le> inner x x * inner y y"

   102     by (simp add: pos_divide_le_eq y)

   103 qed

   105 lemma Cauchy_Schwarz_ineq2:

   106   "\<bar>inner x y\<bar> \<le> norm x * norm y"

   107 proof (rule power2_le_imp_le)

   108   have "(inner x y)\<twosuperior> \<le> inner x x * inner y y"

   109     using Cauchy_Schwarz_ineq .

   110   thus "\<bar>inner x y\<bar>\<twosuperior> \<le> (norm x * norm y)\<twosuperior>"

   111     by (simp add: power_mult_distrib power2_norm_eq_inner)

   112   show "0 \<le> norm x * norm y"

   113     unfolding norm_eq_sqrt_inner

   114     by (intro mult_nonneg_nonneg real_sqrt_ge_zero inner_ge_zero)

   115 qed

   117 subclass real_normed_vector

   118 proof

   119   fix a :: real and x y :: 'a

   120   show "0 \<le> norm x"

   121     unfolding norm_eq_sqrt_inner by simp

   122   show "norm x = 0 \<longleftrightarrow> x = 0"

   123     unfolding norm_eq_sqrt_inner by simp

   124   show "norm (x + y) \<le> norm x + norm y"

   125     proof (rule power2_le_imp_le)

   126       have "inner x y \<le> norm x * norm y"

   127         by (rule order_trans [OF abs_ge_self Cauchy_Schwarz_ineq2])

   128       thus "(norm (x + y))\<twosuperior> \<le> (norm x + norm y)\<twosuperior>"

   129         unfolding power2_sum power2_norm_eq_inner

   130         by (simp add: inner_add inner_commute)

   131       show "0 \<le> norm x + norm y"

   132         unfolding norm_eq_sqrt_inner by simp

   133     qed

   134   have "sqrt (a\<twosuperior> * inner x x) = \<bar>a\<bar> * sqrt (inner x x)"

   135     by (simp add: real_sqrt_mult_distrib)

   136   then show "norm (a *\<^sub>R x) = \<bar>a\<bar> * norm x"

   137     unfolding norm_eq_sqrt_inner

   138     by (simp add: power2_eq_square mult_assoc)

   139 qed

   141 end

   143 text {*

   144   Re-enable constraints for @{term "open"},

   145   @{term dist}, and @{term norm}.

   146 *}

   148 setup {* Sign.add_const_constraint

   149   (@{const_name "open"}, SOME @{typ "'a::topological_space set \<Rightarrow> bool"}) *}

   151 setup {* Sign.add_const_constraint

   152   (@{const_name dist}, SOME @{typ "'a::metric_space \<Rightarrow> 'a \<Rightarrow> real"}) *}

   154 setup {* Sign.add_const_constraint

   155   (@{const_name norm}, SOME @{typ "'a::real_normed_vector \<Rightarrow> real"}) *}

   157 lemma bounded_bilinear_inner:

   158   "bounded_bilinear (inner::'a::real_inner \<Rightarrow> 'a \<Rightarrow> real)"

   159 proof

   160   fix x y z :: 'a and r :: real

   161   show "inner (x + y) z = inner x z + inner y z"

   162     by (rule inner_add_left)

   163   show "inner x (y + z) = inner x y + inner x z"

   164     by (rule inner_add_right)

   165   show "inner (scaleR r x) y = scaleR r (inner x y)"

   166     unfolding real_scaleR_def by (rule inner_scaleR_left)

   167   show "inner x (scaleR r y) = scaleR r (inner x y)"

   168     unfolding real_scaleR_def by (rule inner_scaleR_right)

   169   show "\<exists>K. \<forall>x y::'a. norm (inner x y) \<le> norm x * norm y * K"

   170   proof

   171     show "\<forall>x y::'a. norm (inner x y) \<le> norm x * norm y * 1"

   172       by (simp add: Cauchy_Schwarz_ineq2)

   173   qed

   174 qed

   176 lemmas tendsto_inner [tendsto_intros] =

   177   bounded_bilinear.tendsto [OF bounded_bilinear_inner]

   179 lemmas isCont_inner [simp] =

   180   bounded_bilinear.isCont [OF bounded_bilinear_inner]

   182 lemmas FDERIV_inner =

   183   bounded_bilinear.FDERIV [OF bounded_bilinear_inner]

   185 lemmas bounded_linear_inner_left =

   186   bounded_bilinear.bounded_linear_left [OF bounded_bilinear_inner]

   188 lemmas bounded_linear_inner_right =

   189   bounded_bilinear.bounded_linear_right [OF bounded_bilinear_inner]

   192 subsection {* Class instances *}

   194 instantiation real :: real_inner

   195 begin

   197 definition inner_real_def [simp]: "inner = op *"

   199 instance proof

   200   fix x y z r :: real

   201   show "inner x y = inner y x"

   202     unfolding inner_real_def by (rule mult_commute)

   203   show "inner (x + y) z = inner x z + inner y z"

   204     unfolding inner_real_def by (rule left_distrib)

   205   show "inner (scaleR r x) y = r * inner x y"

   206     unfolding inner_real_def real_scaleR_def by (rule mult_assoc)

   207   show "0 \<le> inner x x"

   208     unfolding inner_real_def by simp

   209   show "inner x x = 0 \<longleftrightarrow> x = 0"

   210     unfolding inner_real_def by simp

   211   show "norm x = sqrt (inner x x)"

   212     unfolding inner_real_def by simp

   213 qed

   215 end

   217 instantiation complex :: real_inner

   218 begin

   220 definition inner_complex_def:

   221   "inner x y = Re x * Re y + Im x * Im y"

   223 instance proof

   224   fix x y z :: complex and r :: real

   225   show "inner x y = inner y x"

   226     unfolding inner_complex_def by (simp add: mult_commute)

   227   show "inner (x + y) z = inner x z + inner y z"

   228     unfolding inner_complex_def by (simp add: left_distrib)

   229   show "inner (scaleR r x) y = r * inner x y"

   230     unfolding inner_complex_def by (simp add: right_distrib)

   231   show "0 \<le> inner x x"

   232     unfolding inner_complex_def by simp

   233   show "inner x x = 0 \<longleftrightarrow> x = 0"

   234     unfolding inner_complex_def

   235     by (simp add: add_nonneg_eq_0_iff complex_Re_Im_cancel_iff)

   236   show "norm x = sqrt (inner x x)"

   237     unfolding inner_complex_def complex_norm_def

   238     by (simp add: power2_eq_square)

   239 qed

   241 end

   243 lemma complex_inner_1 [simp]: "inner 1 x = Re x"

   244   unfolding inner_complex_def by simp

   246 lemma complex_inner_1_right [simp]: "inner x 1 = Re x"

   247   unfolding inner_complex_def by simp

   249 lemma complex_inner_ii_left [simp]: "inner ii x = Im x"

   250   unfolding inner_complex_def by simp

   252 lemma complex_inner_ii_right [simp]: "inner x ii = Im x"

   253   unfolding inner_complex_def by simp

   256 subsection {* Gradient derivative *}

   258 definition

   259   gderiv ::

   260     "['a::real_inner \<Rightarrow> real, 'a, 'a] \<Rightarrow> bool"

   261           ("(GDERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60)

   262 where

   263   "GDERIV f x :> D \<longleftrightarrow> FDERIV f x :> (\<lambda>h. inner h D)"

   265 lemma deriv_fderiv: "DERIV f x :> D \<longleftrightarrow> FDERIV f x :> (\<lambda>h. h * D)"

   266   by (simp only: deriv_def field_fderiv_def)

   268 lemma gderiv_deriv [simp]: "GDERIV f x :> D \<longleftrightarrow> DERIV f x :> D"

   269   by (simp only: gderiv_def deriv_fderiv inner_real_def)

   271 lemma GDERIV_DERIV_compose:

   272     "\<lbrakk>GDERIV f x :> df; DERIV g (f x) :> dg\<rbrakk>

   273      \<Longrightarrow> GDERIV (\<lambda>x. g (f x)) x :> scaleR dg df"

   274   unfolding gderiv_def deriv_fderiv

   275   apply (drule (1) FDERIV_compose)

   276   apply (simp add: mult_ac)

   277   done

   279 lemma FDERIV_subst: "\<lbrakk>FDERIV f x :> df; df = d\<rbrakk> \<Longrightarrow> FDERIV f x :> d"

   280   by simp

   282 lemma GDERIV_subst: "\<lbrakk>GDERIV f x :> df; df = d\<rbrakk> \<Longrightarrow> GDERIV f x :> d"

   283   by simp

   285 lemma GDERIV_const: "GDERIV (\<lambda>x. k) x :> 0"

   286   unfolding gderiv_def inner_zero_right by (rule FDERIV_const)

   288 lemma GDERIV_add:

   289     "\<lbrakk>GDERIV f x :> df; GDERIV g x :> dg\<rbrakk>

   290      \<Longrightarrow> GDERIV (\<lambda>x. f x + g x) x :> df + dg"

   291   unfolding gderiv_def inner_add_right by (rule FDERIV_add)

   293 lemma GDERIV_minus:

   294     "GDERIV f x :> df \<Longrightarrow> GDERIV (\<lambda>x. - f x) x :> - df"

   295   unfolding gderiv_def inner_minus_right by (rule FDERIV_minus)

   297 lemma GDERIV_diff:

   298     "\<lbrakk>GDERIV f x :> df; GDERIV g x :> dg\<rbrakk>

   299      \<Longrightarrow> GDERIV (\<lambda>x. f x - g x) x :> df - dg"

   300   unfolding gderiv_def inner_diff_right by (rule FDERIV_diff)

   302 lemma GDERIV_scaleR:

   303     "\<lbrakk>DERIV f x :> df; GDERIV g x :> dg\<rbrakk>

   304      \<Longrightarrow> GDERIV (\<lambda>x. scaleR (f x) (g x)) x

   305       :> (scaleR (f x) dg + scaleR df (g x))"

   306   unfolding gderiv_def deriv_fderiv inner_add_right inner_scaleR_right

   307   apply (rule FDERIV_subst)

   308   apply (erule (1) FDERIV_scaleR)

   309   apply (simp add: mult_ac)

   310   done

   312 lemma GDERIV_mult:

   313     "\<lbrakk>GDERIV f x :> df; GDERIV g x :> dg\<rbrakk>

   314      \<Longrightarrow> GDERIV (\<lambda>x. f x * g x) x :> scaleR (f x) dg + scaleR (g x) df"

   315   unfolding gderiv_def

   316   apply (rule FDERIV_subst)

   317   apply (erule (1) FDERIV_mult)

   318   apply (simp add: inner_add mult_ac)

   319   done

   321 lemma GDERIV_inverse:

   322     "\<lbrakk>GDERIV f x :> df; f x \<noteq> 0\<rbrakk>

   323      \<Longrightarrow> GDERIV (\<lambda>x. inverse (f x)) x :> - (inverse (f x))\<twosuperior> *\<^sub>R df"

   324   apply (erule GDERIV_DERIV_compose)

   325   apply (erule DERIV_inverse [folded numeral_2_eq_2])

   326   done

   328 lemma GDERIV_norm:

   329   assumes "x \<noteq> 0" shows "GDERIV (\<lambda>x. norm x) x :> sgn x"

   330 proof -

   331   have 1: "FDERIV (\<lambda>x. inner x x) x :> (\<lambda>h. inner x h + inner h x)"

   332     by (intro FDERIV_inner FDERIV_ident)

   333   have 2: "(\<lambda>h. inner x h + inner h x) = (\<lambda>h. inner h (scaleR 2 x))"

   334     by (simp add: fun_eq_iff inner_commute)

   335   have "0 < inner x x" using `x \<noteq> 0` by simp

   336   then have 3: "DERIV sqrt (inner x x) :> (inverse (sqrt (inner x x)) / 2)"

   337     by (rule DERIV_real_sqrt)

   338   have 4: "(inverse (sqrt (inner x x)) / 2) *\<^sub>R 2 *\<^sub>R x = sgn x"

   339     by (simp add: sgn_div_norm norm_eq_sqrt_inner)

   340   show ?thesis

   341     unfolding norm_eq_sqrt_inner

   342     apply (rule GDERIV_subst [OF _ 4])

   343     apply (rule GDERIV_DERIV_compose [where g=sqrt and df="scaleR 2 x"])

   344     apply (subst gderiv_def)

   345     apply (rule FDERIV_subst [OF _ 2])

   346     apply (rule 1)

   347     apply (rule 3)

   348     done

   349 qed

   351 lemmas FDERIV_norm = GDERIV_norm [unfolded gderiv_def]

   353 end

author	haftmann
	Sun, 22 Jul 2012 09:56:34 +0200
changeset 49442	571cb1df0768
parent 45773	9ba11d41cd1f
child 50977	a8cc904a6820
permissions	-rw-r--r--