lemmas about linear, bilinear
authorhuffman
Mon Jun 08 14:28:09 2009 -0700 (2009-06-08)
changeset 31529689f5dae1f41
parent 31528 c701f4085ca4
child 31530 e31d63c66f55
lemmas about linear, bilinear
src/HOL/Library/Euclidean_Space.thy
src/HOL/Library/Topology_Euclidean_Space.thy
     1.1 --- a/src/HOL/Library/Euclidean_Space.thy	Mon Jun 08 12:09:43 2009 -0700
     1.2 +++ b/src/HOL/Library/Euclidean_Space.thy	Mon Jun 08 14:28:09 2009 -0700
     1.3 @@ -1828,6 +1828,36 @@
     1.4    then show ?thesis using Kp by blast
     1.5  qed
     1.6  
     1.7 +lemma smult_conv_scaleR: "c *s x = scaleR c x"
     1.8 +  unfolding vector_scalar_mult_def vector_scaleR_def by simp
     1.9 +
    1.10 +lemma linear_conv_bounded_linear:
    1.11 +  fixes f :: "real ^ _ \<Rightarrow> real ^ _"
    1.12 +  shows "linear f \<longleftrightarrow> bounded_linear f"
    1.13 +proof
    1.14 +  assume "linear f"
    1.15 +  show "bounded_linear f"
    1.16 +  proof
    1.17 +    fix x y show "f (x + y) = f x + f y"
    1.18 +      using `linear f` unfolding linear_def by simp
    1.19 +  next
    1.20 +    fix r x show "f (scaleR r x) = scaleR r (f x)"
    1.21 +      using `linear f` unfolding linear_def
    1.22 +      by (simp add: smult_conv_scaleR)
    1.23 +  next
    1.24 +    have "\<exists>B. \<forall>x. norm (f x) \<le> B * norm x"
    1.25 +      using `linear f` by (rule linear_bounded)
    1.26 +    thus "\<exists>K. \<forall>x. norm (f x) \<le> norm x * K"
    1.27 +      by (simp add: mult_commute)
    1.28 +  qed
    1.29 +next
    1.30 +  assume "bounded_linear f"
    1.31 +  then interpret f: bounded_linear f .
    1.32 +  show "linear f"
    1.33 +    unfolding linear_def smult_conv_scaleR
    1.34 +    by (simp add: f.add f.scaleR)
    1.35 +qed
    1.36 +
    1.37  subsection{* Bilinear functions. *}
    1.38  
    1.39  definition "bilinear f \<longleftrightarrow> (\<forall>x. linear(\<lambda>y. f x y)) \<and> (\<forall>y. linear(\<lambda>x. f x y))"
    1.40 @@ -1931,6 +1961,41 @@
    1.41    with Kp show ?thesis by blast
    1.42  qed
    1.43  
    1.44 +lemma bilinear_conv_bounded_bilinear:
    1.45 +  fixes h :: "real ^ _ \<Rightarrow> real ^ _ \<Rightarrow> real ^ _"
    1.46 +  shows "bilinear h \<longleftrightarrow> bounded_bilinear h"
    1.47 +proof
    1.48 +  assume "bilinear h"
    1.49 +  show "bounded_bilinear h"
    1.50 +  proof
    1.51 +    fix x y z show "h (x + y) z = h x z + h y z"
    1.52 +      using `bilinear h` unfolding bilinear_def linear_def by simp
    1.53 +  next
    1.54 +    fix x y z show "h x (y + z) = h x y + h x z"
    1.55 +      using `bilinear h` unfolding bilinear_def linear_def by simp
    1.56 +  next
    1.57 +    fix r x y show "h (scaleR r x) y = scaleR r (h x y)"
    1.58 +      using `bilinear h` unfolding bilinear_def linear_def
    1.59 +      by (simp add: smult_conv_scaleR)
    1.60 +  next
    1.61 +    fix r x y show "h x (scaleR r y) = scaleR r (h x y)"
    1.62 +      using `bilinear h` unfolding bilinear_def linear_def
    1.63 +      by (simp add: smult_conv_scaleR)
    1.64 +  next
    1.65 +    have "\<exists>B. \<forall>x y. norm (h x y) \<le> B * norm x * norm y"
    1.66 +      using `bilinear h` by (rule bilinear_bounded)
    1.67 +    thus "\<exists>K. \<forall>x y. norm (h x y) \<le> norm x * norm y * K"
    1.68 +      by (simp add: mult_ac)
    1.69 +  qed
    1.70 +next
    1.71 +  assume "bounded_bilinear h"
    1.72 +  then interpret h: bounded_bilinear h .
    1.73 +  show "bilinear h"
    1.74 +    unfolding bilinear_def linear_conv_bounded_linear
    1.75 +    using h.bounded_linear_left h.bounded_linear_right
    1.76 +    by simp
    1.77 +qed
    1.78 +
    1.79  subsection{* Adjoints. *}
    1.80  
    1.81  definition "adjoint f = (SOME f'. \<forall>x y. f x \<bullet> y = x \<bullet> f' y)"
     2.1 --- a/src/HOL/Library/Topology_Euclidean_Space.thy	Mon Jun 08 12:09:43 2009 -0700
     2.2 +++ b/src/HOL/Library/Topology_Euclidean_Space.thy	Mon Jun 08 14:28:09 2009 -0700
     2.3 @@ -1241,22 +1241,9 @@
     2.4  lemma Lim_linear: fixes f :: "('a \<Rightarrow> real^'n::finite)" and h :: "(real^'n \<Rightarrow> real^'m::finite)"
     2.5    assumes "(f ---> l) net" "linear h"
     2.6    shows "((\<lambda>x. h (f x)) ---> h l) net"
     2.7 -proof -
     2.8 -  obtain b where b: "b>0" "\<forall>x. norm (h x) \<le> b * norm x"
     2.9 -    using assms(2) using linear_bounded_pos[of h] by auto
    2.10 -  { fix e::real assume "e >0"
    2.11 -    hence "e/b > 0" using `b>0` by (metis divide_pos_pos)
    2.12 -    with `(f ---> l) net` have "eventually (\<lambda>x. dist (f x) l < e/b) net"
    2.13 -      by (rule tendstoD)
    2.14 -    then have "eventually (\<lambda>x. dist (h (f x)) (h l) < e) net"
    2.15 -      apply (rule eventually_rev_mono [rule_format])
    2.16 -      apply (simp add: dist_norm linear_sub [OF `linear h`, symmetric])
    2.17 -      apply (rule le_less_trans [OF b(2) [rule_format]])
    2.18 -      apply (simp add: pos_less_divide_eq `0 < b` mult_commute)
    2.19 -      done
    2.20 -  }
    2.21 -  thus ?thesis unfolding tendsto_iff by simp
    2.22 -qed
    2.23 +using `linear h` `(f ---> l) net`
    2.24 +unfolding linear_conv_bounded_linear
    2.25 +by (rule bounded_linear.tendsto)
    2.26  
    2.27  lemma Lim_const: "((\<lambda>x. a) ---> a) net"
    2.28    by (rule tendsto_const)
    2.29 @@ -1432,76 +1419,15 @@
    2.30    shows "~(trivial_limit net) \<Longrightarrow> (f ---> l) net ==> Lim net f = l"
    2.31    unfolding Lim_def using Lim_unique[of net f] by auto
    2.32  
    2.33 -text{* Limit under bilinear function (surprisingly tedious, but important) *}
    2.34 -
    2.35 -lemma norm_bound_lemma:
    2.36 -  "0 < e \<Longrightarrow> \<exists>d>0. \<forall>(x'::real^'b::finite) y'::real^'a::finite. norm(x' - (x::real^'b)) < d \<and> norm(y' - y) < d \<longrightarrow> norm(x') * norm(y' - y) + norm(x' - x) * norm(y) < e"
    2.37 -proof-
    2.38 -  assume e: "0 < e"
    2.39 -  have th1: "(2 * norm x + 2 * norm y + 2) > 0" using norm_ge_zero[of x] norm_ge_zero[of y] by norm
    2.40 -  hence th0: "0 < e / (2 * norm x + 2 * norm y + 2)"  using `e>0` using divide_pos_pos by auto
    2.41 -  moreover
    2.42 -  { fix x' y'
    2.43 -    assume h: "norm (x' - x) < 1" "norm (x' - x) < e / (2 * norm x + 2 * norm y + 2)"
    2.44 -      "norm (y' - y) < 1" "norm (y' - y) < e / (2 * norm x + 2 * norm y + 2)"
    2.45 -    have th: "\<And>a b (c::real). a \<ge> 0 \<Longrightarrow> c \<ge> 0 \<Longrightarrow> a + (b + c) < e ==> b < e " by arith
    2.46 -    from h have thx: "norm (x' - x) * norm y < e / 2"
    2.47 -      using th0 th1 apply (simp add: field_simps)
    2.48 -      apply (rule th) defer defer apply assumption
    2.49 -      by (simp_all add: norm_ge_zero zero_le_mult_iff)
    2.50 -
    2.51 -    have "norm x' - norm x < 1" apply(rule le_less_trans)
    2.52 -      using h(1) using norm_triangle_ineq2[of x' x] by auto
    2.53 -    hence *:"norm x' < 1 + norm x"  by auto
    2.54 -
    2.55 -    have thy: "norm (y' - y) * norm x' < e / (2 * norm x + 2 * norm y + 2) * (1 + norm x)"
    2.56 -      using mult_strict_mono'[OF h(4) * norm_ge_zero norm_ge_zero] by auto
    2.57 -    also have "\<dots> \<le> e/2" apply simp unfolding divide_le_eq
    2.58 -      using th1 th0 `e>0` by auto
    2.59 -
    2.60 -    finally have "norm x' * norm (y' - y) + norm (x' - x) * norm y < e"
    2.61 -      using thx and e by (simp add: field_simps)  }
    2.62 -  ultimately show ?thesis apply(rule_tac x="min 1 (e / 2 / (norm x + norm y + 1))" in exI) by auto
    2.63 -qed
    2.64 +text{* Limit under bilinear function *}
    2.65  
    2.66  lemma Lim_bilinear:
    2.67    fixes net :: "'a net" and h:: "real ^'m::finite \<Rightarrow> real ^'n::finite \<Rightarrow> real ^'p::finite"
    2.68    assumes "(f ---> l) net" and "(g ---> m) net" and "bilinear h"
    2.69    shows "((\<lambda>x. h (f x) (g x)) ---> (h l m)) net"
    2.70 -proof -
    2.71 -  obtain B where "B>0" and B:"\<forall>x y. norm (h x y) \<le> B * norm x * norm y" using bilinear_bounded_pos[OF assms(3)] by auto
    2.72 -  { fix e::real assume "e>0"
    2.73 -    obtain d where "d>0" and d:"\<forall>x' y'. norm (x' - l) < d \<and> norm (y' - m) < d \<longrightarrow> norm x' * norm (y' - m) + norm (x' - l) * norm m < e / B" using `B>0` `e>0`
    2.74 -      using norm_bound_lemma[of "e / B" l m] using divide_pos_pos by auto
    2.75 -
    2.76 -    have *:"\<And>x y. h (f x) (g x) - h l m = h (f x) (g x - m) + h (f x - l) m"
    2.77 -      unfolding bilinear_rsub[OF assms(3)]
    2.78 -      unfolding bilinear_lsub[OF assms(3)] by auto
    2.79 -
    2.80 -    have "eventually (\<lambda>x. dist (f x) l < d) net"
    2.81 -      using assms(1) `d>0` by (rule tendstoD)
    2.82 -    moreover
    2.83 -    have "eventually (\<lambda>x. dist (g x) m < d) net"
    2.84 -      using assms(2) `d>0` by (rule tendstoD)
    2.85 -    ultimately
    2.86 -    have "eventually (\<lambda>x. dist (f x) l < d \<and> dist (g x) m < d) net"
    2.87 -      by (rule eventually_conjI)
    2.88 -    moreover
    2.89 -    { fix x assume "dist (f x) l < d \<and> dist (g x) m < d"
    2.90 -      hence **:"norm (f x) * norm (g x - m) + norm (f x - l) * norm m < e / B"
    2.91 -	using d[THEN spec[where x="f x"], THEN spec[where x="g x"]] unfolding dist_norm  by auto
    2.92 -      have "norm (h (f x) (g x - m)) + norm (h (f x - l) m) \<le> B * norm (f x) * norm (g x - m) + B * norm (f x - l) * norm m"
    2.93 -	using B[THEN spec[where x="f x"], THEN spec[where x="g x - m"]]
    2.94 -	using B[THEN spec[where x="f x - l"], THEN spec[where x="m"]] by auto
    2.95 -      also have "\<dots> < e" using ** and `B>0` by(auto simp add: field_simps)
    2.96 -      finally have "dist (h (f x) (g x)) (h l m) < e" unfolding dist_norm and * using norm_triangle_lt by auto
    2.97 -    }
    2.98 -    ultimately have "eventually (\<lambda>x. dist (h (f x) (g x)) (h l m) < e) net"
    2.99 -      by (auto elim: eventually_rev_mono)
   2.100 -  }
   2.101 -  thus "((\<lambda>x. h (f x) (g x)) ---> h l m) net"
   2.102 -    unfolding tendsto_iff by simp
   2.103 -qed
   2.104 +using `bilinear h` `(f ---> l) net` `(g ---> m) net`
   2.105 +unfolding bilinear_conv_bounded_bilinear
   2.106 +by (rule bounded_bilinear.tendsto)
   2.107  
   2.108  text{* These are special for limits out of the same vector space. *}
   2.109