src/HOL/Real_Vector_Spaces.thy
changeset 60026 41d81b4a0a21
parent 60017 b785d6d06430
child 60155 91477b3a2d6b
     1.1 --- a/src/HOL/Real_Vector_Spaces.thy	Sun Apr 12 00:26:24 2015 +0200
     1.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Sun Apr 12 11:00:56 2015 +0100
     1.3 @@ -405,7 +405,7 @@
     1.4  apply (rule of_real_inverse [symmetric])
     1.5  done
     1.6  
     1.7 -lemma Reals_inverse_iff [simp]: 
     1.8 +lemma Reals_inverse_iff [simp]:
     1.9    fixes x:: "'a :: {real_div_algebra, division_ring}"
    1.10    shows "inverse x \<in> \<real> \<longleftrightarrow> x \<in> \<real>"
    1.11  by (metis Reals_inverse inverse_inverse_eq)
    1.12 @@ -454,7 +454,7 @@
    1.13      by (metis Reals_0 setsum.infinite)
    1.14  qed
    1.15  
    1.16 -lemma setprod_in_Reals [intro,simp]: 
    1.17 +lemma setprod_in_Reals [intro,simp]:
    1.18    assumes "\<And>i. i \<in> s \<Longrightarrow> f i \<in> \<real>" shows "setprod f s \<in> \<real>"
    1.19  proof (cases "finite s")
    1.20    case True then show ?thesis using assms
    1.21 @@ -640,7 +640,7 @@
    1.22  
    1.23  lemma norm_ge_zero [simp]: "0 \<le> norm x"
    1.24  proof -
    1.25 -  have "0 = norm (x + -1 *\<^sub>R x)" 
    1.26 +  have "0 = norm (x + -1 *\<^sub>R x)"
    1.27      using scaleR_add_left[of 1 "-1" x] norm_scaleR[of 0 x] by (simp add: scaleR_one)
    1.28    also have "\<dots> \<le> norm x + norm (-1 *\<^sub>R x)" by (rule norm_triangle_ineq)
    1.29    finally show ?thesis by simp
    1.30 @@ -756,7 +756,7 @@
    1.31    finally show ?thesis .
    1.32  qed
    1.33  
    1.34 -lemma norm_triangle_mono: 
    1.35 +lemma norm_triangle_mono:
    1.36    fixes a b :: "'a::real_normed_vector"
    1.37    shows "\<lbrakk>norm a \<le> r; norm b \<le> s\<rbrakk> \<Longrightarrow> norm (a + b) \<le> r + s"
    1.38  by (metis add_mono_thms_linordered_semiring(1) norm_triangle_ineq order.trans)
    1.39 @@ -876,7 +876,7 @@
    1.40    shows "setprod (\<lambda>x. norm(f x)) A = norm (setprod f A)"
    1.41    by (induct A rule: infinite_finite_induct) (auto simp: norm_mult)
    1.42  
    1.43 -lemma norm_setprod_le: 
    1.44 +lemma norm_setprod_le:
    1.45    "norm (setprod f A) \<le> (\<Prod>a\<in>A. norm (f a :: 'a :: {real_normed_algebra_1, comm_monoid_mult}))"
    1.46  proof (induction A rule: infinite_finite_induct)
    1.47    case (insert a A)
    1.48 @@ -891,7 +891,7 @@
    1.49  lemma norm_setprod_diff:
    1.50    fixes z w :: "'i \<Rightarrow> 'a::{real_normed_algebra_1, comm_monoid_mult}"
    1.51    shows "(\<And>i. i \<in> I \<Longrightarrow> norm (z i) \<le> 1) \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> norm (w i) \<le> 1) \<Longrightarrow>
    1.52 -    norm ((\<Prod>i\<in>I. z i) - (\<Prod>i\<in>I. w i)) \<le> (\<Sum>i\<in>I. norm (z i - w i))" 
    1.53 +    norm ((\<Prod>i\<in>I. z i) - (\<Prod>i\<in>I. w i)) \<le> (\<Sum>i\<in>I. norm (z i - w i))"
    1.54  proof (induction I rule: infinite_finite_induct)
    1.55    case (insert i I)
    1.56    note insert.hyps[simp]
    1.57 @@ -918,7 +918,7 @@
    1.58      by (auto simp add: ac_simps mult_right_mono mult_left_mono)
    1.59  qed simp_all
    1.60  
    1.61 -lemma norm_power_diff: 
    1.62 +lemma norm_power_diff:
    1.63    fixes z w :: "'a::{real_normed_algebra_1, comm_monoid_mult}"
    1.64    assumes "norm z \<le> 1" "norm w \<le> 1"
    1.65    shows "norm (z^m - w^m) \<le> m * norm (z - w)"
    1.66 @@ -1025,7 +1025,7 @@
    1.67  
    1.68  subclass first_countable_topology
    1.69  proof
    1.70 -  fix x 
    1.71 +  fix x
    1.72    show "\<exists>A::nat \<Rightarrow> 'a set. (\<forall>i. x \<in> A i \<and> open (A i)) \<and> (\<forall>S. open S \<and> x \<in> S \<longrightarrow> (\<exists>i. A i \<subseteq> S))"
    1.73    proof (safe intro!: exI[of _ "\<lambda>n. {y. dist x y < inverse (Suc n)}"])
    1.74      fix S assume "open S" "x \<in> S"
    1.75 @@ -1202,13 +1202,13 @@
    1.76  
    1.77  lemma zero_le_sgn_iff [simp]: "0 \<le> sgn x \<longleftrightarrow> 0 \<le> (x::real)"
    1.78    by (cases "0::real" x rule: linorder_cases) simp_all
    1.79 -  
    1.80 +
    1.81  lemma zero_less_sgn_iff [simp]: "0 < sgn x \<longleftrightarrow> 0 < (x::real)"
    1.82    by (cases "0::real" x rule: linorder_cases) simp_all
    1.83  
    1.84  lemma sgn_le_0_iff [simp]: "sgn x \<le> 0 \<longleftrightarrow> (x::real) \<le> 0"
    1.85    by (cases "0::real" x rule: linorder_cases) simp_all
    1.86 -  
    1.87 +
    1.88  lemma sgn_less_0_iff [simp]: "sgn x < 0 \<longleftrightarrow> (x::real) < 0"
    1.89    by (cases "0::real" x rule: linorder_cases) simp_all
    1.90  
    1.91 @@ -1547,6 +1547,8 @@
    1.92  lemma lim_sequentially: "X ----> (L::'a::metric_space) \<longleftrightarrow> (\<forall>r>0. \<exists>no. \<forall>n\<ge>no. dist (X n) L < r)"
    1.93    unfolding tendsto_iff eventually_sequentially ..
    1.94  
    1.95 +lemmas LIMSEQ_def = lim_sequentially  (*legacy binding*)
    1.96 +
    1.97  lemma LIMSEQ_iff_nz: "X ----> (L::'a::metric_space) = (\<forall>r>0. \<exists>no>0. \<forall>n\<ge>no. dist (X n) L < r)"
    1.98    unfolding lim_sequentially by (metis Suc_leD zero_less_Suc)
    1.99  
   1.100 @@ -1729,7 +1731,7 @@
   1.101    also have "\<dots> < x" using N by simp
   1.102    finally have "y \<le> x"
   1.103      by (rule order_less_imp_le) }
   1.104 -  note bound_isUb = this 
   1.105 +  note bound_isUb = this
   1.106  
   1.107    obtain N where "\<forall>m\<ge>N. \<forall>n\<ge>N. dist (X m) (X n) < 1"
   1.108      using X[THEN metric_CauchyD, OF zero_less_one] by auto