--- a/src/HOL/Analysis/Bochner_Integration.thy Tue May 02 15:29:45 2017 +0200
+++ b/src/HOL/Analysis/Bochner_Integration.thy Tue May 02 18:27:51 2017 +0200
@@ -444,7 +444,7 @@
lemma simple_bochner_integral_nonneg[simp]:
fixes f :: "'a \<Rightarrow> real"
shows "(\<And>x. 0 \<le> f x) \<Longrightarrow> 0 \<le> simple_bochner_integral M f"
- by (simp add: sum_nonneg simple_bochner_integral_def)
+ by (force simp add: simple_bochner_integral_def intro: sum_nonneg)
lemma simple_bochner_integral_eq_nn_integral:
assumes f: "simple_bochner_integrable M f" "\<And>x. 0 \<le> f x"
--- a/src/HOL/Analysis/Caratheodory.thy Tue May 02 15:29:45 2017 +0200
+++ b/src/HOL/Analysis/Caratheodory.thy Tue May 02 18:27:51 2017 +0200
@@ -30,7 +30,7 @@
then have "a < ?M fst" "b < ?M snd"
by (auto intro!: Max_ge le_imp_less_Suc image_eqI) }
then have "sum f (prod_decode ` {..<n}) \<le> sum f ({..<?M fst} \<times> {..<?M snd})"
- by (auto intro!: sum_mono3)
+ by (auto intro!: sum_mono2)
then show "\<exists>a b. sum f (prod_decode ` {..<n}) \<le> sum f ({..<a} \<times> {..<b})" by auto
next
fix a b
@@ -38,7 +38,7 @@
{ fix a' b' assume "a' < a" "b' < b" then have "(a', b') \<in> ?M"
by (auto intro!: Max_ge le_imp_less_Suc image_eqI[where x="prod_encode (a', b')"]) }
then have "sum f ({..<a} \<times> {..<b}) \<le> sum f ?M"
- by (auto intro!: sum_mono3)
+ by (auto intro!: sum_mono2)
then show "\<exists>n. sum f ({..<a} \<times> {..<b}) \<le> sum f (prod_decode ` {..<n})"
by auto
qed
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Tue May 02 15:29:45 2017 +0200
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Tue May 02 18:27:51 2017 +0200
@@ -1969,23 +1969,7 @@
qed auto
qed
note p'= tagged_division_ofD[OF p[THEN conjunct1]] and p''=division_of_tagged_division[OF p[THEN conjunct1]]
- show "norm ((\<Sum>(x, ka)\<in>p. content ka *\<^sub>R ?i x) - 0) < e"
- unfolding diff_0_right *
- unfolding real_scaleR_def real_norm_def
- apply (subst abs_of_nonneg)
- apply (rule sum_nonneg)
- apply rule
- unfolding split_paired_all split_conv
- apply (rule mult_nonneg_nonneg)
- apply (drule p'(4))
- apply (erule exE)+
- apply(rule_tac b=b in back_subst)
- prefer 2
- apply (subst(asm) eq_commute)
- apply assumption
- apply (subst interval_doublesplit[OF k])
- apply (rule content_pos_le)
- apply (rule indicator_pos_le)
+ have "(\<Sum>(x, ka)\<in>p. content (ka \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) * indicator {x. x \<bullet> k = c} x) < e"
proof -
have "(\<Sum>(x, ka)\<in>p. content (ka \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) * ?i x) \<le>
(\<Sum>(x, ka)\<in>p. content (ka \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}))"
@@ -2037,11 +2021,14 @@
qed
finally show "(\<Sum>(x, ka)\<in>p. content (ka \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) * ?i x) < e" .
qed
+ then show "norm ((\<Sum>(x, ka)\<in>p. content ka *\<^sub>R ?i x) - 0) < e"
+ unfolding * real_norm_def
+ apply (subst abs_of_nonneg)
+ using measure_nonneg by (force simp add: indicator_def intro: sum_nonneg)+
qed
qed
-
subsection \<open>Hence the main theorem about negligible sets.\<close>
lemma has_integral_negligible:
@@ -3876,26 +3863,17 @@
have *: "\<And>x s1 s2::real. 0 \<le> s1 \<Longrightarrow> x \<le> (s1 + s2) / 2 \<Longrightarrow> x - s1 \<le> s2 / 2"
by auto
case 2
- show ?case
- apply (rule *)
- apply (rule sum_nonneg)
- apply rule
- apply (unfold split_paired_all split_conv)
- defer
- unfolding sum.union_disjoint[OF pA(2-),symmetric] pA(1)[symmetric]
- unfolding sum_distrib_left[symmetric]
- apply (subst additive_tagged_division_1[OF _ as(1)])
- apply (rule assms)
+ have ge0: "0 \<le> e * (Sup k - Inf k)" if xkp: "(x, k) \<in> p \<inter> {t. fst t \<in> {a, b}}" for x k
proof -
- fix x k
- assume "(x, k) \<in> p \<inter> {t. fst t \<in> {a, b}}"
- note xk=IntD1[OF this]
- from p(4)[OF this] guess u v by (elim exE) note uv=this
- with p(2)[OF xk] have "cbox u v \<noteq> {}"
- by auto
+ obtain u v where uv: "k = cbox u v"
+ by (meson Int_iff xkp p(4))
+ with p(2) that uv have "cbox u v \<noteq> {}"
+ by blast
then show "0 \<le> e * ((Sup k) - (Inf k))"
unfolding uv using e by (auto simp add: field_simps)
- next
+ qed
+ have **: "norm (\<Sum>(x, k)\<in>p \<inter> {t. fst t \<in> {a, b}}. content k *\<^sub>R f' x - (f (Sup k) - f (Inf k))) \<le> e * (b - a) / 2"
+ proof -
have *: "\<And>s f t e. sum f s = sum f t \<Longrightarrow> norm (sum f t) \<le> e \<Longrightarrow> norm (sum f s) \<le> e"
by auto
show "norm (\<Sum>(x, k)\<in>p \<inter> ?A. content k *\<^sub>R f' x -
@@ -4122,6 +4100,15 @@
qed (insert p(1) ab e, auto simp add: field_simps)
qed auto
qed
+ show ?case
+ apply (rule * [OF sum_nonneg])
+ using ge0 apply (force simp add: )
+ unfolding sum.union_disjoint[OF pA(2-),symmetric] pA(1)[symmetric]
+ unfolding sum_distrib_left[symmetric]
+ apply (subst additive_tagged_division_1[OF _ as(1)])
+ apply (rule assms)
+ apply (rule **)
+ done
qed
qed
qed
--- a/src/HOL/Analysis/Lebesgue_Measure.thy Tue May 02 15:29:45 2017 +0200
+++ b/src/HOL/Analysis/Lebesgue_Measure.thy Tue May 02 18:27:51 2017 +0200
@@ -281,7 +281,7 @@
also have "... = (\<Sum>i\<in>S. F (r i) - F (l i)) + epsilon"
by auto
also have "... \<le> (\<Sum>i\<le>n. F (r i) - F (l i)) + epsilon"
- using finS Sbound Sprop by (auto intro!: add_right_mono sum_mono3)
+ using finS Sbound Sprop by (auto intro!: add_right_mono sum_mono2)
finally have "ennreal (F b - F a) \<le> (\<Sum>i\<le>n. ennreal (F (r i) - F (l i))) + epsilon"
using egt0 by (simp add: ennreal_plus[symmetric] sum_nonneg del: ennreal_plus)
then show "ennreal (F b - F a) \<le> (\<Sum>i. ennreal (F (r i) - F (l i))) + (epsilon :: real)"
--- a/src/HOL/Analysis/Linear_Algebra.thy Tue May 02 15:29:45 2017 +0200
+++ b/src/HOL/Analysis/Linear_Algebra.thy Tue May 02 18:27:51 2017 +0200
@@ -1480,12 +1480,6 @@
and "finite S \<Longrightarrow> sum f (insert x S) = (if x \<in> S then sum f S else f x + sum f S)"
by (auto simp add: insert_absorb)
-lemma sum_norm_le:
- fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
- assumes fg: "\<And>x. x \<in> S \<Longrightarrow> norm (f x) \<le> g x"
- shows "norm (sum f S) \<le> sum g S"
- by (rule order_trans [OF norm_sum sum_mono]) (simp add: fg)
-
lemma sum_norm_bound:
fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
assumes K: "\<And>x. x \<in> S \<Longrightarrow> norm (f x) \<le> K"
--- a/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy Tue May 02 15:29:45 2017 +0200
+++ b/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy Tue May 02 18:27:51 2017 +0200
@@ -1143,7 +1143,7 @@
unfolding nn_integral_sum[OF f] ..
also have "\<dots> = \<integral>\<^sup>+x. (SUP n. \<Sum>i<n. f i x) \<partial>M" using f all_pos
by (intro nn_integral_monotone_convergence_SUP_AE[symmetric])
- (elim AE_mp, auto simp: sum_nonneg simp del: sum_lessThan_Suc intro!: AE_I2 sum_mono3)
+ (elim AE_mp, auto simp: sum_nonneg simp del: sum_lessThan_Suc intro!: AE_I2 sum_mono2)
also have "\<dots> = \<integral>\<^sup>+x. (\<Sum>i. f i x) \<partial>M" using all_pos
by (intro nn_integral_cong_AE) (auto simp: suminf_eq_SUP)
finally show ?thesis by simp
--- a/src/HOL/Analysis/Polytope.thy Tue May 02 15:29:45 2017 +0200
+++ b/src/HOL/Analysis/Polytope.thy Tue May 02 18:27:51 2017 +0200
@@ -311,7 +311,7 @@
proof (cases "sum c (S - T) = 0")
case True
have ci0: "\<And>i. i \<in> (S - T) \<Longrightarrow> c i = 0"
- using True cge0 by (simp add: \<open>finite S\<close> sum_nonneg_eq_0_iff)
+ using True cge0 fin(2) sum_nonneg_eq_0_iff by auto
have a0: "a i = 0" if "i \<in> (S - T)" for i
using ci0 [OF that] u01 a [of i] b [of i] that
by (simp add: c_def Groups.ordered_comm_monoid_add_class.add_nonneg_eq_0_iff)
@@ -2775,7 +2775,7 @@
by (simp add: \<open>0 < e\<close>)
finally show ?thesis .
qed
- qed (auto simp: eq poly aff face \<open>finite \<F>'\<close>)
+ qed (auto simp: eq poly aff face \<open>finite \<F>'\<close>)
qed
end
--- a/src/HOL/Groups_Big.thy Tue May 02 15:29:45 2017 +0200
+++ b/src/HOL/Groups_Big.thy Tue May 02 18:27:51 2017 +0200
@@ -675,7 +675,7 @@
context ordered_comm_monoid_add
begin
-lemma sum_nonneg: "\<forall>x\<in>A. 0 \<le> f x \<Longrightarrow> 0 \<le> sum f A"
+lemma sum_nonneg: "(\<And>x. x \<in> A \<Longrightarrow> 0 \<le> f x) \<Longrightarrow> 0 \<le> sum f A"
proof (induct A rule: infinite_finite_induct)
case infinite
then show ?case by simp
@@ -688,7 +688,7 @@
with insert show ?case by simp
qed
-lemma sum_nonpos: "\<forall>x\<in>A. f x \<le> 0 \<Longrightarrow> sum f A \<le> 0"
+lemma sum_nonpos: "(\<And>x. x \<in> A \<Longrightarrow> f x \<le> 0) \<Longrightarrow> sum f A \<le> 0"
proof (induct A rule: infinite_finite_induct)
case infinite
then show ?case by simp
@@ -702,7 +702,7 @@
qed
lemma sum_nonneg_eq_0_iff:
- "finite A \<Longrightarrow> \<forall>x\<in>A. 0 \<le> f x \<Longrightarrow> sum f A = 0 \<longleftrightarrow> (\<forall>x\<in>A. f x = 0)"
+ "finite A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> 0 \<le> f x) \<Longrightarrow> sum f A = 0 \<longleftrightarrow> (\<forall>x\<in>A. f x = 0)"
by (induct set: finite) (simp_all add: add_nonneg_eq_0_iff sum_nonneg)
lemma sum_nonneg_0:
@@ -727,7 +727,7 @@
shows "sum f A \<le> sum f B"
proof -
have "sum f A \<le> sum f A + sum f (B-A)"
- by(simp add: add_increasing2[OF sum_nonneg] nn Ball_def)
+ by (auto intro: add_increasing2 [OF sum_nonneg] nn)
also from fin finite_subset[OF sub fin] have "\<dots> = sum f (A \<union> (B-A))"
by (simp add: sum.union_disjoint del: Un_Diff_cancel)
also from sub have "A \<union> (B-A) = B" by blast
@@ -755,9 +755,6 @@
finally show ?thesis .
qed
-lemma sum_mono3: "finite B \<Longrightarrow> A \<subseteq> B \<Longrightarrow> \<forall>x\<in>B - A. 0 \<le> f x \<Longrightarrow> sum f A \<le> sum f B"
- by (rule sum_mono2) auto
-
end
lemma (in canonically_ordered_monoid_add) sum_eq_0_iff [simp]:
@@ -1210,12 +1207,19 @@
for c :: "nat \<Rightarrow> 'a::field"
using sum_zero_power [of "\<lambda>i. c i / d i" A] by auto
-lemma (in field) prod_inversef:
- "finite A \<Longrightarrow> prod (inverse \<circ> f) A = inverse (prod f A)"
- by (induct A rule: finite_induct) simp_all
+lemma (in field) prod_inversef: "prod (inverse \<circ> f) A = inverse (prod f A)"
+ proof (cases "finite A")
+ case True
+ then show ?thesis
+ by (induct A rule: finite_induct) simp_all
+ next
+ case False
+ then show ?thesis
+ by auto
+ qed
-lemma (in field) prod_dividef: "finite A \<Longrightarrow> (\<Prod>x\<in>A. f x / g x) = prod f A / prod g A"
- using prod_inversef [of A g] by (simp add: divide_inverse prod.distrib)
+lemma (in field) prod_dividef: "(\<Prod>x\<in>A. f x / g x) = prod f A / prod g A"
+ using prod_inversef [of g A] by (simp add: divide_inverse prod.distrib)
lemma prod_Un:
fixes f :: "'b \<Rightarrow> 'a :: field"
--- a/src/HOL/Library/Extended_Nonnegative_Real.thy Tue May 02 15:29:45 2017 +0200
+++ b/src/HOL/Library/Extended_Nonnegative_Real.thy Tue May 02 18:27:51 2017 +0200
@@ -223,7 +223,7 @@
lemma suminf_eq_SUP_real:
assumes X: "summable X" "\<And>i. 0 \<le> X i" shows "suminf X = (SUP i. \<Sum>n<i. X n::real)"
by (intro LIMSEQ_unique[OF summable_LIMSEQ] X LIMSEQ_incseq_SUP)
- (auto intro!: bdd_aboveI2[where M="\<Sum>i. X i"] sum_le_suminf X monoI sum_mono3)
+ (auto intro!: bdd_aboveI2[where M="\<Sum>i. X i"] sum_le_suminf X monoI sum_mono2)
subsection \<open>Defining the extended non-negative reals\<close>
--- a/src/HOL/Library/Extended_Real.thy Tue May 02 15:29:45 2017 +0200
+++ b/src/HOL/Library/Extended_Real.thy Tue May 02 18:27:51 2017 +0200
@@ -3394,7 +3394,7 @@
also have "\<dots> = (\<Sum>i\<in>(\<lambda>i. i + k) ` {..<n}. f i)"
by (subst sum.reindex) auto
also have "\<dots> \<le> sum f {..<n + k}"
- by (intro sum_mono3) (auto simp: f)
+ by (intro sum_mono2) (auto simp: f)
finally show "(\<Sum>i<n. f (i + k)) \<le> sum f {..<n + k}" .
qed
qed
--- a/src/HOL/Limits.thy Tue May 02 15:29:45 2017 +0200
+++ b/src/HOL/Limits.thy Tue May 02 18:27:51 2017 +0200
@@ -824,6 +824,10 @@
for f :: "'a \<Rightarrow> 'b::{power,real_normed_algebra}"
by (induct n) (simp_all add: tendsto_mult)
+lemma tendsto_null_power: "\<lbrakk>(f \<longlongrightarrow> 0) F; 0 < n\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x ^ n) \<longlongrightarrow> 0) F"
+ for f :: "'a \<Rightarrow> 'b::{power,real_normed_algebra_1}"
+ using tendsto_power [of f 0 F n] by (simp add: power_0_left)
+
lemma continuous_power [continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. (f x)^n)"
for f :: "'a::t2_space \<Rightarrow> 'b::{power,real_normed_algebra}"
unfolding continuous_def by (rule tendsto_power)
--- a/src/HOL/Real_Vector_Spaces.thy Tue May 02 15:29:45 2017 +0200
+++ b/src/HOL/Real_Vector_Spaces.thy Tue May 02 18:27:51 2017 +0200
@@ -871,7 +871,7 @@
lemma sum_norm_le:
fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
- assumes fg: "\<forall>x \<in> S. norm (f x) \<le> g x"
+ assumes fg: "\<And>x. x \<in> S \<Longrightarrow> norm (f x) \<le> g x"
shows "norm (sum f S) \<le> sum g S"
by (rule order_trans [OF norm_sum sum_mono]) (simp add: fg)
--- a/src/HOL/Series.thy Tue May 02 15:29:45 2017 +0200
+++ b/src/HOL/Series.thy Tue May 02 18:27:51 2017 +0200
@@ -1062,7 +1062,7 @@
have "(\<Sum>i<n. f (g i)) = sum f (g ` {..<n})"
by (simp add: sum.reindex)
also have "\<dots> \<le> (\<Sum>i<m. f i)"
- by (rule sum_mono3) (auto simp add: pos n[rule_format])
+ by (rule sum_mono2) (auto simp add: pos n[rule_format])
also have "\<dots> \<le> suminf f"
using \<open>summable f\<close> by (rule sum_le_suminf) (simp add: pos)
finally show "(\<Sum>i<n. (f \<circ> g) i) \<le> suminf f"
@@ -1097,7 +1097,7 @@
also have "\<dots> = (\<Sum>i\<in>g -` {..<n}. (f \<circ> g) i)"
by (rule sum.reindex_cong[where l=g])(auto)
also have "\<dots> \<le> (\<Sum>i<m. (f \<circ> g) i)"
- by (rule sum_mono3)(auto simp add: pos n)
+ by (rule sum_mono2)(auto simp add: pos n)
also have "\<dots> \<le> suminf (f \<circ> g)"
using \<open>summable (f \<circ> g)\<close> by (rule sum_le_suminf) (simp add: pos)
finally show "sum f {..<n} \<le> suminf (f \<circ> g)" .
--- a/src/HOL/Transcendental.thy Tue May 02 15:29:45 2017 +0200
+++ b/src/HOL/Transcendental.thy Tue May 02 18:27:51 2017 +0200
@@ -197,7 +197,7 @@
also have "(\<Sum>k\<in>{0,2*n}. (2*n) choose k) \<le> (\<Sum>k\<le>1. (n choose k)\<^sup>2)"
by (cases n) simp_all
also from assms have "\<dots> \<le> (\<Sum>k\<le>n. (n choose k)\<^sup>2)"
- by (intro sum_mono3) auto
+ by (intro sum_mono2) auto
also have "\<dots> = (2*n) choose n" by (rule choose_square_sum)
also have "(\<Sum>k\<in>{0<..<2*n}. (2*n) choose k) \<le> (\<Sum>k\<in>{0<..<2*n}. (2*n) choose n)"
by (intro sum_mono binomial_maximum')
@@ -1774,13 +1774,13 @@
for x :: real
by (simp add: order_eq_iff)
-lemma ln_add_one_self_le_self [simp]: "0 \<le> x \<Longrightarrow> ln (1 + x) \<le> x"
+lemma ln_add_one_self_le_self: "0 \<le> x \<Longrightarrow> ln (1 + x) \<le> x"
for x :: real
by (rule exp_le_cancel_iff [THEN iffD1]) (simp add: exp_ge_add_one_self_aux)
lemma ln_less_self [simp]: "0 < x \<Longrightarrow> ln x < x"
for x :: real
- by (rule order_less_le_trans [where y = "ln (1 + x)"]) simp_all
+ by (rule order_less_le_trans [where y = "ln (1 + x)"]) (simp_all add: ln_add_one_self_le_self)
lemma ln_ge_iff: "\<And>x::real. 0 < x \<Longrightarrow> y \<le> ln x \<longleftrightarrow> exp y \<le> x"
using exp_le_cancel_iff exp_total by force