author paulson Fri Mar 06 12:48:03 2015 +0000 (2015-03-06) changeset 59615 fdfdf89a83a6 parent 59614 452458cf8506 child 59620 92d7d8e4f1bf
A few new lemmas and a bit of tidying up
 src/HOL/Deriv.thy file | annotate | diff | revisions src/HOL/Groups_Big.thy file | annotate | diff | revisions src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy file | annotate | diff | revisions src/HOL/Multivariate_Analysis/PolyRoots.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Deriv.thy	Thu Mar 05 17:39:04 2015 +0000
1.2 +++ b/src/HOL/Deriv.thy	Fri Mar 06 12:48:03 2015 +0000
1.3 @@ -842,10 +842,6 @@
1.4       by (auto simp add: isCont_iff DERIV_def cong: LIM_cong)
1.5  qed
1.6
1.7 -text {*
1.8 - Let's do the standard proof, though theorem
1.9 - @{text "LIM_mult2"} follows from a NS proof
1.10 -*}
1.11
1.12  subsection {* Local extrema *}
1.13
```
```     2.1 --- a/src/HOL/Groups_Big.thy	Thu Mar 05 17:39:04 2015 +0000
2.2 +++ b/src/HOL/Groups_Big.thy	Fri Mar 06 12:48:03 2015 +0000
2.3 @@ -953,8 +953,9 @@
2.4  apply (auto simp add: algebra_simps)
2.5  done
2.6
2.7 -lemma setsum_Suc: "setsum (%x. Suc(f x)) A = setsum f A + card A"
2.8 -using setsum.distrib[of f "%_. 1" A] by(simp)
2.9 +lemma setsum_Suc: "setsum (\<lambda>x. Suc(f x)) A = setsum f A + card A"
2.10 +  using setsum.distrib[of f "\<lambda>_. 1" A]
2.11 +  by simp
2.12
2.13  lemma setsum_bounded:
2.14    assumes le: "\<And>i. i\<in>A \<Longrightarrow> f i \<le> (K::'a::{semiring_1, ordered_ab_semigroup_add})"
```
```     3.1 --- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Thu Mar 05 17:39:04 2015 +0000
3.2 +++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Fri Mar 06 12:48:03 2015 +0000
3.3 @@ -201,6 +201,12 @@
3.4      shows "DERIV g a :> f'"
3.5    by (blast intro: assms DERIV_transform_within)
3.6
3.7 +(*generalising DERIV_isconst_all, which requires type real (using the ordering)*)
3.8 +lemma DERIV_zero_UNIV_unique:
3.9 +  fixes f :: "'a::{real_normed_field, real_inner} \<Rightarrow> 'a"
3.10 +  shows "(\<And>x. DERIV f x :> 0) \<Longrightarrow> f x = f a"
3.11 +by (metis DERIV_zero_unique UNIV_I assms convex_UNIV)
3.12 +
3.13  subsection {*Some limit theorems about real part of real series etc.*}
3.14
3.15  (*MOVE? But not to Finite_Cartesian_Product*)
3.16 @@ -553,7 +559,7 @@
3.18  done
3.19
3.20 -subsection{*analyticity on a set*}
3.21 +subsection{*Analyticity on a set*}
3.22
3.23  definition analytic_on (infixl "(analytic'_on)" 50)
3.24    where
```
```     4.1 --- a/src/HOL/Multivariate_Analysis/PolyRoots.thy	Thu Mar 05 17:39:04 2015 +0000
4.2 +++ b/src/HOL/Multivariate_Analysis/PolyRoots.thy	Fri Mar 06 12:48:03 2015 +0000
4.3 @@ -17,11 +17,15 @@
4.4    by (simp only: one_diff_power_eq [of "Suc n" x] lessThan_Suc_atMost)
4.5
4.6  lemma setsum_gp0:
4.7 - fixes x :: "'a::{comm_ring,division_ring_inverse_zero}"
4.8 - shows   "(\<Sum>i\<le>n. x^i) = (if x = 1 then of_nat(n + 1) else (1 - x^Suc n) / (1 - x))"
4.9 -using setsum_gp_basic[of x n]
4.11 -by (metis eq_iff_diff_eq_0 mult.commute nonzero_eq_divide_eq)
4.12 +  fixes x :: "'a::{comm_ring,division_ring_inverse_zero}"
4.13 +  shows   "(\<Sum>i\<le>n. x^i) = (if x = 1 then of_nat(n + 1) else (1 - x^Suc n) / (1 - x))"
4.14 +  using setsum_gp_basic[of x n]
4.15 +  by (simp add: real_of_nat_def mult.commute divide_simps)
4.16 +
4.18 +  fixes x :: "'a::{comm_ring,monoid_mult}"
4.19 +  shows "(\<Sum>i\<in>I. x^(m+i)) = x^m * (\<Sum>i\<in>I. x^i)"
4.21
4.22  lemma setsum_power_shift:
4.23    fixes x :: "'a::{comm_ring,monoid_mult}"
4.24 @@ -67,6 +71,11 @@
4.25    using setsum_gp [of x m "m+n"]
4.26    by (auto simp: power_add algebra_simps)
4.27
4.28 +lemma setsum_gp_strict:
4.29 +  fixes x :: "'a::{comm_ring,division_ring_inverse_zero}"
4.30 +  shows "(\<Sum>i<n. x^i) = (if x = 1 then of_nat n else (1 - x^n) / (1 - x))"
4.31 +  by (induct n) (auto simp: algebra_simps divide_simps)
4.32 +
4.33  subsection{*Basics about polynomial functions: extremal behaviour and root counts.*}
4.34
4.35  lemma sub_polyfun:
```