--- a/src/HOL/Library/Inner_Product.thy Thu Aug 18 17:42:35 2011 +0200
+++ b/src/HOL/Library/Inner_Product.thy Thu Aug 18 13:36:58 2011 -0700
@@ -5,7 +5,7 @@
header {* Inner Product Spaces and the Gradient Derivative *}
theory Inner_Product
-imports Complex_Main FrechetDeriv
+imports FrechetDeriv
begin
subsection {* Real inner product spaces *}
@@ -43,6 +43,9 @@
lemma inner_diff_left: "inner (x - y) z = inner x z - inner y z"
by (simp add: diff_minus inner_add_left)
+lemma inner_setsum_left: "inner (\<Sum>x\<in>A. f x) y = (\<Sum>x\<in>A. inner (f x) y)"
+ by (cases "finite A", induct set: finite, simp_all add: inner_add_left)
+
text {* Transfer distributivity rules to right argument. *}
lemma inner_add_right: "inner x (y + z) = inner x y + inner x z"
@@ -60,6 +63,9 @@
lemma inner_diff_right: "inner x (y - z) = inner x y - inner x z"
using inner_diff_left [of y z x] by (simp only: inner_commute)
+lemma inner_setsum_right: "inner x (\<Sum>y\<in>A. f y) = (\<Sum>y\<in>A. inner x (f y))"
+ using inner_setsum_left [of f A x] by (simp only: inner_commute)
+
lemmas inner_add [algebra_simps] = inner_add_left inner_add_right
lemmas inner_diff [algebra_simps] = inner_diff_left inner_diff_right
lemmas inner_scaleR = inner_scaleR_left inner_scaleR_right
@@ -148,8 +154,8 @@
setup {* Sign.add_const_constraint
(@{const_name norm}, SOME @{typ "'a::real_normed_vector \<Rightarrow> real"}) *}
-interpretation inner:
- bounded_bilinear "inner::'a::real_inner \<Rightarrow> 'a \<Rightarrow> real"
+lemma bounded_bilinear_inner:
+ "bounded_bilinear (inner::'a::real_inner \<Rightarrow> 'a \<Rightarrow> real)"
proof
fix x y z :: 'a and r :: real
show "inner (x + y) z = inner x z + inner y z"
@@ -167,15 +173,20 @@
qed
qed
-interpretation inner_left:
- bounded_linear "\<lambda>x::'a::real_inner. inner x y"
- by (rule inner.bounded_linear_left)
+lemmas tendsto_inner [tendsto_intros] =
+ bounded_bilinear.tendsto [OF bounded_bilinear_inner]
+
+lemmas isCont_inner [simp] =
+ bounded_bilinear.isCont [OF bounded_bilinear_inner]
-interpretation inner_right:
- bounded_linear "\<lambda>y::'a::real_inner. inner x y"
- by (rule inner.bounded_linear_right)
+lemmas FDERIV_inner =
+ bounded_bilinear.FDERIV [OF bounded_bilinear_inner]
-declare inner.isCont [simp]
+lemmas bounded_linear_inner_left =
+ bounded_bilinear.bounded_linear_left [OF bounded_bilinear_inner]
+
+lemmas bounded_linear_inner_right =
+ bounded_bilinear.bounded_linear_right [OF bounded_bilinear_inner]
subsection {* Class instances *}
@@ -260,29 +271,29 @@
by simp
lemma GDERIV_const: "GDERIV (\<lambda>x. k) x :> 0"
- unfolding gderiv_def inner_right.zero by (rule FDERIV_const)
+ unfolding gderiv_def inner_zero_right by (rule FDERIV_const)
lemma GDERIV_add:
"\<lbrakk>GDERIV f x :> df; GDERIV g x :> dg\<rbrakk>
\<Longrightarrow> GDERIV (\<lambda>x. f x + g x) x :> df + dg"
- unfolding gderiv_def inner_right.add by (rule FDERIV_add)
+ unfolding gderiv_def inner_add_right by (rule FDERIV_add)
lemma GDERIV_minus:
"GDERIV f x :> df \<Longrightarrow> GDERIV (\<lambda>x. - f x) x :> - df"
- unfolding gderiv_def inner_right.minus by (rule FDERIV_minus)
+ unfolding gderiv_def inner_minus_right by (rule FDERIV_minus)
lemma GDERIV_diff:
"\<lbrakk>GDERIV f x :> df; GDERIV g x :> dg\<rbrakk>
\<Longrightarrow> GDERIV (\<lambda>x. f x - g x) x :> df - dg"
- unfolding gderiv_def inner_right.diff by (rule FDERIV_diff)
+ unfolding gderiv_def inner_diff_right by (rule FDERIV_diff)
lemma GDERIV_scaleR:
"\<lbrakk>DERIV f x :> df; GDERIV g x :> dg\<rbrakk>
\<Longrightarrow> GDERIV (\<lambda>x. scaleR (f x) (g x)) x
:> (scaleR (f x) dg + scaleR df (g x))"
- unfolding gderiv_def deriv_fderiv inner_right.add inner_right.scaleR
+ unfolding gderiv_def deriv_fderiv inner_add_right inner_scaleR_right
apply (rule FDERIV_subst)
- apply (erule (1) scaleR.FDERIV)
+ apply (erule (1) FDERIV_scaleR)
apply (simp add: mult_ac)
done
@@ -306,7 +317,7 @@
assumes "x \<noteq> 0" shows "GDERIV (\<lambda>x. norm x) x :> sgn x"
proof -
have 1: "FDERIV (\<lambda>x. inner x x) x :> (\<lambda>h. inner x h + inner h x)"
- by (intro inner.FDERIV FDERIV_ident)
+ by (intro FDERIV_inner FDERIV_ident)
have 2: "(\<lambda>h. inner x h + inner h x) = (\<lambda>h. inner h (scaleR 2 x))"
by (simp add: fun_eq_iff inner_commute)
have "0 < inner x x" using `x \<noteq> 0` by simp