# HG changeset patch
# User eberlm
# Date 1446129652 -3600
# Node ID f2e51e704a962fbdb3f62b28a11c73eabc62d97f
# Parent  9ad1fccbba965e77e817f7fbd5fdb5986a79ac06
added many small lemmas about setsum/setprod/powr/...

diff -r 9ad1fccbba96 -r f2e51e704a96 src/HOL/Groups_Big.thy
--- a/src/HOL/Groups_Big.thy	Tue Oct 27 23:18:32 2015 +0100
+++ b/src/HOL/Groups_Big.thy	Thu Oct 29 15:40:52 2015 +0100
@@ -930,6 +930,14 @@
   finally show ?thesis .
 qed
 
+lemma setsum_cong_Suc:
+  assumes "0 \<notin> A" "\<And>x. Suc x \<in> A \<Longrightarrow> f (Suc x) = g (Suc x)"
+  shows   "setsum f A = setsum g A"
+proof (rule setsum.cong)
+  fix x assume "x \<in> A"
+  with assms(1) show "f x = g x" by (cases x) (auto intro!: assms(2))
+qed simp_all
+
 
 subsubsection \<open>Cardinality as special case of @{const setsum}\<close>
 
diff -r 9ad1fccbba96 -r f2e51e704a96 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Tue Oct 27 23:18:32 2015 +0100
+++ b/src/HOL/Int.thy	Thu Oct 29 15:40:52 2015 +0100
@@ -724,8 +724,36 @@
   "q \<in> \<int> \<Longrightarrow> (\<And>z. P (of_int z)) \<Longrightarrow> P q"
   by (rule Ints_cases) auto
 
+lemma Nats_subset_Ints: "\<nat> \<subseteq> \<int>"
+  unfolding Nats_def Ints_def
+  by (rule subsetI, elim imageE, hypsubst, subst of_int_of_nat_eq[symmetric], rule imageI) simp_all
+
+lemma Nats_altdef1: "\<nat> = {of_int n |n. n \<ge> 0}"
+proof (intro subsetI equalityI)
+  fix x :: 'a assume "x \<in> {of_int n |n. n \<ge> 0}"
+  then obtain n where "x = of_int n" "n \<ge> 0" by (auto elim!: Ints_cases)
+  hence "x = of_nat (nat n)" by (subst of_nat_nat) simp_all
+  thus "x \<in> \<nat>" by simp
+next
+  fix x :: 'a assume "x \<in> \<nat>"
+  then obtain n where "x = of_nat n" by (auto elim!: Nats_cases)
+  hence "x = of_int (int n)" by simp
+  also have "int n \<ge> 0" by simp
+  hence "of_int (int n) \<in> {of_int n |n. n \<ge> 0}" by blast
+  finally show "x \<in> {of_int n |n. n \<ge> 0}" .
+qed
+
 end
 
+lemma (in linordered_idom) Nats_altdef2: "\<nat> = {n \<in> \<int>. n \<ge> 0}"
+proof (intro subsetI equalityI)
+  fix x :: 'a assume "x \<in> {n \<in> \<int>. n \<ge> 0}"
+  then obtain n where "x = of_int n" "n \<ge> 0" by (auto elim!: Ints_cases)
+  hence "x = of_nat (nat n)" by (subst of_nat_nat) simp_all
+  thus "x \<in> \<nat>" by simp
+qed (auto elim!: Nats_cases)
+
+
 text \<open>The premise involving @{term Ints} prevents @{term "a = 1/2"}.\<close>
 
 lemma Ints_double_eq_0_iff:
diff -r 9ad1fccbba96 -r f2e51e704a96 src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Tue Oct 27 23:18:32 2015 +0100
+++ b/src/HOL/Limits.thy	Thu Oct 29 15:40:52 2015 +0100
@@ -1436,6 +1436,39 @@
   using tendsto_mult [OF tendsto_const LIMSEQ_inverse_real_of_nat_add_minus [of 1]]
   by auto
 
+lemma lim_1_over_n: "((\<lambda>n. 1 / of_nat n) ---> (0::'a::real_normed_field)) sequentially"
+proof (subst lim_sequentially, intro allI impI exI)
+  fix e :: real assume e: "e > 0"
+  fix n :: nat assume n: "n \<ge> nat \<lceil>inverse e + 1\<rceil>"
+  have "inverse e < of_nat (nat \<lceil>inverse e + 1\<rceil>)" by linarith
+  also note n
+  finally show "dist (1 / of_nat n :: 'a) 0 < e" using e 
+    by (simp add: divide_simps mult.commute norm_conv_dist[symmetric] norm_divide)
+qed
+
+lemma lim_inverse_n: "((\<lambda>n. inverse(of_nat n)) ---> (0::'a::real_normed_field)) sequentially"
+  using lim_1_over_n by (simp add: inverse_eq_divide)
+
+lemma LIMSEQ_Suc_n_over_n: "(\<lambda>n. of_nat (Suc n) / of_nat n :: 'a :: real_normed_field) ----> 1"
+proof (rule Lim_transform_eventually)
+  show "eventually (\<lambda>n. 1 + inverse (of_nat n :: 'a) = of_nat (Suc n) / of_nat n) sequentially"
+    using eventually_gt_at_top[of "0::nat"] by eventually_elim (simp add: field_simps)
+  have "(\<lambda>n. 1 + inverse (of_nat n) :: 'a) ----> 1 + 0"
+    by (intro tendsto_add tendsto_const lim_inverse_n)
+  thus "(\<lambda>n. 1 + inverse (of_nat n) :: 'a) ----> 1" by simp
+qed
+
+lemma LIMSEQ_n_over_Suc_n: "(\<lambda>n. of_nat n / of_nat (Suc n) :: 'a :: real_normed_field) ----> 1"
+proof (rule Lim_transform_eventually)
+  show "eventually (\<lambda>n. inverse (of_nat (Suc n) / of_nat n :: 'a) = 
+                        of_nat n / of_nat (Suc n)) sequentially"
+    using eventually_gt_at_top[of "0::nat"] 
+    by eventually_elim (simp add: field_simps del: of_nat_Suc)
+  have "(\<lambda>n. inverse (of_nat (Suc n) / of_nat n :: 'a)) ----> inverse 1"
+    by (intro tendsto_inverse LIMSEQ_Suc_n_over_n) simp_all
+  thus "(\<lambda>n. inverse (of_nat (Suc n) / of_nat n :: 'a)) ----> 1" by simp
+qed
+
 subsection \<open>Convergence on sequences\<close>
 
 lemma convergent_add:
diff -r 9ad1fccbba96 -r f2e51e704a96 src/HOL/Multivariate_Analysis/Complex_Transcendental.thy
--- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Tue Oct 27 23:18:32 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Thu Oct 29 15:40:52 2015 +0100
@@ -977,7 +977,6 @@
   apply (auto simp: exp_of_nat_mult [symmetric])
   done
 
-
 subsection\<open>The Unwinding Number and the Ln-product Formula\<close>
 
 text\<open>Note that in this special case the unwinding number is -1, 0 or 1.\<close>
@@ -1262,6 +1261,21 @@
         Im_Ln_eq_pi [of z] Im_Ln_pos_lt [of z] Re_Ln_pos_le [of z]
   by (auto simp: of_real_numeral Ln_times)
 
+lemma Ln_of_nat: "0 < n \<Longrightarrow> Ln (of_nat n) = of_real (ln (of_nat n))"
+  by (subst of_real_of_nat_eq[symmetric], subst Ln_of_real[symmetric]) simp_all
+
+lemma Ln_of_nat_over_of_nat: 
+  assumes "m > 0" "n > 0"
+  shows   "Ln (of_nat m / of_nat n) = of_real (ln (of_nat m) - ln (of_nat n))"
+proof -
+  have "of_nat m / of_nat n = (of_real (of_nat m / of_nat n) :: complex)" by simp
+  also from assms have "Ln ... = of_real (ln (of_nat m / of_nat n))"
+    by (simp add: Ln_of_real[symmetric])
+  also from assms have "... = of_real (ln (of_nat m) - ln (of_nat n))"
+    by (simp add: ln_div)
+  finally show ?thesis .
+qed
+
 
 subsection\<open>Relation between Ln and Arg, and hence continuity of Arg\<close>
 
@@ -1445,6 +1459,15 @@
   using Im_Ln_eq_0 complex_is_Real_iff norm_complex_def
   by auto
 
+lemma cnj_powr:
+  assumes "Im a = 0 \<Longrightarrow> Re a \<ge> 0"
+  shows   "cnj (a powr b) = cnj a powr cnj b"
+proof (cases "a = 0")
+  case False
+  with assms have "Im a = 0 \<Longrightarrow> Re a > 0" by (auto simp: complex_eq_iff)
+  with False show ?thesis by (simp add: powr_def exp_cnj cnj_Ln)
+qed simp
+
 lemma powr_real_real:
     "\<lbrakk>w \<in> \<real>; z \<in> \<real>; 0 < Re w\<rbrakk> \<Longrightarrow> w powr z = exp(Re z * ln(Re w))"
   apply (simp add: powr_def)
@@ -1466,6 +1489,19 @@
            \<Longrightarrow> (x * y) powr z = x powr z * y powr z"
   by (auto simp: Reals_def powr_def Ln_times exp_add algebra_simps less_eq_real_def Ln_of_real)
 
+lemma powr_neg_real_complex:
+  shows   "(- of_real x) powr a = (-1) powr (of_real (sgn x) * a) * of_real x powr (a :: complex)"
+proof (cases "x = 0")
+  assume x: "x \<noteq> 0"
+  hence "(-x) powr a = exp (a * ln (-of_real x))" by (simp add: powr_def)
+  also from x have "ln (-of_real x) = Ln (of_real x) + of_real (sgn x) * pi * \<i>"
+    by (simp add: Ln_minus Ln_of_real)
+  also from x assms have "exp (a * ...) = cis pi powr (of_real (sgn x) * a) * of_real x powr a"
+    by (simp add: powr_def exp_add algebra_simps Ln_of_real cis_conv_exp)
+  also note cis_pi
+  finally show ?thesis by simp
+qed simp_all
+
 lemma has_field_derivative_powr:
     "(Im z = 0 \<Longrightarrow> 0 < Re z)
      \<Longrightarrow> ((\<lambda>z. z powr s) has_field_derivative (s * z powr (s - 1))) (at z)"
@@ -1477,6 +1513,25 @@
   apply (simp add: field_simps exp_diff)
   done
 
+lemma has_field_derivative_powr_complex':
+  assumes "Im z \<noteq> 0 \<or> Re z > 0"
+  shows "((\<lambda>z. z powr r :: complex) has_field_derivative r * z powr (r - 1)) (at z)"
+proof (subst DERIV_cong_ev[OF refl _ refl])
+  from assms have "eventually (\<lambda>z. z \<noteq> 0) (nhds z)" by (intro t1_space_nhds) auto
+  thus "eventually (\<lambda>z. z powr r = Exp (r * Ln z)) (nhds z)"
+    unfolding powr_def by eventually_elim simp
+
+  have "((\<lambda>z. Exp (r * Ln z)) has_field_derivative Exp (r * Ln z) * (inverse z * r)) (at z)" 
+    using assms by (auto intro!: derivative_eq_intros has_field_derivative_powr)
+  also have "Exp (r * Ln z) * (inverse z * r) = r * z powr (r - 1)"
+    unfolding powr_def by (simp add: assms exp_diff field_simps)
+  finally show "((\<lambda>z. Exp (r * Ln z)) has_field_derivative r * z powr (r - 1)) (at z)" 
+    by simp
+qed
+
+declare has_field_derivative_powr_complex'[THEN DERIV_chain2, derivative_intros]
+
+
 lemma has_field_derivative_powr_right:
     "w \<noteq> 0 \<Longrightarrow> ((\<lambda>z. w powr z) has_field_derivative Ln w * w powr z) (at z)"
   apply (simp add: powr_def)
diff -r 9ad1fccbba96 -r f2e51e704a96 src/HOL/Multivariate_Analysis/Derivative.thy
--- a/src/HOL/Multivariate_Analysis/Derivative.thy	Tue Oct 27 23:18:32 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Thu Oct 29 15:40:52 2015 +0100
@@ -1135,6 +1135,15 @@
     by metis
 qed
 
+lemma has_field_derivative_zero_constant:
+  assumes "convex s" "\<And>x. x \<in> s \<Longrightarrow> (f has_field_derivative 0) (at x within s)"
+  shows   "\<exists>c. \<forall>x\<in>s. f (x) = (c :: 'a :: real_normed_field)"
+proof (rule has_derivative_zero_constant)
+  have A: "op * 0 = (\<lambda>_. 0 :: 'a)" by (intro ext) simp
+  fix x assume "x \<in> s" thus "(f has_derivative (\<lambda>h. 0)) (at x within s)"
+    using assms(2)[of x] by (simp add: has_field_derivative_def A)
+qed fact
+
 lemma has_derivative_zero_unique:
   fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
   assumes "convex s"
diff -r 9ad1fccbba96 -r f2e51e704a96 src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Tue Oct 27 23:18:32 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Thu Oct 29 15:40:52 2015 +0100
@@ -6019,12 +6019,6 @@
 
 subsection \<open>Taylor series expansion\<close>
 
-lemma
-  setsum_telescope:
-  fixes f::"nat \<Rightarrow> 'a::ab_group_add"
-  shows "setsum (\<lambda>i. f i - f (Suc i)) {.. i} = f 0 - f (Suc i)"
-  by (induct i) simp_all
-
 lemma (in bounded_bilinear) setsum_prod_derivatives_has_vector_derivative:
   assumes "p>0"
   and f0: "Df 0 = f"
diff -r 9ad1fccbba96 -r f2e51e704a96 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Oct 27 23:18:32 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Oct 29 15:40:52 2015 +0100
@@ -1506,6 +1506,18 @@
     by (metis islimpt_approachable closed_limpt [where 'a='a])
 qed
 
+lemma closed_of_nat_image: "closed (of_nat ` A :: 'a :: real_normed_algebra_1 set)"
+  by (rule discrete_imp_closed[of 1]) (auto simp: dist_of_nat)
+
+lemma closed_of_int_image: "closed (of_int ` A :: 'a :: real_normed_algebra_1 set)"
+  by (rule discrete_imp_closed[of 1]) (auto simp: dist_of_int)
+
+lemma closed_Nats [simp]: "closed (\<nat> :: 'a :: real_normed_algebra_1 set)"
+  unfolding Nats_def by (rule closed_of_nat_image)
+
+lemma closed_Ints [simp]: "closed (\<int> :: 'a :: real_normed_algebra_1 set)"
+  unfolding Ints_def by (rule closed_of_int_image)
+
 
 subsection \<open>Interior of a Set\<close>
 
diff -r 9ad1fccbba96 -r f2e51e704a96 src/HOL/Real_Vector_Spaces.thy
--- a/src/HOL/Real_Vector_Spaces.thy	Tue Oct 27 23:18:32 2015 +0100
+++ b/src/HOL/Real_Vector_Spaces.thy	Thu Oct 29 15:40:52 2015 +0100
@@ -735,6 +735,9 @@
   thus ?thesis by simp
 qed
 
+lemma norm_uminus_minus: "norm (-x - y :: 'a :: real_normed_vector) = norm (x + y)"
+  by (subst (2) norm_minus_cancel[symmetric], subst minus_add_distrib) simp
+
 lemma norm_triangle_ineq2:
   fixes a b :: "'a::real_normed_vector"
   shows "norm a - norm b \<le> norm (a - b)"
@@ -1281,6 +1284,18 @@
 lemma dist_diff [simp]: "dist a (a - b) = norm b"  "dist (a - b) a = norm b"
   by (simp_all add: dist_norm)
   
+lemma dist_of_int: "dist (of_int m) (of_int n :: 'a :: real_normed_algebra_1) = of_int \<bar>m - n\<bar>"
+proof -
+  have "dist (of_int m) (of_int n :: 'a) = dist (of_int m :: 'a) (of_int m - (of_int (m - n)))"
+    by simp
+  also have "\<dots> = of_int \<bar>m - n\<bar>" by (subst dist_diff, subst norm_of_int) simp
+  finally show ?thesis .
+qed
+
+lemma dist_of_nat: 
+  "dist (of_nat m) (of_nat n :: 'a :: real_normed_algebra_1) = of_int \<bar>int m - int n\<bar>"
+  by (subst (1 2) of_int_of_nat_eq [symmetric]) (rule dist_of_int)
+  
 subsection \<open>Bounded Linear and Bilinear Operators\<close>
 
 locale linear = additive f for f :: "'a::real_vector \<Rightarrow> 'b::real_vector" +
diff -r 9ad1fccbba96 -r f2e51e704a96 src/HOL/Set_Interval.thy
--- a/src/HOL/Set_Interval.thy	Tue Oct 27 23:18:32 2015 +0100
+++ b/src/HOL/Set_Interval.thy	Thu Oct 29 15:40:52 2015 +0100
@@ -409,6 +409,11 @@
   "{a .. b} \<subseteq> { c ..< d } \<longleftrightarrow> (a \<le> b \<longrightarrow> c \<le> a \<and> b < d)"
   using dense[of "max a d" "b"]
   by (force simp: subset_eq Ball_def not_less[symmetric])
+  
+lemma greaterThanLessThan_subseteq_greaterThanLessThan:
+  "{a <..< b} \<subseteq> {c <..< d} \<longleftrightarrow> (a < b \<longrightarrow> a \<ge> c \<and> b \<le> d)"
+  using dense[of "a" "min c b"] dense[of "max a d" "b"]
+  by (force simp: subset_eq Ball_def not_less[symmetric])
 
 lemma greaterThanAtMost_subseteq_atLeastLessThan_iff:
   "{a <.. b} \<subseteq> { c ..< d } \<longleftrightarrow> (a < b \<longrightarrow> c \<le> a \<and> b < d)"
@@ -1648,6 +1653,18 @@
   by auto
 
 
+subsection \<open>Telescoping\<close>
+
+lemma setsum_telescope:
+  fixes f::"nat \<Rightarrow> 'a::ab_group_add"
+  shows "setsum (\<lambda>i. f i - f (Suc i)) {.. i} = f 0 - f (Suc i)"
+  by (induct i) simp_all
+
+lemma setsum_telescope'':
+  assumes "m \<le> n"
+  shows   "(\<Sum>k\<in>{Suc m..n}. f k - f (k - 1)) = f n - (f m :: 'a :: ab_group_add)"
+  by (rule dec_induct[OF assms]) (simp_all add: algebra_simps)
+
 subsection \<open>The formula for geometric sums\<close>
 
 lemma geometric_sum:
@@ -1845,4 +1862,38 @@
     by auto
 qed
 
+
+subsection \<open>Shifting bounds\<close>
+
+lemma setprod_shift_bounds_nat_ivl:
+  "setprod f {m+k..<n+k} = setprod (%i. f(i + k)){m..<n::nat}"
+by (induct "n", auto simp:atLeastLessThanSuc)
+
+lemma setprod_shift_bounds_cl_nat_ivl:
+  "setprod f {m+k..n+k} = setprod (%i. f(i + k)){m..n::nat}"
+  by (rule setprod.reindex_bij_witness[where i="\<lambda>i. i + k" and j="\<lambda>i. i - k"]) auto
+
+corollary setprod_shift_bounds_cl_Suc_ivl:
+  "setprod f {Suc m..Suc n} = setprod (%i. f(Suc i)){m..n}"
+by (simp add:setprod_shift_bounds_cl_nat_ivl[where k="Suc 0", simplified])
+
+corollary setprod_shift_bounds_Suc_ivl:
+  "setprod f {Suc m..<Suc n} = setprod (%i. f(Suc i)){m..<n}"
+by (simp add:setprod_shift_bounds_nat_ivl[where k="Suc 0", simplified])
+
+lemma setprod_lessThan_Suc: "setprod f {..<Suc n} = setprod f {..<n} * f n"
+  by (simp add: lessThan_Suc mult.commute)
+
+lemma setprod_atLeastLessThan_Suc: "a \<le> b \<Longrightarrow> setprod f {a..<Suc b} = setprod f {a..<b} * f b"
+  by (simp add: atLeastLessThanSuc mult.commute)
+
+lemma setprod_nat_ivl_Suc':
+  assumes "m \<le> Suc n"
+  shows   "setprod f {m..Suc n} = f (Suc n) * setprod f {m..n}"
+proof -
+  from assms have "{m..Suc n} = insert (Suc n) {m..n}" by auto
+  also have "setprod f \<dots> = f (Suc n) * setprod f {m..n}" by simp
+  finally show ?thesis .
+qed
+
 end
diff -r 9ad1fccbba96 -r f2e51e704a96 src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Tue Oct 27 23:18:32 2015 +0100
+++ b/src/HOL/Transcendental.thy	Thu Oct 29 15:40:52 2015 +0100
@@ -25,6 +25,14 @@
 lemma real_fact_int [simp]: "real (fact n :: int) = fact n"
   by (metis of_int_of_nat_eq of_nat_fact real_of_int_def)
 
+lemma norm_fact [simp]:
+  "norm (fact n :: 'a :: {real_normed_algebra_1}) = fact n"
+proof -
+  have "(fact n :: 'a) = of_real (fact n)" by simp
+  also have "norm \<dots> = fact n" by (subst norm_of_real) simp
+  finally show ?thesis .
+qed
+
 lemma root_test_convergence:
   fixes f :: "nat \<Rightarrow> 'a::banach"
   assumes f: "(\<lambda>n. root n (norm (f n))) ----> x" -- "could be weakened to lim sup"
@@ -2431,6 +2439,14 @@
   apply (metis dual_order.strict_iff_order powr_less_mono2)
   done
 
+lemma powr_mono2':
+  assumes "a \<le> 0" "x > 0" "x \<le> (y::real)"
+  shows   "x powr a \<ge> y powr a"
+proof -
+  from assms have "x powr -a \<le> y powr -a" by (intro powr_mono2) simp_all
+  with assms show ?thesis by (auto simp add: powr_minus field_simps)
+qed
+
 lemma powr_inj:
   fixes x::real shows "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> a powr x = a powr y \<longleftrightarrow> x = y"
   unfolding powr_def exp_inj_iff by simp
@@ -2542,6 +2558,19 @@
   using DERIV_powr[OF g pos DERIV_const, of r] pos
   by (simp add: powr_divide2[symmetric] field_simps)
 
+lemma has_real_derivative_powr:
+  assumes "z > 0"
+  shows "((\<lambda>z. z powr r) has_real_derivative r * z powr (r - 1)) (at z)"
+proof (subst DERIV_cong_ev[OF refl _ refl])
+  from assms have "eventually (\<lambda>z. z \<noteq> 0) (nhds z)" by (intro t1_space_nhds) auto
+  thus "eventually (\<lambda>z. z powr r = exp (r * ln z)) (nhds z)"
+    unfolding powr_def by eventually_elim simp
+  from assms show "((\<lambda>z. exp (r * ln z)) has_real_derivative r * z powr (r - 1)) (at z)"
+    by (auto intro!: derivative_eq_intros simp: powr_def field_simps exp_diff)
+qed
+
+declare has_real_derivative_powr[THEN DERIV_chain2, derivative_intros]
+
 lemma tendsto_zero_powrI:
   assumes "(f ---> (0::real)) F" "(g ---> b) F" "\<forall>\<^sub>F x in F. 0 \<le> f x" "0 < b"
   shows "((\<lambda>x. f x powr g x) ---> 0) F"