# HG changeset patch
# User huffman
# Date 1163115960 -3600
# Node ID dd647b4d79521114cf1f8050294166bc47dc0772
# Parent  0767e7dad5499df4846c94f7bfd1799318aced5a
added bounded_linear and bounded_bilinear locales

diff -r 0767e7dad549 -r dd647b4d7952 src/HOL/Hyperreal/Lim.thy
--- a/src/HOL/Hyperreal/Lim.thy	Fri Nov 10 00:13:35 2006 +0100
+++ b/src/HOL/Hyperreal/Lim.thy	Fri Nov 10 00:46:00 2006 +0100
@@ -219,6 +219,17 @@
    \<Longrightarrow> (f -- a --> l) = (g -- b --> m)"
 by (simp add: LIM_def)
 
+lemma LIM_equal2:
+  assumes 1: "0 < R"
+  assumes 2: "\<And>x. \<lbrakk>x \<noteq> a; norm (x - a) < R\<rbrakk> \<Longrightarrow> f x = g x"
+  shows "g -- a --> l \<Longrightarrow> f -- a --> l"
+apply (unfold LIM_def, safe)
+apply (drule_tac x="r" in spec, safe)
+apply (rule_tac x="min s R" in exI, safe)
+apply (simp add: 1)
+apply (simp add: 2)
+done
+
 text{*Two uses in Hyperreal/Transcendental.ML*}
 lemma LIM_trans:
      "[| (%x. f(x) + -g(x)) -- a --> 0;  g -- a --> l |] ==> f -- a --> l"
@@ -253,6 +264,225 @@
 lemma LIM_o: "\<lbrakk>g -- l --> g l; f -- a --> l\<rbrakk> \<Longrightarrow> (g \<circ> f) -- a --> g l"
 unfolding o_def by (rule LIM_compose)
 
+lemma real_LIM_sandwich_zero:
+  fixes f g :: "'a::real_normed_vector \<Rightarrow> real"
+  assumes f: "f -- a --> 0"
+  assumes 1: "\<And>x. x \<noteq> a \<Longrightarrow> 0 \<le> g x"
+  assumes 2: "\<And>x. x \<noteq> a \<Longrightarrow> g x \<le> f x"
+  shows "g -- a --> 0"
+proof (rule LIM_imp_LIM [OF f])
+  fix x assume x: "x \<noteq> a"
+  have "norm (g x - 0) = g x" by (simp add: 1 x)
+  also have "g x \<le> f x" by (rule 2 [OF x])
+  also have "f x \<le> \<bar>f x\<bar>" by (rule abs_ge_self)
+  also have "\<bar>f x\<bar> = norm (f x - 0)" by simp
+  finally show "norm (g x - 0) \<le> norm (f x - 0)" .
+qed
+
+subsubsection {* Bounded Linear Operators *}
+
+locale bounded_linear = additive +
+  constrains f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
+  assumes scaleR: "f (scaleR r x) = scaleR r (f x)"
+  assumes bounded: "\<exists>K. \<forall>x. norm (f x) \<le> norm x * K"
+
+lemma (in bounded_linear) pos_bounded:
+  "\<exists>K>0. \<forall>x. norm (f x) \<le> norm x * K"
+apply (cut_tac bounded, erule exE)
+apply (rule_tac x="max 1 K" in exI, safe)
+apply (rule order_less_le_trans [OF zero_less_one le_maxI1])
+apply (drule spec, erule order_trans)
+apply (rule mult_left_mono [OF le_maxI2 norm_ge_zero])
+done
+
+lemma (in bounded_linear) pos_boundedE:
+  obtains K where "0 < K" and "\<forall>x. norm (f x) \<le> norm x * K"
+  using pos_bounded by fast
+
+lemma (in bounded_linear) cont: "f -- a --> f a"
+proof (rule LIM_I)
+  fix r::real assume r: "0 < r"
+  obtain K where K: "0 < K" and norm_le: "\<And>x. norm (f x) \<le> norm x * K"
+    using pos_bounded by fast
+  show "\<exists>s>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < s \<longrightarrow> norm (f x - f a) < r"
+  proof (rule exI, safe)
+    from r K show "0 < r / K" by (rule divide_pos_pos)
+  next
+    fix x assume x: "norm (x - a) < r / K"
+    have "norm (f x - f a) = norm (f (x - a))" by (simp only: diff)
+    also have "\<dots> \<le> norm (x - a) * K" by (rule norm_le)
+    also from K x have "\<dots> < r" by (simp only: pos_less_divide_eq)
+    finally show "norm (f x - f a) < r" .
+  qed
+qed
+
+lemma (in bounded_linear) LIM:
+  "g -- a --> l \<Longrightarrow> (\<lambda>x. f (g x)) -- a --> f l"
+by (rule LIM_compose [OF cont])
+
+lemma (in bounded_linear) LIM_zero:
+  "g -- a --> 0 \<Longrightarrow> (\<lambda>x. f (g x)) -- a --> 0"
+by (drule LIM, simp only: zero)
+
+subsubsection {* Bounded Bilinear Operators *}
+
+locale bounded_bilinear =
+  fixes prod :: "['a::real_normed_vector, 'b::real_normed_vector]
+                 \<Rightarrow> 'c::real_normed_vector"
+    (infixl "**" 70)
+  assumes add_left: "prod (a + a') b = prod a b + prod a' b"
+  assumes add_right: "prod a (b + b') = prod a b + prod a b'"
+  assumes scaleR_left: "prod (scaleR r a) b = scaleR r (prod a b)"
+  assumes scaleR_right: "prod a (scaleR r b) = scaleR r (prod a b)"
+  assumes bounded: "\<exists>K. \<forall>a b. norm (prod a b) \<le> norm a * norm b * K"
+
+lemma (in bounded_bilinear) pos_bounded:
+  "\<exists>K>0. \<forall>a b. norm (a ** b) \<le> norm a * norm b * K"
+apply (cut_tac bounded, erule exE)
+apply (rule_tac x="max 1 K" in exI, safe)
+apply (rule order_less_le_trans [OF zero_less_one le_maxI1])
+apply (drule spec, drule spec, erule order_trans)
+apply (rule mult_left_mono [OF le_maxI2])
+apply (intro mult_nonneg_nonneg norm_ge_zero)
+done
+
+lemma (in bounded_bilinear) additive_right: "additive (\<lambda>b. prod a b)"
+by (rule additive.intro, rule add_right)
+
+lemma (in bounded_bilinear) additive_left: "additive (\<lambda>a. prod a b)"
+by (rule additive.intro, rule add_left)
+
+lemma (in bounded_bilinear) zero_left: "prod 0 b = 0"
+by (rule additive.zero [OF additive_left])
+
+lemma (in bounded_bilinear) zero_right: "prod a 0 = 0"
+by (rule additive.zero [OF additive_right])
+
+lemma (in bounded_bilinear) minus_left: "prod (- a) b = - prod a b"
+by (rule additive.minus [OF additive_left])
+
+lemma (in bounded_bilinear) minus_right: "prod a (- b) = - prod a b"
+by (rule additive.minus [OF additive_right])
+
+lemma (in bounded_bilinear) diff_left:
+  "prod (a - a') b = prod a b - prod a' b"
+by (rule additive.diff [OF additive_left])
+
+lemma (in bounded_bilinear) diff_right:
+  "prod a (b - b') = prod a b - prod a b'"
+by (rule additive.diff [OF additive_right])
+
+lemma (in bounded_bilinear) LIM_prod_zero:
+  assumes f: "f -- a --> 0"
+  assumes g: "g -- a --> 0"
+  shows "(\<lambda>x. f x ** g x) -- a --> 0"
+proof (rule LIM_I)
+  fix r::real assume r: "0 < r"
+  obtain K where K: "0 < K"
+    and norm_le: "\<And>x y. norm (x ** y) \<le> norm x * norm y * K"
+    using pos_bounded by fast
+  from K have K': "0 < inverse K"
+    by (rule positive_imp_inverse_positive)
+  obtain s where s: "0 < s"
+    and norm_f: "\<And>x. \<lbrakk>x \<noteq> a; norm (x - a) < s\<rbrakk> \<Longrightarrow> norm (f x) < r"
+    using LIM_D [OF f r] by auto
+  obtain t where t: "0 < t"
+    and norm_g: "\<And>x. \<lbrakk>x \<noteq> a; norm (x - a) < t\<rbrakk> \<Longrightarrow> norm (g x) < inverse K"
+    using LIM_D [OF g K'] by auto
+  show "\<exists>s>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < s \<longrightarrow> norm (f x ** g x - 0) < r"
+  proof (rule exI, safe)
+    from s t show "0 < min s t" by simp
+  next
+    fix x assume x: "x \<noteq> a"
+    assume "norm (x - a) < min s t"
+    hence xs: "norm (x - a) < s" and xt: "norm (x - a) < t" by simp_all
+    from x xs have 1: "norm (f x) < r" by (rule norm_f)
+    from x xt have 2: "norm (g x) < inverse K" by (rule norm_g)
+    have "norm (f x ** g x) \<le> norm (f x) * norm (g x) * K" by (rule norm_le)
+    also from 1 2 K have "\<dots> < r * inverse K * K"
+      by (intro mult_strict_right_mono mult_strict_mono' norm_ge_zero)
+    also from K have "r * inverse K * K = r" by simp
+    finally show "norm (f x ** g x - 0) < r" by simp
+  qed
+qed
+
+lemma (in bounded_bilinear) bounded_linear_left:
+  "bounded_linear (\<lambda>a. a ** b)"
+apply (unfold_locales)
+apply (rule add_left)
+apply (rule scaleR_left)
+apply (cut_tac bounded, safe)
+apply (rule_tac x="norm b * K" in exI)
+apply (simp add: mult_ac)
+done
+
+lemma (in bounded_bilinear) bounded_linear_right:
+  "bounded_linear (\<lambda>b. a ** b)"
+apply (unfold_locales)
+apply (rule add_right)
+apply (rule scaleR_right)
+apply (cut_tac bounded, safe)
+apply (rule_tac x="norm a * K" in exI)
+apply (simp add: mult_ac)
+done
+
+lemma (in bounded_bilinear) LIM_left_zero:
+  "f -- a --> 0 \<Longrightarrow> (\<lambda>x. f x ** c) -- a --> 0"
+by (rule bounded_linear.LIM_zero [OF bounded_linear_left])
+
+lemma (in bounded_bilinear) LIM_right_zero:
+  "f -- a --> 0 \<Longrightarrow> (\<lambda>x. c ** f x) -- a --> 0"
+by (rule bounded_linear.LIM_zero [OF bounded_linear_right])
+
+lemma (in bounded_bilinear) prod_diff_prod:
+  "(x ** y - a ** b) = (x - a) ** (y - b) + (x - a) ** b + a ** (y - b)"
+by (simp add: diff_left diff_right)
+
+lemma (in bounded_bilinear) LIM:
+  "\<lbrakk>f -- a --> L; g -- a --> M\<rbrakk> \<Longrightarrow> (\<lambda>x. f x ** g x) -- a --> L ** M"
+apply (drule LIM_zero)
+apply (drule LIM_zero)
+apply (rule LIM_zero_cancel)
+apply (subst prod_diff_prod)
+apply (rule LIM_add_zero)
+apply (rule LIM_add_zero)
+apply (erule (1) LIM_prod_zero)
+apply (erule LIM_left_zero)
+apply (erule LIM_right_zero)
+done
+
+interpretation bounded_bilinear_mult:
+  bounded_bilinear ["op * :: 'a \<Rightarrow> 'a \<Rightarrow> 'a::real_normed_algebra"]
+apply (rule bounded_bilinear.intro)
+apply (rule left_distrib)
+apply (rule right_distrib)
+apply (rule mult_scaleR_left)
+apply (rule mult_scaleR_right)
+apply (rule_tac x="1" in exI)
+apply (simp add: norm_mult_ineq)
+done
+
+interpretation bounded_bilinear_scaleR:
+  bounded_bilinear ["scaleR"]
+apply (rule bounded_bilinear.intro)
+apply (rule scaleR_left_distrib)
+apply (rule scaleR_right_distrib)
+apply (simp add: real_scaleR_def)
+apply (rule scaleR_left_commute)
+apply (rule_tac x="1" in exI)
+apply (simp add: norm_scaleR)
+done
+
+lemmas LIM_mult = bounded_bilinear_mult.LIM
+
+lemmas LIM_mult_zero = bounded_bilinear_mult.LIM_prod_zero
+
+lemmas LIM_mult_left_zero = bounded_bilinear_mult.LIM_left_zero
+
+lemmas LIM_mult_right_zero = bounded_bilinear_mult.LIM_right_zero
+
+lemmas LIM_scaleR = bounded_bilinear_scaleR.LIM
+
 subsubsection {* Purely nonstandard proofs *}
 
 lemma NSLIM_I:
@@ -478,39 +708,48 @@
 by (simp add: isCont_def LIM_isCont_iff)
 
 lemma isCont_Id: "isCont (\<lambda>x. x) a"
-unfolding isCont_def by (rule LIM_self)
+  unfolding isCont_def by (rule LIM_self)
 
 lemma isCont_const [simp]: "isCont (%x. k) a"
-unfolding isCont_def by (rule LIM_const)
+  unfolding isCont_def by (rule LIM_const)
 
 lemma isCont_add: "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x + g x) a"
-unfolding isCont_def by (rule LIM_add)
+  unfolding isCont_def by (rule LIM_add)
 
 lemma isCont_minus: "isCont f a \<Longrightarrow> isCont (\<lambda>x. - f x) a"
-unfolding isCont_def by (rule LIM_minus)
+  unfolding isCont_def by (rule LIM_minus)
 
 lemma isCont_diff: "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x - g x) a"
-unfolding isCont_def by (rule LIM_diff)
+  unfolding isCont_def by (rule LIM_diff)
 
 lemma isCont_mult:
   fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_algebra"
   shows "[| isCont f a; isCont g a |] ==> isCont (%x. f(x) * g(x)) a"
-unfolding isCont_def by (rule LIM_mult2)
+  unfolding isCont_def by (rule LIM_mult)
 
 lemma isCont_inverse:
   fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_div_algebra"
   shows "[| isCont f x; f x \<noteq> 0 |] ==> isCont (%x. inverse (f x)) x"
-unfolding isCont_def by (rule LIM_inverse)
+  unfolding isCont_def by (rule LIM_inverse)
 
 lemma isCont_LIM_compose:
   "\<lbrakk>isCont g l; f -- a --> l\<rbrakk> \<Longrightarrow> (\<lambda>x. g (f x)) -- a --> g l"
-unfolding isCont_def by (rule LIM_compose)
+  unfolding isCont_def by (rule LIM_compose)
 
 lemma isCont_o2: "\<lbrakk>isCont f a; isCont g (f a)\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. g (f x)) a"
-unfolding isCont_def by (rule LIM_compose)
+  unfolding isCont_def by (rule LIM_compose)
 
 lemma isCont_o: "\<lbrakk>isCont f a; isCont g (f a)\<rbrakk> \<Longrightarrow> isCont (g o f) a"
-unfolding o_def by (rule isCont_o2)
+  unfolding o_def by (rule isCont_o2)
+
+lemma (in bounded_linear) isCont: "isCont f a"
+  unfolding isCont_def by (rule cont)
+
+lemma (in bounded_bilinear) isCont:
+  "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x ** g x) a"
+  unfolding isCont_def by (rule LIM)
+
+lemmas isCont_scaleR = bounded_bilinear_scaleR.isCont
 
 subsubsection {* Nonstandard proofs *}