--- a/src/HOL/Deriv.thy Thu Mar 05 17:39:04 2015 +0000
+++ b/src/HOL/Deriv.thy Fri Mar 06 12:48:03 2015 +0000
@@ -842,10 +842,6 @@
by (auto simp add: isCont_iff DERIV_def cong: LIM_cong)
qed
-text {*
- Let's do the standard proof, though theorem
- @{text "LIM_mult2"} follows from a NS proof
-*}
subsection {* Local extrema *}
--- a/src/HOL/Groups_Big.thy Thu Mar 05 17:39:04 2015 +0000
+++ b/src/HOL/Groups_Big.thy Fri Mar 06 12:48:03 2015 +0000
@@ -953,8 +953,9 @@
apply (auto simp add: algebra_simps)
done
-lemma setsum_Suc: "setsum (%x. Suc(f x)) A = setsum f A + card A"
-using setsum.distrib[of f "%_. 1" A] by(simp)
+lemma setsum_Suc: "setsum (\<lambda>x. Suc(f x)) A = setsum f A + card A"
+ using setsum.distrib[of f "\<lambda>_. 1" A]
+ by simp
lemma setsum_bounded:
assumes le: "\<And>i. i\<in>A \<Longrightarrow> f i \<le> (K::'a::{semiring_1, ordered_ab_semigroup_add})"
--- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy Thu Mar 05 17:39:04 2015 +0000
+++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy Fri Mar 06 12:48:03 2015 +0000
@@ -201,6 +201,12 @@
shows "DERIV g a :> f'"
by (blast intro: assms DERIV_transform_within)
+(*generalising DERIV_isconst_all, which requires type real (using the ordering)*)
+lemma DERIV_zero_UNIV_unique:
+ fixes f :: "'a::{real_normed_field, real_inner} \<Rightarrow> 'a"
+ shows "(\<And>x. DERIV f x :> 0) \<Longrightarrow> f x = f a"
+by (metis DERIV_zero_unique UNIV_I assms convex_UNIV)
+
subsection {*Some limit theorems about real part of real series etc.*}
(*MOVE? But not to Finite_Cartesian_Product*)
@@ -553,7 +559,7 @@
apply (simp add: algebra_simps)
done
-subsection{*analyticity on a set*}
+subsection{*Analyticity on a set*}
definition analytic_on (infixl "(analytic'_on)" 50)
where
--- a/src/HOL/Multivariate_Analysis/PolyRoots.thy Thu Mar 05 17:39:04 2015 +0000
+++ b/src/HOL/Multivariate_Analysis/PolyRoots.thy Fri Mar 06 12:48:03 2015 +0000
@@ -17,11 +17,15 @@
by (simp only: one_diff_power_eq [of "Suc n" x] lessThan_Suc_atMost)
lemma setsum_gp0:
- fixes x :: "'a::{comm_ring,division_ring_inverse_zero}"
- shows "(\<Sum>i\<le>n. x^i) = (if x = 1 then of_nat(n + 1) else (1 - x^Suc n) / (1 - x))"
-using setsum_gp_basic[of x n]
-apply (simp add: real_of_nat_def)
-by (metis eq_iff_diff_eq_0 mult.commute nonzero_eq_divide_eq)
+ fixes x :: "'a::{comm_ring,division_ring_inverse_zero}"
+ shows "(\<Sum>i\<le>n. x^i) = (if x = 1 then of_nat(n + 1) else (1 - x^Suc n) / (1 - x))"
+ using setsum_gp_basic[of x n]
+ by (simp add: real_of_nat_def mult.commute divide_simps)
+
+lemma setsum_power_add:
+ fixes x :: "'a::{comm_ring,monoid_mult}"
+ shows "(\<Sum>i\<in>I. x^(m+i)) = x^m * (\<Sum>i\<in>I. x^i)"
+ by (simp add: setsum_right_distrib power_add)
lemma setsum_power_shift:
fixes x :: "'a::{comm_ring,monoid_mult}"
@@ -67,6 +71,11 @@
using setsum_gp [of x m "m+n"]
by (auto simp: power_add algebra_simps)
+lemma setsum_gp_strict:
+ fixes x :: "'a::{comm_ring,division_ring_inverse_zero}"
+ shows "(\<Sum>i<n. x^i) = (if x = 1 then of_nat n else (1 - x^n) / (1 - x))"
+ by (induct n) (auto simp: algebra_simps divide_simps)
+
subsection{*Basics about polynomial functions: extremal behaviour and root counts.*}
lemma sub_polyfun: