# HG changeset patch # User nipkow # Date 1298668076 -3600 # Node ID 96184364aa6f5fb7536cceda2435f0cafc016325 # Parent edfc06b8a507b9e89a91fde6ced0b51bb9f3d4ed got rid of lemma upper_bound_finite_set diff -r edfc06b8a507 -r 96184364aa6f src/HOL/Multivariate_Analysis/Integration.thy --- a/src/HOL/Multivariate_Analysis/Integration.thy Fri Feb 25 20:08:00 2011 +0100 +++ b/src/HOL/Multivariate_Analysis/Integration.thy Fri Feb 25 22:07:56 2011 +0100 @@ -4473,6 +4473,24 @@ subsection {* monotone convergence (bounded interval first). *} +lemma upper_bound_finite_set: + assumes fS: "finite S" + shows "\(a::'a::linorder). \x \ S. f x \ a" +proof(induct rule: finite_induct[OF fS]) + case 1 thus ?case by simp +next + case (2 x F) + from "2.hyps" obtain a where a:"\x \F. f x \ a" by blast + let ?a = "max a (f x)" + have m: "a \ ?a" "f x \ ?a" by simp_all + {fix y assume y: "y \ insert x F" + {assume "y = x" hence "f y \ ?a" using m by simp} + moreover + {assume yF: "y\ F" from a[rule_format, OF yF] m have "f y \ ?a" by (simp add: max_def)} + ultimately have "f y \ ?a" using y by blast} + then show ?case by blast +qed + lemma monotone_convergence_interval: fixes f::"nat \ 'n::ordered_euclidean_space \ real" assumes "\k. (f k) integrable_on {a..b}" "\k. \x\{a..b}.(f k x) \ (f (Suc k) x)" @@ -4530,7 +4548,8 @@ proof safe show "gauge d" using c(1) unfolding gauge_def d_def by auto next fix p assume p:"p tagged_division_of {a..b}" "d fine p" note p'=tagged_division_ofD[OF p(1)] - have "\a. \x\p. m (fst x) \ a" by(rule upper_bound_finite_set,fact) + have "\a. \x\p. m (fst x) \ a" + by (metis finite_imageI finite_nat_set_iff_bounded_le p'(1) rev_image_eqI) then guess s .. note s=this have *:"\a b c d. norm(a - b) \ e / 4 \ norm(b - c) < e / 2 \ norm(c - d) < e / 4 \ norm(a - d) < e"