--- a/src/HOL/Filter.thy Wed Aug 19 15:40:59 2015 +0200
+++ b/src/HOL/Filter.thy Wed Aug 19 19:18:19 2015 +0100
@@ -670,7 +670,7 @@
"F \<le> sequentially \<longleftrightarrow> (\<forall>N. eventually (\<lambda>n. N \<le> n) F)"
by (simp add: at_top_def le_INF_iff le_principal)
-lemma eventually_sequentiallyI:
+lemma eventually_sequentiallyI [intro?]:
assumes "\<And>x. c \<le> x \<Longrightarrow> P x"
shows "eventually P sequentially"
using assms by (auto simp: eventually_sequentially)
--- a/src/HOL/Groups_Big.thy Wed Aug 19 15:40:59 2015 +0200
+++ b/src/HOL/Groups_Big.thy Wed Aug 19 19:18:19 2015 +0100
@@ -807,20 +807,10 @@
case False thus ?thesis by simp
qed
-lemma setsum_abs_ge_zero[iff]:
+lemma setsum_abs_ge_zero[iff]:
fixes f :: "'a => ('b::ordered_ab_group_add_abs)"
shows "0 \<le> setsum (%i. abs(f i)) A"
-proof (cases "finite A")
- case True
- thus ?thesis
- proof induct
- case empty thus ?case by simp
- next
- case (insert x A) thus ?case by auto
- qed
-next
- case False thus ?thesis by simp
-qed
+ by (simp add: setsum_nonneg)
lemma abs_setsum_abs[simp]:
fixes f :: "'a => ('b::ordered_ab_group_add_abs)"
@@ -931,6 +921,19 @@
"(\<And>a. a \<in> A \<Longrightarrow> d dvd f a) \<Longrightarrow> d dvd setsum f A"
by (induct A rule: infinite_finite_induct) simp_all
+lemma setsum_pos2:
+ assumes "finite I" "i \<in> I" "0 < f i" "(\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i)"
+ shows "(0::'a::{ordered_ab_group_add,comm_monoid_add}) < setsum f I"
+proof -
+ have "0 \<le> setsum f (I-{i})"
+ using assms by (simp add: setsum_nonneg)
+ also have "... < setsum f (I-{i}) + f i"
+ using assms by auto
+ also have "... = setsum f I"
+ using assms by (simp add: setsum.remove)
+ finally show ?thesis .
+qed
+
subsubsection \<open>Cardinality as special case of @{const setsum}\<close>
@@ -957,7 +960,7 @@
using setsum.distrib[of f "\<lambda>_. 1" A]
by simp
-lemma setsum_bounded:
+lemma setsum_bounded_above:
assumes le: "\<And>i. i\<in>A \<Longrightarrow> f i \<le> (K::'a::{semiring_1, ordered_ab_semigroup_add})"
shows "setsum f A \<le> of_nat (card A) * K"
proof (cases "finite A")
@@ -967,6 +970,23 @@
case False thus ?thesis by simp
qed
+lemma setsum_bounded_above_strict:
+ assumes "\<And>i. i\<in>A \<Longrightarrow> f i < (K::'a::{ordered_cancel_ab_semigroup_add,semiring_1})"
+ "card A > 0"
+ shows "setsum f A < of_nat (card A) * K"
+using assms setsum_strict_mono[where A=A and g = "%x. K"]
+by (simp add: card_gt_0_iff)
+
+lemma setsum_bounded_below:
+ assumes le: "\<And>i. i\<in>A \<Longrightarrow> (K::'a::{semiring_1, ordered_ab_semigroup_add}) \<le> f i"
+ shows "of_nat (card A) * K \<le> setsum f A"
+proof (cases "finite A")
+ case True
+ thus ?thesis using le setsum_mono[where K=A and f = "%x. K"] by simp
+next
+ case False thus ?thesis by simp
+qed
+
lemma card_UN_disjoint:
assumes "finite I" and "\<forall>i\<in>I. finite (A i)"
and "\<forall>i\<in>I. \<forall>j\<in>I. i \<noteq> j \<longrightarrow> A i \<inter> A j = {}"
@@ -1210,6 +1230,15 @@
using assms by (induct A rule: infinite_finite_induct)
(auto intro!: setprod_nonneg mult_mono)
+lemma (in linordered_semidom) setprod_mono_strict:
+ assumes"finite A" "\<forall>i\<in>A. 0 \<le> f i \<and> f i < g i" "A \<noteq> {}"
+ shows "setprod f A < setprod g A"
+using assms
+apply (induct A rule: finite_induct)
+apply (simp add: )
+apply (force intro: mult_strict_mono' setprod_nonneg)
+done
+
lemma (in linordered_field) abs_setprod:
"\<bar>setprod f A\<bar> = (\<Prod>x\<in>A. \<bar>f x\<bar>)"
by (induct A rule: infinite_finite_induct) (simp_all add: abs_mult)
@@ -1218,12 +1247,15 @@
"finite A \<Longrightarrow> setprod f A = 1 \<longleftrightarrow> (\<forall>a\<in>A. f a = (1::nat))"
by (induct A rule: finite_induct) simp_all
-lemma setprod_pos_nat:
- "finite A \<Longrightarrow> (\<forall>a\<in>A. f a > (0::nat)) \<Longrightarrow> setprod f A > 0"
- using setprod_zero_iff by (simp del: neq0_conv add: neq0_conv [symmetric])
-
lemma setprod_pos_nat_iff [simp]:
"finite A \<Longrightarrow> setprod f A > 0 \<longleftrightarrow> (\<forall>a\<in>A. f a > (0::nat))"
using setprod_zero_iff by (simp del:neq0_conv add:neq0_conv [symmetric])
+lemma setsum_nonneg_eq_0_iff:
+ fixes f :: "'a \<Rightarrow> 'b::ordered_ab_group_add"
+ shows "\<lbrakk>finite A; \<forall>x\<in>A. 0 \<le> f x\<rbrakk> \<Longrightarrow> setsum f A = 0 \<longleftrightarrow> (\<forall>x\<in>A. f x = 0)"
+ apply (induct set: finite, simp)
+ apply (simp add: add_nonneg_eq_0_iff setsum_nonneg)
+ done
+
end
--- a/src/HOL/Hilbert_Choice.thy Wed Aug 19 15:40:59 2015 +0200
+++ b/src/HOL/Hilbert_Choice.thy Wed Aug 19 19:18:19 2015 +0100
@@ -49,12 +49,16 @@
text\<open>Easier to apply than @{text someI} because the conclusion has only one
occurrence of @{term P}.\<close>
lemma someI2: "[| P a; !!x. P x ==> Q x |] ==> Q (SOME x. P x)"
-by (blast intro: someI)
+ by (blast intro: someI)
text\<open>Easier to apply than @{text someI2} if the witness comes from an
existential formula\<close>
+
lemma someI2_ex: "[| \<exists>a. P a; !!x. P x ==> Q x |] ==> Q (SOME x. P x)"
-by (blast intro: someI2)
+ by (blast intro: someI2)
+
+lemma someI2_bex: "[| \<exists>a\<in>A. P a; !!x. x \<in> A \<and> P x ==> Q x |] ==> Q (SOME x. x \<in> A \<and> P x)"
+ by (blast intro: someI2)
lemma some_equality [intro]:
"[| P a; !!x. P x ==> x=a |] ==> (SOME x. P x) = a"
@@ -102,7 +106,7 @@
by (fast elim: someI)
lemma dependent_nat_choice:
- assumes 1: "\<exists>x. P 0 x" and
+ assumes 1: "\<exists>x. P 0 x" and
2: "\<And>x n. P n x \<Longrightarrow> \<exists>y. P (Suc n) y \<and> Q n x y"
shows "\<exists>f. \<forall>n. P n (f n) \<and> Q n (f n) (f (Suc n))"
proof (intro exI allI conjI)
@@ -263,7 +267,7 @@
apply (blast intro: bij_is_surj [THEN surj_f_inv_f, symmetric])
done
-lemma bij_vimage_eq_inv_image: "bij f ==> f -` A = inv f ` A"
+lemma bij_vimage_eq_inv_image: "bij f ==> f -` A = inv f ` A"
apply (auto simp add: bij_is_surj [THEN surj_f_inv_f])
apply (blast intro: bij_is_inj [THEN inv_into_f_f, symmetric])
done
@@ -312,7 +316,7 @@
unfolding pick_def by (subst (asm) finite.simps) (auto simp add: ex_in_conv intro: someI_ex)
ultimately have "range pick \<subseteq> S" by auto
moreover
- { fix n m
+ { fix n m
have "pick n \<notin> Sseq (n + Suc m)" by (induct m) (auto simp add: Sseq_def pick_def)
with * have "pick n \<noteq> pick (n + Suc m)" by auto
}
--- a/src/HOL/IMP/Abs_Int0.thy Wed Aug 19 15:40:59 2015 +0200
+++ b/src/HOL/IMP/Abs_Int0.thy Wed Aug 19 19:18:19 2015 +0100
@@ -317,7 +317,7 @@
"m_s S X = (\<Sum> x \<in> X. m(S x))"
lemma m_s_h: "finite X \<Longrightarrow> m_s S X \<le> h * card X"
-by(simp add: m_s_def) (metis mult.commute of_nat_id setsum_bounded[OF h])
+by(simp add: m_s_def) (metis mult.commute of_nat_id setsum_bounded_above[OF h])
fun m_o :: "'av st option \<Rightarrow> vname set \<Rightarrow> nat" ("m\<^sub>o") where
"m_o (Some S) X = m_s S X" |
--- a/src/HOL/IMP/Abs_Int1.thy Wed Aug 19 15:40:59 2015 +0200
+++ b/src/HOL/IMP/Abs_Int1.thy Wed Aug 19 19:18:19 2015 +0100
@@ -109,7 +109,7 @@
"m_s S X = (\<Sum> x \<in> X. m(fun S x))"
lemma m_s_h: "finite X \<Longrightarrow> m_s S X \<le> h * card X"
-by(simp add: m_s_def) (metis mult.commute of_nat_id setsum_bounded[OF h])
+by(simp add: m_s_def) (metis mult.commute of_nat_id setsum_bounded_above[OF h])
definition m_o :: "'av st option \<Rightarrow> vname set \<Rightarrow> nat" ("m\<^sub>o") where
"m_o opt X = (case opt of None \<Rightarrow> h * card X + 1 | Some S \<Rightarrow> m_s S X)"
--- a/src/HOL/Limits.thy Wed Aug 19 15:40:59 2015 +0200
+++ b/src/HOL/Limits.thy Wed Aug 19 19:18:19 2015 +0100
@@ -1945,6 +1945,20 @@
by auto
qed
+lemma open_Collect_positive:
+ fixes f :: "'a::t2_space \<Rightarrow> real"
+ assumes f: "continuous_on s f"
+ shows "\<exists>A. open A \<and> A \<inter> s = {x\<in>s. 0 < f x}"
+ using continuous_on_open_invariant[THEN iffD1, OF f, rule_format, of "{0 <..}"]
+ by (auto simp: Int_def field_simps)
+
+lemma open_Collect_less_Int:
+ fixes f g :: "'a::t2_space \<Rightarrow> real"
+ assumes f: "continuous_on s f" and g: "continuous_on s g"
+ shows "\<exists>A. open A \<and> A \<inter> s = {x\<in>s. f x < g x}"
+ using open_Collect_positive[OF continuous_on_diff[OF g f]] by (simp add: field_simps)
+
+
subsection \<open>Boundedness of continuous functions\<close>
text\<open>By bisection, function continuous on closed interval is bounded above\<close>
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Wed Aug 19 15:40:59 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Wed Aug 19 19:18:19 2015 +0100
@@ -1226,7 +1226,7 @@
then have "0 \<in> closure S \<and> (\<forall>c. c > 0 \<longrightarrow> op *\<^sub>R c ` closure S = closure S)"
using closure_subset by (auto simp add: closure_scaleR)
then show ?thesis
- using cone_iff[of "closure S"] by auto
+ using False cone_iff[of "closure S"] by auto
qed
@@ -9545,4 +9545,216 @@
apply simp
done
+subsection\<open>The infimum of the distance between two sets\<close>
+
+definition setdist :: "'a::metric_space set \<Rightarrow> 'a set \<Rightarrow> real" where
+ "setdist s t \<equiv>
+ (if s = {} \<or> t = {} then 0
+ else Inf {dist x y| x y. x \<in> s \<and> y \<in> t})"
+
+lemma setdist_empty1 [simp]: "setdist {} t = 0"
+ by (simp add: setdist_def)
+
+lemma setdist_empty2 [simp]: "setdist t {} = 0"
+ by (simp add: setdist_def)
+
+lemma setdist_pos_le: "0 \<le> setdist s t"
+ by (auto simp: setdist_def ex_in_conv [symmetric] intro: cInf_greatest)
+
+lemma le_setdistI:
+ assumes "s \<noteq> {}" "t \<noteq> {}" "\<And>x y. \<lbrakk>x \<in> s; y \<in> t\<rbrakk> \<Longrightarrow> d \<le> dist x y"
+ shows "d \<le> setdist s t"
+ using assms
+ by (auto simp: setdist_def Set.ex_in_conv [symmetric] intro: cInf_greatest)
+
+lemma setdist_le_dist: "\<lbrakk>x \<in> s; y \<in> t\<rbrakk> \<Longrightarrow> setdist s t \<le> dist x y"
+ unfolding setdist_def
+ by (auto intro!: bdd_belowI [where m=0] cInf_lower)
+
+lemma le_setdist_iff:
+ "d \<le> setdist s t \<longleftrightarrow>
+ (\<forall>x \<in> s. \<forall>y \<in> t. d \<le> dist x y) \<and> (s = {} \<or> t = {} \<longrightarrow> d \<le> 0)"
+ apply (cases "s = {} \<or> t = {}")
+ apply (force simp add: setdist_def)
+ apply (intro iffI conjI)
+ using setdist_le_dist apply fastforce
+ apply (auto simp: intro: le_setdistI)
+ done
+
+lemma setdist_ltE:
+ assumes "setdist s t < b" "s \<noteq> {}" "t \<noteq> {}"
+ obtains x y where "x \<in> s" "y \<in> t" "dist x y < b"
+using assms
+by (auto simp: not_le [symmetric] le_setdist_iff)
+
+lemma setdist_refl: "setdist s s = 0"
+ apply (cases "s = {}")
+ apply (force simp add: setdist_def)
+ apply (rule antisym [OF _ setdist_pos_le])
+ apply (metis all_not_in_conv dist_self setdist_le_dist)
+ done
+
+lemma setdist_sym: "setdist s t = setdist t s"
+ by (force simp: setdist_def dist_commute intro!: arg_cong [where f=Inf])
+
+lemma setdist_triangle: "setdist s t \<le> setdist s {a} + setdist {a} t"
+proof (cases "s = {} \<or> t = {}")
+ case True then show ?thesis
+ using setdist_pos_le by fastforce
+next
+ case False
+ have "\<And>x. x \<in> s \<Longrightarrow> setdist s t - dist x a \<le> setdist {a} t"
+ apply (rule le_setdistI, blast)
+ using False apply (fastforce intro: le_setdistI)
+ apply (simp add: algebra_simps)
+ apply (metis dist_commute dist_triangle_alt order_trans [OF setdist_le_dist])
+ done
+ then have "setdist s t - setdist {a} t \<le> setdist s {a}"
+ using False by (fastforce intro: le_setdistI)
+ then show ?thesis
+ by (simp add: algebra_simps)
+qed
+
+lemma setdist_singletons [simp]: "setdist {x} {y} = dist x y"
+ by (simp add: setdist_def)
+
+lemma setdist_Lipschitz: "abs(setdist {x} s - setdist {y} s) \<le> dist x y"
+ apply (subst setdist_singletons [symmetric])
+ by (metis abs_diff_le_iff diff_le_eq setdist_triangle setdist_sym)
+
+lemma continuous_at_setdist: "continuous (at x) (\<lambda>y. (setdist {y} s))"
+ by (force simp: continuous_at_eps_delta dist_real_def intro: le_less_trans [OF setdist_Lipschitz])
+
+lemma continuous_on_setdist: "continuous_on t (\<lambda>y. (setdist {y} s))"
+ by (metis continuous_at_setdist continuous_at_imp_continuous_on)
+
+lemma uniformly_continuous_on_setdist: "uniformly_continuous_on t (\<lambda>y. (setdist {y} s))"
+ by (force simp: uniformly_continuous_on_def dist_real_def intro: le_less_trans [OF setdist_Lipschitz])
+
+lemma setdist_subset_right: "\<lbrakk>t \<noteq> {}; t \<subseteq> u\<rbrakk> \<Longrightarrow> setdist s u \<le> setdist s t"
+ apply (cases "s = {} \<or> u = {}", force)
+ apply (auto simp: setdist_def intro!: bdd_belowI [where m=0] cInf_superset_mono)
+ done
+
+lemma setdist_subset_left: "\<lbrakk>s \<noteq> {}; s \<subseteq> t\<rbrakk> \<Longrightarrow> setdist t u \<le> setdist s u"
+ by (metis setdist_subset_right setdist_sym)
+
+lemma setdist_closure_1 [simp]: "setdist (closure s) t = setdist s t"
+proof (cases "s = {} \<or> t = {}")
+ case True then show ?thesis by force
+next
+ case False
+ { fix y
+ assume "y \<in> t"
+ have "continuous_on (closure s) (\<lambda>a. dist a y)"
+ by (auto simp: continuous_intros dist_norm)
+ then have *: "\<And>x. x \<in> closure s \<Longrightarrow> setdist s t \<le> dist x y"
+ apply (rule continuous_ge_on_closure)
+ apply assumption
+ apply (blast intro: setdist_le_dist `y \<in> t` )
+ done
+ } note * = this
+ show ?thesis
+ apply (rule antisym)
+ using False closure_subset apply (blast intro: setdist_subset_left)
+ using False *
+ apply (force simp add: closure_eq_empty intro!: le_setdistI)
+ done
+qed
+
+lemma setdist_closure_2 [simp]: "setdist t (closure s) = setdist t s"
+by (metis setdist_closure_1 setdist_sym)
+
+lemma setdist_compact_closed:
+ fixes s :: "'a::euclidean_space set"
+ assumes s: "compact s" and t: "closed t"
+ and "s \<noteq> {}" "t \<noteq> {}"
+ shows "\<exists>x \<in> s. \<exists>y \<in> t. dist x y = setdist s t"
+proof -
+ have "{x - y |x y. x \<in> s \<and> y \<in> t} \<noteq> {}"
+ using assms by blast
+ then
+ have "\<exists>x \<in> s. \<exists>y \<in> t. dist x y \<le> setdist s t"
+ using distance_attains_inf [where a=0, OF compact_closed_differences [OF s t]] assms
+ apply (clarsimp simp: dist_norm le_setdist_iff, blast)
+ done
+ then show ?thesis
+ by (blast intro!: antisym [OF _ setdist_le_dist] )
+qed
+
+lemma setdist_closed_compact:
+ fixes s :: "'a::euclidean_space set"
+ assumes s: "closed s" and t: "compact t"
+ and "s \<noteq> {}" "t \<noteq> {}"
+ shows "\<exists>x \<in> s. \<exists>y \<in> t. dist x y = setdist s t"
+ using setdist_compact_closed [OF t s `t \<noteq> {}` `s \<noteq> {}`]
+ by (metis dist_commute setdist_sym)
+
+lemma setdist_eq_0I: "\<lbrakk>x \<in> s; x \<in> t\<rbrakk> \<Longrightarrow> setdist s t = 0"
+ by (metis antisym dist_self setdist_le_dist setdist_pos_le)
+
+lemma setdist_eq_0_compact_closed:
+ fixes s :: "'a::euclidean_space set"
+ assumes s: "compact s" and t: "closed t"
+ shows "setdist s t = 0 \<longleftrightarrow> s = {} \<or> t = {} \<or> s \<inter> t \<noteq> {}"
+ apply (cases "s = {} \<or> t = {}", force)
+ using setdist_compact_closed [OF s t]
+ apply (force intro: setdist_eq_0I )
+ done
+
+corollary setdist_gt_0_compact_closed:
+ fixes s :: "'a::euclidean_space set"
+ assumes s: "compact s" and t: "closed t"
+ shows "setdist s t > 0 \<longleftrightarrow> (s \<noteq> {} \<and> t \<noteq> {} \<and> s \<inter> t = {})"
+ using setdist_pos_le [of s t] setdist_eq_0_compact_closed [OF assms]
+ by linarith
+
+lemma setdist_eq_0_closed_compact:
+ fixes s :: "'a::euclidean_space set"
+ assumes s: "closed s" and t: "compact t"
+ shows "setdist s t = 0 \<longleftrightarrow> s = {} \<or> t = {} \<or> s \<inter> t \<noteq> {}"
+ using setdist_eq_0_compact_closed [OF t s]
+ by (metis Int_commute setdist_sym)
+
+lemma setdist_eq_0_bounded:
+ fixes s :: "'a::euclidean_space set"
+ assumes "bounded s \<or> bounded t"
+ shows "setdist s t = 0 \<longleftrightarrow> s = {} \<or> t = {} \<or> closure s \<inter> closure t \<noteq> {}"
+ apply (cases "s = {} \<or> t = {}", force)
+ using setdist_eq_0_compact_closed [of "closure s" "closure t"]
+ setdist_eq_0_closed_compact [of "closure s" "closure t"] assms
+ apply (force simp add: bounded_closure compact_eq_bounded_closed)
+ done
+
+lemma setdist_unique:
+ "\<lbrakk>a \<in> s; b \<in> t; \<And>x y. x \<in> s \<and> y \<in> t ==> dist a b \<le> dist x y\<rbrakk>
+ \<Longrightarrow> setdist s t = dist a b"
+ by (force simp add: setdist_le_dist le_setdist_iff intro: antisym)
+
+lemma setdist_closest_point:
+ "\<lbrakk>closed s; s \<noteq> {}\<rbrakk> \<Longrightarrow> setdist {a} s = dist a (closest_point s a)"
+ apply (rule setdist_unique)
+ using closest_point_le
+ apply (auto simp: closest_point_in_set)
+ done
+
+lemma setdist_eq_0_sing_1 [simp]:
+ fixes s :: "'a::euclidean_space set"
+ shows "setdist {x} s = 0 \<longleftrightarrow> s = {} \<or> x \<in> closure s"
+by (auto simp: setdist_eq_0_bounded)
+
+lemma setdist_eq_0_sing_2 [simp]:
+ fixes s :: "'a::euclidean_space set"
+ shows "setdist s {x} = 0 \<longleftrightarrow> s = {} \<or> x \<in> closure s"
+by (auto simp: setdist_eq_0_bounded)
+
+lemma setdist_sing_in_set:
+ fixes s :: "'a::euclidean_space set"
+ shows "x \<in> s \<Longrightarrow> setdist {x} s = 0"
+using closure_subset by force
+
+lemma setdist_le_sing: "x \<in> s ==> setdist s t \<le> setdist {x} t"
+ using setdist_subset_left by auto
+
+
end
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Wed Aug 19 15:40:59 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Wed Aug 19 19:18:19 2015 +0100
@@ -92,6 +92,18 @@
by (auto intro!: exI[of _ "\<Sum>i\<in>Basis. f i *\<^sub>R i"])
qed auto
+lemma (in euclidean_space) euclidean_representation_setsum_fun:
+ "(\<lambda>x. \<Sum>b\<in>Basis. inner (f x) b *\<^sub>R b) = f"
+ by (rule ext) (simp add: euclidean_representation_setsum)
+
+lemma euclidean_isCont:
+ assumes "\<And>b. b \<in> Basis \<Longrightarrow> isCont (\<lambda>x. (inner (f x) b) *\<^sub>R b) x"
+ shows "isCont f x"
+ apply (subst euclidean_representation_setsum_fun [symmetric])
+ apply (rule isCont_setsum)
+ apply (blast intro: assms)
+ done
+
lemma DIM_positive: "0 < DIM('a::euclidean_space)"
by (simp add: card_gt_0_iff)
--- a/src/HOL/Multivariate_Analysis/L2_Norm.thy Wed Aug 19 15:40:59 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/L2_Norm.thy Wed Aug 19 19:18:19 2015 +0100
@@ -70,13 +70,6 @@
apply (simp add: real_sqrt_mult setsum_nonneg)
done
-lemma setsum_nonneg_eq_0_iff:
- fixes f :: "'a \<Rightarrow> 'b::ordered_ab_group_add"
- shows "\<lbrakk>finite A; \<forall>x\<in>A. 0 \<le> f x\<rbrakk> \<Longrightarrow> setsum f A = 0 \<longleftrightarrow> (\<forall>x\<in>A. f x = 0)"
- apply (induct set: finite, simp)
- apply (simp add: add_nonneg_eq_0_iff setsum_nonneg)
- done
-
lemma setL2_eq_0_iff: "finite A \<Longrightarrow> setL2 f A = 0 \<longleftrightarrow> (\<forall>x\<in>A. f x = 0)"
unfolding setL2_def
by (simp add: setsum_nonneg setsum_nonneg_eq_0_iff)
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Wed Aug 19 15:40:59 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Wed Aug 19 19:18:19 2015 +0100
@@ -562,25 +562,45 @@
using reals_Archimedean[of e] less_trans[of 0 "1 / real n" e for n::nat]
by (auto simp add: field_simps cong: conj_cong)
-lemma real_pow_lbound: "0 \<le> x \<Longrightarrow> 1 + real n * x \<le> (1 + x) ^ n"
+text{*Bernoulli's inequality*}
+lemma Bernoulli_inequality:
+ fixes x :: real
+ assumes "-1 \<le> x"
+ shows "1 + n * x \<le> (1 + x) ^ n"
proof (induct n)
case 0
then show ?case by simp
next
case (Suc n)
- then have h: "1 + real n * x \<le> (1 + x) ^ n"
- by simp
- from h have p: "1 \<le> (1 + x) ^ n"
- using Suc.prems by simp
- from h have "1 + real n * x + x \<le> (1 + x) ^ n + x"
+ have "1 + Suc n * x \<le> 1 + (Suc n)*x + n * x^2"
+ by (simp add: algebra_simps)
+ also have "... = (1 + x) * (1 + n*x)"
+ by (auto simp: power2_eq_square algebra_simps real_of_nat_Suc)
+ also have "... \<le> (1 + x) ^ Suc n"
+ using Suc.hyps assms mult_left_mono by fastforce
+ finally show ?case .
+qed
+
+lemma Bernoulli_inequality_even:
+ fixes x :: real
+ assumes "even n"
+ shows "1 + n * x \<le> (1 + x) ^ n"
+proof (cases "-1 \<le> x \<or> n=0")
+ case True
+ then show ?thesis
+ by (auto simp: Bernoulli_inequality)
+next
+ case False
+ then have "real n \<ge> 1"
by simp
- also have "\<dots> \<le> (1 + x) ^ Suc n"
- apply (subst diff_le_0_iff_le[symmetric])
- using mult_left_mono[OF p Suc.prems]
- apply (simp add: field_simps)
- done
- finally show ?case
- by (simp add: real_of_nat_Suc field_simps)
+ with False have "n * x \<le> -1"
+ by (metis linear minus_zero mult.commute mult.left_neutral mult_left_mono_neg neg_le_iff_le order_trans zero_le_one)
+ then have "1 + n * x \<le> 0"
+ by auto
+ also have "... \<le> (1 + x) ^ n"
+ using assms
+ using zero_le_even_power by blast
+ finally show ?thesis .
qed
lemma real_arch_pow:
@@ -592,8 +612,8 @@
by arith
from reals_Archimedean3[OF x0, rule_format, of y]
obtain n :: nat where n: "y < real n * (x - 1)" by metis
- from x0 have x00: "x- 1 \<ge> 0" by arith
- from real_pow_lbound[OF x00, of n] n
+ from x0 have x00: "x- 1 \<ge> -1" by arith
+ from Bernoulli_inequality[OF x00, of n] n
have "y < x^n" by auto
then show ?thesis by metis
qed
@@ -1417,7 +1437,7 @@
also have "(\<Sum>x\<in>P. \<Sum>b\<in>Basis. \<bar>f x \<bullet> b\<bar>) = (\<Sum>b\<in>Basis. \<Sum>x\<in>P. \<bar>f x \<bullet> b\<bar>)"
by (rule setsum.commute)
also have "\<dots> \<le> of_nat (card (Basis :: 'n set)) * (2 * e)"
- proof (rule setsum_bounded)
+ proof (rule setsum_bounded_above)
fix i :: 'n
assume i: "i \<in> Basis"
have "norm (\<Sum>x\<in>P. \<bar>f x \<bullet> i\<bar>) \<le>
@@ -2828,7 +2848,7 @@
unfolding real_of_nat_def
apply (subst euclidean_inner)
apply (subst power2_abs[symmetric])
- apply (rule order_trans[OF setsum_bounded[where K="\<bar>infnorm x\<bar>\<^sup>2"]])
+ apply (rule order_trans[OF setsum_bounded_above[where K="\<bar>infnorm x\<bar>\<^sup>2"]])
apply (auto simp add: power2_eq_square[symmetric])
apply (subst power2_abs[symmetric])
apply (rule power_mono)
--- a/src/HOL/Multivariate_Analysis/Path_Connected.thy Wed Aug 19 15:40:59 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy Wed Aug 19 19:18:19 2015 +0100
@@ -175,7 +175,7 @@
lemma simple_path_eq_arc: "pathfinish g \<noteq> pathstart g \<Longrightarrow> (simple_path g = arc g)"
by (simp add: arc_simple_path)
-lemma path_image_nonempty: "path_image g \<noteq> {}"
+lemma path_image_nonempty [simp]: "path_image g \<noteq> {}"
unfolding path_image_def image_is_empty box_eq_empty
by auto
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Wed Aug 19 15:40:59 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Wed Aug 19 19:18:19 2015 +0100
@@ -1602,7 +1602,7 @@
lemma closure_union [simp]: "closure (S \<union> T) = closure S \<union> closure T"
unfolding closure_interior by simp
-lemma closure_eq_empty: "closure S = {} \<longleftrightarrow> S = {}"
+lemma closure_eq_empty [iff]: "closure S = {} \<longleftrightarrow> S = {}"
using closure_empty closure_subset[of S]
by blast
@@ -1826,7 +1826,7 @@
text\<open>Interrelations between restricted and unrestricted limits.\<close>
-lemma Lim_at_imp_Lim_at_within:
+lemma Lim_at_imp_Lim_at_within:
"(f ---> l) (at x) \<Longrightarrow> (f ---> l) (at x within S)"
by (metis order_refl filterlim_mono subset_UNIV at_le)
@@ -2831,12 +2831,12 @@
(metis abs_le_D1 add.commute diff_le_eq)
lemma bounded_inner_imp_bdd_above:
- assumes "bounded s"
+ assumes "bounded s"
shows "bdd_above ((\<lambda>x. x \<bullet> a) ` s)"
by (simp add: assms bounded_imp_bdd_above bounded_linear_image bounded_linear_inner_left)
lemma bounded_inner_imp_bdd_below:
- assumes "bounded s"
+ assumes "bounded s"
shows "bdd_below ((\<lambda>x. x \<bullet> a) ` s)"
by (simp add: assms bounded_imp_bdd_below bounded_linear_image bounded_linear_inner_left)
@@ -4635,6 +4635,12 @@
text\<open>Some simple consequential lemmas.\<close>
+lemma uniformly_continuous_onE:
+ assumes "uniformly_continuous_on s f" "0 < e"
+ obtains d where "d>0" "\<And>x x'. \<lbrakk>x\<in>s; x'\<in>s; dist x' x < d\<rbrakk> \<Longrightarrow> dist (f x') (f x) < e"
+using assms
+by (auto simp: uniformly_continuous_on_def)
+
lemma uniformly_continuous_imp_continuous:
"uniformly_continuous_on s f \<Longrightarrow> continuous_on s f"
unfolding uniformly_continuous_on_def continuous_on_iff by blast
@@ -6166,6 +6172,19 @@
finally show ?thesis .
qed
+lemma continuous_on_closed_Collect_le:
+ fixes f g :: "'a::t2_space \<Rightarrow> real"
+ assumes f: "continuous_on s f" and g: "continuous_on s g" and s: "closed s"
+ shows "closed {x \<in> s. f x \<le> g x}"
+proof -
+ have "closed ((\<lambda>x. g x - f x) -` {0..} \<inter> s)"
+ using closed_real_atLeast continuous_on_diff [OF g f]
+ by (simp add: continuous_on_closed_vimage [OF s])
+ also have "((\<lambda>x. g x - f x) -` {0..} \<inter> s) = {x\<in>s. f x \<le> g x}"
+ by auto
+ finally show ?thesis .
+qed
+
lemma continuous_at_inner: "continuous (at x) (inner a)"
unfolding continuous_at by (intro tendsto_intros)
@@ -6194,6 +6213,25 @@
shows "closed {x::'a. \<forall>i\<in>Basis. a\<bullet>i \<le> x\<bullet>i}"
by (simp add: Collect_ball_eq closed_INT closed_Collect_le)
+lemma continuous_le_on_closure:
+ fixes a::real
+ assumes f: "continuous_on (closure s) f"
+ and x: "x \<in> closure(s)"
+ and xlo: "\<And>x. x \<in> s ==> f(x) \<le> a"
+ shows "f(x) \<le> a"
+ using image_closure_subset [OF f]
+ using image_closure_subset [OF f] closed_halfspace_le [of "1::real" a] assms
+ by force
+
+lemma continuous_ge_on_closure:
+ fixes a::real
+ assumes f: "continuous_on (closure s) f"
+ and x: "x \<in> closure(s)"
+ and xlo: "\<And>x. x \<in> s ==> f(x) \<ge> a"
+ shows "f(x) \<ge> a"
+ using image_closure_subset [OF f] closed_halfspace_ge [of a "1::real"] assms
+ by force
+
text \<open>Openness of halfspaces.\<close>
lemma open_halfspace_lt: "open {x. inner a x < b}"
@@ -7320,7 +7358,7 @@
subsection \<open>Banach fixed point theorem (not really topological...)\<close>
-lemma banach_fix:
+theorem banach_fix:
assumes s: "complete s" "s \<noteq> {}"
and c: "0 \<le> c" "c < 1"
and f: "(f ` s) \<subseteq> s"
@@ -7501,7 +7539,7 @@
subsection \<open>Edelstein fixed point theorem\<close>
-lemma edelstein_fix:
+theorem edelstein_fix:
fixes s :: "'a::metric_space set"
assumes s: "compact s" "s \<noteq> {}"
and gs: "(g ` s) \<subseteq> s"
--- a/src/HOL/Power.thy Wed Aug 19 15:40:59 2015 +0200
+++ b/src/HOL/Power.thy Wed Aug 19 19:18:19 2015 +0100
@@ -762,6 +762,10 @@
"(x - y)\<^sup>2 = x\<^sup>2 + y\<^sup>2 - 2 * x * y"
by (simp add: algebra_simps power2_eq_square mult_2_right)
+lemma (in comm_ring_1) power2_commute:
+ "(x - y)\<^sup>2 = (y - x)\<^sup>2"
+ by (simp add: algebra_simps power2_eq_square)
+
text \<open>Simprules for comparisons where common factors can be cancelled.\<close>