--- a/src/HOL/Analysis/Borel_Space.thy Mon Sep 26 07:56:54 2016 +0200
+++ b/src/HOL/Analysis/Borel_Space.thy Wed Sep 28 17:01:01 2016 +0100
@@ -101,7 +101,7 @@
assumes mono: "mono_on f A" and deriv: "(f has_real_derivative D) (at x)"
assumes "x \<in> interior A"
shows "D \<ge> 0"
-proof (rule tendsto_le_const)
+proof (rule tendsto_lowerbound)
let ?A' = "(\<lambda>y. y - x) ` interior A"
from deriv show "((\<lambda>h. (f (x + h) - f x) / h) \<longlongrightarrow> D) (at 0)"
by (simp add: field_has_derivative_at has_field_derivative_def)
--- a/src/HOL/Analysis/Bounded_Linear_Function.thy Mon Sep 26 07:56:54 2016 +0200
+++ b/src/HOL/Analysis/Bounded_Linear_Function.thy Wed Sep 28 17:01:01 2016 +0100
@@ -328,7 +328,7 @@
have tendsto_v: "(\<lambda>m. norm (X n x - X m x)) \<longlonglongrightarrow> norm (X n x - Blinfun v x)"
by (auto intro!: tendsto_intros Bv)
show "norm ((X n - Blinfun v) x) \<le> r' * norm x"
- by (auto intro!: tendsto_ge_const tendsto_v ev_le simp: blinfun.bilinear_simps)
+ by (auto intro!: tendsto_upperbound tendsto_v ev_le simp: blinfun.bilinear_simps)
qed (simp add: \<open>0 < r'\<close> less_imp_le)
thus "norm (X n - Blinfun v) < r"
by (metis \<open>r' < r\<close> le_less_trans)
--- a/src/HOL/Analysis/Derivative.thy Mon Sep 26 07:56:54 2016 +0200
+++ b/src/HOL/Analysis/Derivative.thy Wed Sep 28 17:01:01 2016 +0100
@@ -1998,7 +1998,7 @@
by (auto simp add: algebra_simps)
qed
ultimately show "norm (f n x - f n y - (g x - g y)) \<le> e * norm (x - y)"
- by (rule tendsto_ge_const[OF trivial_limit_sequentially])
+ by (simp add: tendsto_upperbound)
qed
qed
have "\<forall>x\<in>s. ((\<lambda>n. f n x) \<longlongrightarrow> g x) sequentially \<and> (g has_derivative g' x) (at x within s)"
@@ -2667,7 +2667,7 @@
qed
hence "eventually (\<lambda>y. (f y - f c) / (y - c) \<le> (f x - f c) / (x - c)) (at c within ?A')"
by (blast intro: filter_leD at_le)
- ultimately have "f' \<le> (f x - f c) / (x - c)" by (rule tendsto_ge_const)
+ ultimately have "f' \<le> (f x - f c) / (x - c)" by (simp add: tendsto_upperbound)
thus ?thesis using xc by (simp add: field_simps)
next
assume xc: "x < c"
@@ -2691,7 +2691,7 @@
qed
hence "eventually (\<lambda>y. (f y - f c) / (y - c) \<ge> (f x - f c) / (x - c)) (at c within ?A')"
by (blast intro: filter_leD at_le)
- ultimately have "f' \<ge> (f x - f c) / (x - c)" by (rule tendsto_le_const)
+ ultimately have "f' \<ge> (f x - f c) / (x - c)" by (simp add: tendsto_lowerbound)
thus ?thesis using xc by (simp add: field_simps)
qed simp_all
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Mon Sep 26 07:56:54 2016 +0200
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Wed Sep 28 17:01:01 2016 +0100
@@ -1870,7 +1870,7 @@
have F_mono: "a \<le> x \<Longrightarrow> x \<le> y \<Longrightarrow> F x \<le> F y" for x y
using f nonneg by (intro DERIV_nonneg_imp_nondecreasing[of x y F]) (auto intro: order_trans)
then have F_le_T: "a \<le> x \<Longrightarrow> F x \<le> T" for x
- by (intro tendsto_le_const[OF _ lim])
+ by (intro tendsto_lowerbound[OF lim])
(auto simp: trivial_limit_at_top_linorder eventually_at_top_linorder)
have "(SUP i::nat. ?f i x) = ?fR x" for x
--- a/src/HOL/Analysis/Euclidean_Space.thy Mon Sep 26 07:56:54 2016 +0200
+++ b/src/HOL/Analysis/Euclidean_Space.thy Wed Sep 28 17:01:01 2016 +0100
@@ -93,6 +93,11 @@
by (auto intro!: exI[of _ "\<Sum>i\<in>Basis. f i *\<^sub>R i"])
qed auto
+lemma (in euclidean_space) bchoice_Basis_iff:
+ fixes P :: "'a \<Rightarrow> real \<Rightarrow> bool"
+ shows "(\<forall>i\<in>Basis. \<exists>x\<in>A. P i x) \<longleftrightarrow> (\<exists>x. \<forall>i\<in>Basis. inner x i \<in> A \<and> P i (inner x i))"
+by (simp add: choice_Basis_iff Bex_def)
+
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)
--- a/src/HOL/Analysis/Gamma_Function.thy Mon Sep 26 07:56:54 2016 +0200
+++ b/src/HOL/Analysis/Gamma_Function.thy Wed Sep 28 17:01:01 2016 +0100
@@ -1812,13 +1812,13 @@
shows "G x = Gamma x"
proof (rule antisym)
show "G x \<ge> Gamma x"
- proof (rule tendsto_ge_const)
+ proof (rule tendsto_upperbound)
from G_lower[of x] show "eventually (\<lambda>n. Gamma_series x n \<le> G x) sequentially"
using eventually_ge_at_top[of "1::nat"] x by (auto elim!: eventually_mono)
qed (simp_all add: Gamma_series_LIMSEQ)
next
show "G x \<le> Gamma x"
- proof (rule tendsto_le_const)
+ proof (rule tendsto_lowerbound)
have "(\<lambda>n. Gamma_series x n * (1 + x / real n)) \<longlonglongrightarrow> Gamma x * (1 + 0)"
by (rule tendsto_intros real_tendsto_divide_at_top
Gamma_series_LIMSEQ filterlim_real_sequentially)+
--- a/src/HOL/Deriv.thy Mon Sep 26 07:56:54 2016 +0200
+++ b/src/HOL/Deriv.thy Wed Sep 28 17:01:01 2016 +0100
@@ -1563,12 +1563,12 @@
and lim: "(f \<longlongrightarrow> flim) at_bot"
shows "flim < f b"
proof -
- have "flim \<le> f (b - 1)"
- apply (rule tendsto_ge_const [OF _ lim])
- apply (auto simp: trivial_limit_at_bot_linorder eventually_at_bot_linorder)
+ have "\<exists>N. \<forall>n\<le>N. f n \<le> f (b - 1)"
apply (rule_tac x="b - 2" in exI)
apply (force intro: order.strict_implies_order DERIV_pos_imp_increasing [where f=f] assms)
done
+ then have "flim \<le> f (b - 1)"
+ by (auto simp: trivial_limit_at_bot_linorder eventually_at_bot_linorder tendsto_upperbound [OF lim])
also have "\<dots> < f b"
by (force intro: DERIV_pos_imp_increasing [where f=f] assms)
finally show ?thesis .
--- a/src/HOL/Fields.thy Mon Sep 26 07:56:54 2016 +0200
+++ b/src/HOL/Fields.thy Wed Sep 28 17:01:01 2016 +0100
@@ -1192,6 +1192,20 @@
finally show ?thesis .
qed
+text\<open>For creating values between @{term u} and @{term v}.\<close>
+lemma scaling_mono:
+ assumes "u \<le> v" "0 \<le> r" "r \<le> s"
+ shows "u + r * (v - u) / s \<le> v"
+proof -
+ have "r/s \<le> 1" using assms
+ using divide_le_eq_1 by fastforce
+ then have "(r/s) * (v - u) \<le> 1 * (v - u)"
+ apply (rule mult_right_mono)
+ using assms by simp
+ then show ?thesis
+ by (simp add: field_simps)
+qed
+
end
text \<open>Min/max Simplification Rules\<close>
--- a/src/HOL/Groups_Big.thy Mon Sep 26 07:56:54 2016 +0200
+++ b/src/HOL/Groups_Big.thy Wed Sep 28 17:01:01 2016 +0100
@@ -47,6 +47,9 @@
lemma insert_remove: "finite A \<Longrightarrow> F g (insert x A) = g x \<^bold>* F g (A - {x})"
by (cases "x \<in> A") (simp_all add: remove insert_absorb)
+lemma insert_if: "finite A \<Longrightarrow> F g (insert x A) = (if x \<in> A then F g A else g x \<^bold>* F g A)"
+ by (cases "x \<in> A") (simp_all add: insert_absorb)
+
lemma neutral: "\<forall>x\<in>A. g x = \<^bold>1 \<Longrightarrow> F g A = \<^bold>1"
by (induct A rule: infinite_finite_induct) simp_all
@@ -1288,4 +1291,22 @@
qed
qed
+lemma setsum_image_le:
+ fixes g :: "'a \<Rightarrow> 'b::ordered_ab_group_add"
+ assumes "finite I" "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> g(f i)"
+ shows "setsum g (f ` I) \<le> setsum (g \<circ> f) I"
+ using assms
+proof induction
+ case empty
+ then show ?case by auto
+next
+ case (insert x F) then
+ have "setsum g (f ` insert x F) = setsum g (insert (f x) (f ` F))" by simp
+ also have "\<dots> \<le> g (f x) + setsum g (f ` F)"
+ by (simp add: insert setsum.insert_if)
+ also have "\<dots> \<le> setsum (g \<circ> f) (insert x F)"
+ using insert by auto
+ finally show ?case .
+qed
+
end
--- a/src/HOL/Library/Extended_Real.thy Mon Sep 26 07:56:54 2016 +0200
+++ b/src/HOL/Library/Extended_Real.thy Wed Sep 28 17:01:01 2016 +0100
@@ -3856,7 +3856,7 @@
assumes "eventually (\<lambda>x. f x \<ge> 0) F"
shows "((\<lambda>x. inverse (f x)) \<longlongrightarrow> inverse c) F"
by (cases "F = bot")
- (auto intro!: tendsto_le_const[of F] assms
+ (auto intro!: tendsto_lowerbound assms
continuous_on_tendsto_compose[OF continuous_on_inverse_ereal])
--- a/src/HOL/Limits.thy Mon Sep 26 07:56:54 2016 +0200
+++ b/src/HOL/Limits.thy Wed Sep 28 17:01:01 2016 +0100
@@ -2368,7 +2368,7 @@
fixes f :: "real \<Rightarrow> real"
assumes ev: "b < x" "\<forall> x' \<in> { b <..< x}. 0 \<le> f x'" and "isCont f x"
shows "0 \<le> f x"
-proof (rule tendsto_le_const)
+proof (rule tendsto_lowerbound)
show "(f \<longlongrightarrow> f x) (at_left x)"
using \<open>isCont f x\<close> by (simp add: filterlim_at_split isCont_def)
show "eventually (\<lambda>x. 0 \<le> f x) (at_left x)"
--- a/src/HOL/Order_Relation.thy Mon Sep 26 07:56:54 2016 +0200
+++ b/src/HOL/Order_Relation.thy Wed Sep 28 17:01:01 2016 +0100
@@ -397,6 +397,18 @@
ultimately show ?thesis unfolding R_def by blast
qed
+text\<open>A transitive relation is well-founded if all initial segments are finite.\<close>
+corollary wf_finite_segments:
+ assumes "irrefl r" and "trans r" and "\<And>x. finite {y. (y, x) \<in> r}"
+ shows "wf (r)"
+proof (clarsimp simp: trans_wf_iff wf_iff_acyclic_if_finite converse_def assms)
+ fix a
+ have "trans (r \<inter> ({x. (x, a) \<in> r} \<times> {x. (x, a) \<in> r}))"
+ using assms unfolding trans_def Field_def by blast
+ then show "acyclic (r \<inter> {x. (x, a) \<in> r} \<times> {x. (x, a) \<in> r})"
+ using assms acyclic_def assms irrefl_def by fastforce
+qed
+
text \<open>The next lemma is a variation of \<open>wf_eq_minimal\<close> from Wellfounded,
allowing one to assume the set included in the field.\<close>
--- a/src/HOL/Probability/Helly_Selection.thy Mon Sep 26 07:56:54 2016 +0200
+++ b/src/HOL/Probability/Helly_Selection.thy Wed Sep 28 17:01:01 2016 +0100
@@ -108,7 +108,7 @@
moreover have "(\<lambda>n. f (d n) x) \<longlonglongrightarrow> F x" if cts: "continuous (at x) F" for x
proof (rule limsup_le_liminf_real)
show "limsup (\<lambda>n. f (d n) x) \<le> F x"
- proof (rule tendsto_le_const)
+ proof (rule tendsto_lowerbound)
show "(F \<longlongrightarrow> ereal (F x)) (at_right x)"
using cts unfolding continuous_at_split by (auto simp: continuous_within)
show "\<forall>\<^sub>F i in at_right x. limsup (\<lambda>n. f (d n) x) \<le> F i"
@@ -128,7 +128,7 @@
qed
qed simp
show "F x \<le> liminf (\<lambda>n. f (d n) x)"
- proof (rule tendsto_ge_const)
+ proof (rule tendsto_upperbound)
show "(F \<longlongrightarrow> ereal (F x)) (at_left x)"
using cts unfolding continuous_at_split by (auto simp: continuous_within)
show "\<forall>\<^sub>F i in at_left x. F i \<le> liminf (\<lambda>n. f (d n) x)"
@@ -214,7 +214,7 @@
have "(\<lambda>k. ?\<mu> k {..b}) \<longlonglongrightarrow> F b"
using b(2) lim_F unfolding f_def cdf_def o_def by auto
then have "1 - \<epsilon> \<le> F b"
- proof (rule tendsto_le_const[OF sequentially_bot], intro always_eventually allI)
+ proof (rule tendsto_lowerbound, intro always_eventually allI)
fix k
have "1 - \<epsilon> < ?\<mu> k {a<..b}"
using ab by auto
@@ -222,20 +222,20 @@
by (auto intro!: \<mu>.finite_measure_mono)
finally show "1 - \<epsilon> \<le> ?\<mu> k {..b}"
by (rule less_imp_le)
- qed
+ qed (rule sequentially_bot)
then show "\<exists>b. \<forall>x\<ge>b. 1 - \<epsilon> \<le> F x"
using F unfolding mono_def by (metis order.trans)
have "(\<lambda>k. ?\<mu> k {..a}) \<longlonglongrightarrow> F a"
using a(2) lim_F unfolding f_def cdf_def o_def by auto
then have Fa: "F a \<le> \<epsilon>"
- proof (rule tendsto_ge_const[OF sequentially_bot], intro always_eventually allI)
+ proof (rule tendsto_upperbound, intro always_eventually allI)
fix k
have "?\<mu> k {..a} + ?\<mu> k {a<..b} \<le> 1"
by (subst \<mu>.finite_measure_Union[symmetric]) auto
then show "?\<mu> k {..a} \<le> \<epsilon>"
using ab[of k] by simp
- qed
+ qed (rule sequentially_bot)
then show "\<exists>a. \<forall>x\<le>a. F x \<le> \<epsilon>"
using F unfolding mono_def by (metis order.trans)
qed
--- a/src/HOL/Probability/Weak_Convergence.thy Mon Sep 26 07:56:54 2016 +0200
+++ b/src/HOL/Probability/Weak_Convergence.thy Wed Sep 28 17:01:01 2016 +0100
@@ -200,7 +200,7 @@
using \<omega>(2) by (auto intro: tendsto_within_subset simp: continuous_at)
show "limsup (\<lambda>n. \<mu>.I n \<omega>) \<le> M.I \<omega>"
using \<omega>
- by (intro tendsto_le_const[OF trivial_limit_at_right_real **])
+ by (intro tendsto_lowerbound[OF **])
(auto intro!: exI[of _ 1] * simp: eventually_at_right[of _ 1])
qed
@@ -391,12 +391,12 @@
} note ** = this
have "limsup (\<lambda>n. cdf (M_seq n) x) \<le> cdf M x"
- proof (rule tendsto_le_const)
+ proof (rule tendsto_lowerbound)
show "\<forall>\<^sub>F i in at_right x. limsup (\<lambda>xa. ereal (cdf (M_seq xa) x)) \<le> ereal (cdf M i)"
by (subst eventually_at_right[of _ "x + 1"]) (auto simp: * intro: exI [of _ "x+1"])
qed (insert cdf_is_right_cont, auto simp: continuous_within)
moreover have "cdf M x \<le> liminf (\<lambda>n. cdf (M_seq n) x)"
- proof (rule tendsto_ge_const)
+ proof (rule tendsto_upperbound)
show "\<forall>\<^sub>F i in at_left x. ereal (cdf M i) \<le> liminf (\<lambda>xa. ereal (cdf (M_seq xa) x))"
by (subst eventually_at_left[of "x - 1"]) (auto simp: ** intro: exI [of _ "x-1"])
qed (insert left_cont, auto simp: continuous_within)
--- a/src/HOL/Series.thy Mon Sep 26 07:56:54 2016 +0200
+++ b/src/HOL/Series.thy Wed Sep 28 17:01:01 2016 +0100
@@ -26,12 +26,16 @@
(binder "\<Sum>" 10)
where "suminf f = (THE s. f sums s)"
+text\<open>Variants of the definition\<close>
lemma sums_def': "f sums s \<longleftrightarrow> (\<lambda>n. \<Sum>i = 0..n. f i) \<longlonglongrightarrow> s"
apply (simp add: sums_def)
apply (subst LIMSEQ_Suc_iff [symmetric])
apply (simp only: lessThan_Suc_atMost atLeast0AtMost)
done
+lemma sums_def_le: "f sums s \<longleftrightarrow> (\<lambda>n. \<Sum>i\<le>n. f i) \<longlonglongrightarrow> s"
+ by (simp add: sums_def' atMost_atLeast0)
+
subsection \<open>Infinite summability on topological monoids\<close>
--- a/src/HOL/Set.thy Mon Sep 26 07:56:54 2016 +0200
+++ b/src/HOL/Set.thy Wed Sep 28 17:01:01 2016 +0100
@@ -1858,6 +1858,9 @@
definition disjnt :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool"
where "disjnt A B \<longleftrightarrow> A \<inter> B = {}"
+lemma disjnt_self_iff_empty [simp]: "disjnt S S \<longleftrightarrow> S = {}"
+ by (auto simp: disjnt_def)
+
lemma disjnt_iff: "disjnt A B \<longleftrightarrow> (\<forall>x. \<not> (x \<in> A \<and> x \<in> B))"
by (force simp: disjnt_def)
--- a/src/HOL/Topological_Spaces.thy Mon Sep 26 07:56:54 2016 +0200
+++ b/src/HOL/Topological_Spaces.thy Wed Sep 28 17:01:01 2016 +0100
@@ -884,19 +884,19 @@
by (simp add: eventually_False)
qed
-lemma tendsto_le_const:
+lemma tendsto_lowerbound:
fixes f :: "'a \<Rightarrow> 'b::linorder_topology"
- assumes F: "\<not> trivial_limit F"
- and x: "(f \<longlongrightarrow> x) F"
- and ev: "eventually (\<lambda>i. a \<le> f i) F"
+ assumes x: "(f \<longlongrightarrow> x) F"
+ and ev: "eventually (\<lambda>i. a \<le> f i) F"
+ and F: "\<not> trivial_limit F"
shows "a \<le> x"
using F x tendsto_const ev by (rule tendsto_le)
-lemma tendsto_ge_const:
+lemma tendsto_upperbound:
fixes f :: "'a \<Rightarrow> 'b::linorder_topology"
- assumes F: "\<not> trivial_limit F"
- and x: "(f \<longlongrightarrow> x) F"
- and ev: "eventually (\<lambda>i. a \<ge> f i) F"
+ assumes x: "(f \<longlongrightarrow> x) F"
+ and ev: "eventually (\<lambda>i. a \<ge> f i) F"
+ and F: "\<not> trivial_limit F"
shows "a \<ge> x"
by (rule tendsto_le [OF F tendsto_const x ev])
@@ -1256,7 +1256,7 @@
lemma LIMSEQ_le_const: "X \<longlonglongrightarrow> x \<Longrightarrow> \<exists>N. \<forall>n\<ge>N. a \<le> X n \<Longrightarrow> a \<le> x"
for a x :: "'a::linorder_topology"
- using tendsto_le_const[of sequentially X x a] by (simp add: eventually_sequentially)
+ by (simp add: eventually_at_top_linorder tendsto_lowerbound)
lemma LIMSEQ_le: "X \<longlonglongrightarrow> x \<Longrightarrow> Y \<longlonglongrightarrow> y \<Longrightarrow> \<exists>N. \<forall>n\<ge>N. X n \<le> Y n \<Longrightarrow> x \<le> y"
for x y :: "'a::linorder_topology"