# HG changeset patch # User wenzelm # Date 1379195938 -7200 # Node ID b19242603e926edab79c8db6412f3757ae16cba8 # Parent f8147d885600722c37a25e00230c71d8c95a1938# Parent 3170b5eb9f5a22e3906fcaf925c10328d96c4634 merged diff -r f8147d885600 -r b19242603e92 src/HOL/Multivariate_Analysis/Integration.thy --- a/src/HOL/Multivariate_Analysis/Integration.thy Sat Sep 14 22:34:25 2013 +0200 +++ b/src/HOL/Multivariate_Analysis/Integration.thy Sat Sep 14 23:58:58 2013 +0200 @@ -5018,7 +5018,7 @@ case False then have *: "content {a..b} = 0" using content_lt_nz by auto - hence **: "i = 0" + then have **: "i = 0" using assms(2) apply (subst has_integral_null_eq[symmetric]) apply auto @@ -9616,295 +9616,697 @@ qed qed -lemma integrable_straddle: fixes f::"'n::ordered_euclidean_space \ real" +lemma integrable_straddle: + fixes f :: "'n::ordered_euclidean_space \ real" assumes "\e>0. \g h i j. (g has_integral i) s \ (h has_integral j) s \ - norm(i - j) < e \ (\x\s. (g x) \(f x) \(f x) \(h x))" + norm (i - j) < e \ (\x\s. g x \ f x \ f x \ h x)" shows "f integrable_on s" -proof- have "\a b. (\x. if x \ s then f x else 0) integrable_on {a..b}" - proof(rule integrable_straddle_interval,safe) case goal1 hence *:"e/4 > 0" by auto - from assms[rule_format,OF this] guess g h i j apply-by(erule exE conjE)+ note obt=this - note obt(1)[unfolded has_integral_alt'[of g]] note conjunctD2[OF this, rule_format] - note g = this(1) and this(2)[OF *] from this(2) guess B1 .. note B1 = conjunctD2[OF this,rule_format] - note obt(2)[unfolded has_integral_alt'[of h]] note conjunctD2[OF this, rule_format] - note h = this(1) and this(2)[OF *] from this(2) guess B2 .. note B2 = conjunctD2[OF this,rule_format] +proof - + have "\a b. (\x. if x \ s then f x else 0) integrable_on {a..b}" + proof (rule integrable_straddle_interval, safe) + case goal1 + then have *: "e/4 > 0" + by auto + from assms[rule_format,OF this] guess g h i j by (elim exE conjE) note obt=this + note obt(1)[unfolded has_integral_alt'[of g]] + note conjunctD2[OF this, rule_format] + note g = this(1) and this(2)[OF *] + from this(2) guess B1 .. note B1 = conjunctD2[OF this,rule_format] + note obt(2)[unfolded has_integral_alt'[of h]] + note conjunctD2[OF this, rule_format] + note h = this(1) and this(2)[OF *] + from this(2) guess B2 .. note B2 = conjunctD2[OF this,rule_format] def c \ "\i\Basis. min (a\i) (- (max B1 B2)) *\<^sub>R i::'n" def d \ "\i\Basis. max (b\i) (max B1 B2) *\<^sub>R i::'n" - have *:"ball 0 B1 \ {c..d}" "ball 0 B2 \ {c..d}" - apply safe unfolding mem_ball mem_interval dist_norm - proof(rule_tac[!] ballI) - case goal1 thus ?case using Basis_le_norm[of i x] unfolding c_def d_def by auto next - case goal2 thus ?case using Basis_le_norm[of i x] unfolding c_def d_def by auto qed - have **:"\ch cg ag ah::real. norm(ah - ag) \ norm(ch - cg) \ norm(cg - i) < e / 4 \ - norm(ch - j) < e / 4 \ norm(ag - ah) < e" - using obt(3) unfolding real_norm_def by arith - show ?case apply(rule_tac x="\x. if x \ s then g x else 0" in exI) - apply(rule_tac x="\x. if x \ s then h x else 0" in exI) - apply(rule_tac x="integral {a..b} (\x. if x \ s then g x else 0)" in exI) - apply(rule_tac x="integral {a..b} (\x. if x \ s then h x else 0)" in exI) - apply safe apply(rule_tac[1-2] integrable_integral,rule g,rule h) - apply(rule **[OF _ B1(2)[OF *(1)] B2(2)[OF *(2)]]) - proof- have *:"\x f g. (if x \ s then f x else 0) - (if x \ s then g x else 0) = - (if x \ s then f x - g x else (0::real))" by auto + have *: "ball 0 B1 \ {c..d}" "ball 0 B2 \ {c..d}" + apply safe + unfolding mem_ball mem_interval dist_norm + apply (rule_tac[!] ballI) + proof - + case goal1 + then show ?case using Basis_le_norm[of i x] + unfolding c_def d_def by auto + next + case goal2 + then show ?case using Basis_le_norm[of i x] + unfolding c_def d_def by auto + qed + have **:" \ch cg ag ah::real. norm (ah - ag) \ norm (ch - cg) \ norm (cg - i) < e / 4 \ + norm (ch - j) < e / 4 \ norm (ag - ah) < e" + using obt(3) + unfolding real_norm_def + by arith + show ?case + apply (rule_tac x="\x. if x \ s then g x else 0" in exI) + apply (rule_tac x="\x. if x \ s then h x else 0" in exI) + apply (rule_tac x="integral {a..b} (\x. if x \ s then g x else 0)" in exI) + apply (rule_tac x="integral {a..b} (\x. if x \ s then h x else 0)" in exI) + apply safe + apply (rule_tac[1-2] integrable_integral,rule g) + apply (rule h) + apply (rule **[OF _ B1(2)[OF *(1)] B2(2)[OF *(2)]]) + proof - + have *: "\x f g. (if x \ s then f x else 0) - (if x \ s then g x else 0) = + (if x \ s then f x - g x else (0::real))" + by auto note ** = abs_of_nonneg[OF integral_nonneg[OF integrable_sub, OF h g]] - show " norm (integral {a..b} (\x. if x \ s then h x else 0) - - integral {a..b} (\x. if x \ s then g x else 0)) - \ norm (integral {c..d} (\x. if x \ s then h x else 0) - - integral {c..d} (\x. if x \ s then g x else 0))" - unfolding integral_sub[OF h g,symmetric] real_norm_def apply(subst **) defer apply(subst **) defer - apply(rule has_integral_subset_le) defer apply(rule integrable_integral integrable_sub h g)+ - proof safe fix x assume "x\{a..b}" thus "x\{c..d}" unfolding mem_interval c_def d_def - apply - apply rule apply(erule_tac x=i in ballE) by auto - qed(insert obt(4), auto) qed(insert obt(4), auto) qed note interv = this - - show ?thesis unfolding integrable_alt[of f] apply safe apply(rule interv) - proof- case goal1 hence *:"e/3 > 0" by auto - from assms[rule_format,OF this] guess g h i j apply-by(erule exE conjE)+ note obt=this - note obt(1)[unfolded has_integral_alt'[of g]] note conjunctD2[OF this, rule_format] - note g = this(1) and this(2)[OF *] from this(2) guess B1 .. note B1 = conjunctD2[OF this,rule_format] - note obt(2)[unfolded has_integral_alt'[of h]] note conjunctD2[OF this, rule_format] - note h = this(1) and this(2)[OF *] from this(2) guess B2 .. note B2 = conjunctD2[OF this,rule_format] - show ?case apply(rule_tac x="max B1 B2" in exI) apply safe apply(rule min_max.less_supI1,rule B1) - proof- fix a b c d::"'n::ordered_euclidean_space" assume as:"ball 0 (max B1 B2) \ {a..b}" "ball 0 (max B1 B2) \ {c..d}" - have **:"ball 0 B1 \ ball (0::'n::ordered_euclidean_space) (max B1 B2)" "ball 0 B2 \ ball (0::'n::ordered_euclidean_space) (max B1 B2)" by auto - have *:"\ga gc ha hc fa fc::real. abs(ga - i) < e / 3 \ abs(gc - i) < e / 3 \ abs(ha - j) < e / 3 \ - abs(hc - j) < e / 3 \ abs(i - j) < e / 3 \ ga \ fa \ fa \ ha \ gc \ fc \ fc \ hc\ abs(fa - fc) < e" + show "norm (integral {a..b} (\x. if x \ s then h x else 0) - + integral {a..b} (\x. if x \ s then g x else 0)) \ + norm (integral {c..d} (\x. if x \ s then h x else 0) - + integral {c..d} (\x. if x \ s then g x else 0))" + unfolding integral_sub[OF h g,symmetric] real_norm_def + apply (subst **) + defer + apply (subst **) + defer + apply (rule has_integral_subset_le) + defer + apply (rule integrable_integral integrable_sub h g)+ + proof safe + fix x + assume "x \ {a..b}" + then show "x \ {c..d}" + unfolding mem_interval c_def d_def + apply - + apply rule + apply (erule_tac x=i in ballE) + apply auto + done + qed (insert obt(4), auto) + qed (insert obt(4), auto) + qed + note interv = this + + show ?thesis + unfolding integrable_alt[of f] + apply safe + apply (rule interv) + proof - + case goal1 + then have *: "e/3 > 0" + by auto + from assms[rule_format,OF this] guess g h i j by (elim exE conjE) note obt=this + note obt(1)[unfolded has_integral_alt'[of g]] + note conjunctD2[OF this, rule_format] + note g = this(1) and this(2)[OF *] + from this(2) guess B1 .. note B1 = conjunctD2[OF this,rule_format] + note obt(2)[unfolded has_integral_alt'[of h]] + note conjunctD2[OF this, rule_format] + note h = this(1) and this(2)[OF *] + from this(2) guess B2 .. note B2 = conjunctD2[OF this,rule_format] + show ?case + apply (rule_tac x="max B1 B2" in exI) + apply safe + apply (rule min_max.less_supI1) + apply (rule B1) + proof - + fix a b c d :: 'n + assume as: "ball 0 (max B1 B2) \ {a..b}" "ball 0 (max B1 B2) \ {c..d}" + have **: "ball 0 B1 \ ball (0::'n) (max B1 B2)" "ball 0 B2 \ ball (0::'n) (max B1 B2)" + by auto + have *: "\ga gc ha hc fa fc::real. + abs (ga - i) < e / 3 \ abs (gc - i) < e / 3 \ abs (ha - j) < e / 3 \ + abs (hc - j) < e / 3 \ abs (i - j) < e / 3 \ ga \ fa \ fa \ ha \ gc \ fc \ fc \ hc \ + abs (fa - fc) < e" by (simp add: abs_real_def split: split_if_asm) - show "norm (integral {a..b} (\x. if x \ s then f x else 0) - integral {c..d} (\x. if x \ s then f x else 0)) < e" - unfolding real_norm_def apply(rule *, safe) unfolding real_norm_def[symmetric] - apply(rule B1(2),rule order_trans,rule **,rule as(1)) - apply(rule B1(2),rule order_trans,rule **,rule as(2)) - apply(rule B2(2),rule order_trans,rule **,rule as(1)) - apply(rule B2(2),rule order_trans,rule **,rule as(2)) - apply(rule obt) apply(rule_tac[!] integral_le) using obt - by(auto intro!: h g interv) qed qed qed - -subsection {* Adding integrals over several sets. *} - -lemma has_integral_union: fixes f::"'n::ordered_euclidean_space \ 'a::banach" - assumes "(f has_integral i) s" "(f has_integral j) t" "negligible(s \ t)" + show "norm (integral {a..b} (\x. if x \ s then f x else 0) - integral {c..d} + (\x. if x \ s then f x else 0)) < e" + unfolding real_norm_def + apply (rule *) + apply safe + unfolding real_norm_def[symmetric] + apply (rule B1(2)) + apply (rule order_trans) + apply (rule **) + apply (rule as(1)) + apply (rule B1(2)) + apply (rule order_trans) + apply (rule **) + apply (rule as(2)) + apply (rule B2(2)) + apply (rule order_trans) + apply (rule **) + apply (rule as(1)) + apply (rule B2(2)) + apply (rule order_trans) + apply (rule **) + apply (rule as(2)) + apply (rule obt) + apply (rule_tac[!] integral_le) + using obt + apply (auto intro!: h g interv) + done + qed + qed +qed + + +subsection {* Adding integrals over several sets *} + +lemma has_integral_union: + fixes f :: "'n::ordered_euclidean_space \ 'a::banach" + assumes "(f has_integral i) s" + and "(f has_integral j) t" + and "negligible (s \ t)" shows "(f has_integral (i + j)) (s \ t)" -proof- note * = has_integral_restrict_univ[symmetric, of f] - show ?thesis unfolding * apply(rule has_integral_spike[OF assms(3)]) - defer apply(rule has_integral_add[OF assms(1-2)[unfolded *]]) by auto qed - -lemma has_integral_unions: fixes f::"'n::ordered_euclidean_space \ 'a::banach" - assumes "finite t" "\s\t. (f has_integral (i s)) s" "\s\t. \s'\t. ~(s = s') \ negligible(s \ s')" +proof - + note * = has_integral_restrict_univ[symmetric, of f] + show ?thesis + unfolding * + apply (rule has_integral_spike[OF assms(3)]) + defer + apply (rule has_integral_add[OF assms(1-2)[unfolded *]]) + apply auto + done +qed + +lemma has_integral_unions: + fixes f :: "'n::ordered_euclidean_space \ 'a::banach" + assumes "finite t" + and "\s\t. (f has_integral (i s)) s" + and "\s\t. \s'\t. s \ s' \ negligible (s \ s')" shows "(f has_integral (setsum i t)) (\t)" -proof- note * = has_integral_restrict_univ[symmetric, of f] - have **:"negligible (\((\(a,b). a \ b) ` {(a,b). a \ t \ b \ {y. y \ t \ ~(a = y)}}))" - apply(rule negligible_unions) apply(rule finite_imageI) apply(rule finite_subset[of _ "t \ t"]) defer - apply(rule finite_cartesian_product[OF assms(1,1)]) using assms(3) by auto - note assms(2)[unfolded *] note has_integral_setsum[OF assms(1) this] - thus ?thesis unfolding * apply-apply(rule has_integral_spike[OF **]) defer apply assumption - proof safe case goal1 thus ?case - proof(cases "x\\t") case True then guess s unfolding Union_iff .. note s=this - hence *:"\b\t. x \ b \ b = s" using goal1(3) by blast - show ?thesis unfolding if_P[OF True] apply(rule trans) defer - apply(rule setsum_cong2) apply(subst *, assumption) apply(rule refl) - unfolding setsum_delta[OF assms(1)] using s by auto qed auto qed qed - -subsection {* In particular adding integrals over a division, maybe not of an interval. *} - -lemma has_integral_combine_division: fixes f::"'n::ordered_euclidean_space \ 'a::banach" - assumes "d division_of s" "\k\d. (f has_integral (i k)) k" +proof - + note * = has_integral_restrict_univ[symmetric, of f] + have **: "negligible (\((\(a,b). a \ b) ` {(a,b). a \ t \ b \ {y. y \ t \ a \ y}}))" + apply (rule negligible_unions) + apply (rule finite_imageI) + apply (rule finite_subset[of _ "t \ t"]) + defer + apply (rule finite_cartesian_product[OF assms(1,1)]) + using assms(3) + apply auto + done + note assms(2)[unfolded *] + note has_integral_setsum[OF assms(1) this] + then show ?thesis unfolding * apply-apply(rule has_integral_spike[OF **]) defer apply assumption + proof safe + case goal1 + then show ?case + proof (cases "x \ \t") + case True + then guess s unfolding Union_iff .. note s=this + then have *: "\b\t. x \ b \ b = s" + using goal1(3) by blast + show ?thesis + unfolding if_P[OF True] + apply (rule trans) + defer + apply (rule setsum_cong2) + apply (subst *) + apply assumption + apply (rule refl) + unfolding setsum_delta[OF assms(1)] + using s + apply auto + done + qed auto + qed +qed + + +text {* In particular adding integrals over a division, maybe not of an interval. *} + +lemma has_integral_combine_division: + fixes f :: "'n::ordered_euclidean_space \ 'a::banach" + assumes "d division_of s" + and "\k\d. (f has_integral (i k)) k" shows "(f has_integral (setsum i d)) s" -proof- note d = division_ofD[OF assms(1)] - show ?thesis unfolding d(6)[symmetric] apply(rule has_integral_unions) - apply(rule d assms)+ apply(rule,rule,rule) - proof- case goal1 from d(4)[OF this(1)] d(4)[OF this(2)] - guess a c b d apply-by(erule exE)+ note obt=this - from d(5)[OF goal1] show ?case unfolding obt interior_closed_interval - apply-apply(rule negligible_subset[of "({a..b}-{a<.. ({c..d}-{c<.. 'a::banach" - assumes "d division_of s" "\k\d. f integrable_on k" +proof - + note d = division_ofD[OF assms(1)] + show ?thesis + unfolding d(6)[symmetric] + apply (rule has_integral_unions) + apply (rule d assms)+ + apply rule + apply rule + apply rule + proof - + case goal1 + from d(4)[OF this(1)] d(4)[OF this(2)] guess a c b d by (elim exE) note obt=this + from d(5)[OF goal1] show ?case + unfolding obt interior_closed_interval + apply - + apply (rule negligible_subset[of "({a..b}-{a<.. ({c..d}-{c<.. 'a::banach" + assumes "d division_of s" + and "\k\d. f integrable_on k" shows "integral s f = setsum (\i. integral i f) d" - apply(rule integral_unique) apply(rule has_integral_combine_division[OF assms(1)]) - using assms(2) unfolding has_integral_integral . - -lemma has_integral_combine_division_topdown: fixes f::"'n::ordered_euclidean_space \ 'a::banach" - assumes "f integrable_on s" "d division_of k" "k \ s" + apply (rule integral_unique) + apply (rule has_integral_combine_division[OF assms(1)]) + using assms(2) + unfolding has_integral_integral + apply assumption + done + +lemma has_integral_combine_division_topdown: + fixes f :: "'n::ordered_euclidean_space \ 'a::banach" + assumes "f integrable_on s" + and "d division_of k" + and "k \ s" shows "(f has_integral (setsum (\i. integral i f) d)) k" - apply(rule has_integral_combine_division[OF assms(2)]) - apply safe unfolding has_integral_integral[symmetric] -proof- case goal1 from division_ofD(2,4)[OF assms(2) this] - show ?case apply safe apply(rule integrable_on_subinterval) - apply(rule assms) using assms(3) by auto qed - -lemma integral_combine_division_topdown: fixes f::"'n::ordered_euclidean_space \ 'a::banach" - assumes "f integrable_on s" "d division_of s" + apply (rule has_integral_combine_division[OF assms(2)]) + apply safe + unfolding has_integral_integral[symmetric] +proof - + case goal1 + from division_ofD(2,4)[OF assms(2) this] + show ?case + apply safe + apply (rule integrable_on_subinterval) + apply (rule assms) + using assms(3) + apply auto + done +qed + +lemma integral_combine_division_topdown: + fixes f :: "'n::ordered_euclidean_space \ 'a::banach" + assumes "f integrable_on s" + and "d division_of s" shows "integral s f = setsum (\i. integral i f) d" - apply(rule integral_unique,rule has_integral_combine_division_topdown) using assms by auto - -lemma integrable_combine_division: fixes f::"'n::ordered_euclidean_space \ 'a::banach" - assumes "d division_of s" "\i\d. f integrable_on i" + apply (rule integral_unique) + apply (rule has_integral_combine_division_topdown) + using assms + apply auto + done + +lemma integrable_combine_division: + fixes f :: "'n::ordered_euclidean_space \ 'a::banach" + assumes "d division_of s" + and "\i\d. f integrable_on i" shows "f integrable_on s" - using assms(2) unfolding integrable_on_def - by(metis has_integral_combine_division[OF assms(1)]) - -lemma integrable_on_subdivision: fixes f::"'n::ordered_euclidean_space \ 'a::banach" - assumes "d division_of i" "f integrable_on s" "i \ s" + using assms(2) + unfolding integrable_on_def + by (metis has_integral_combine_division[OF assms(1)]) + +lemma integrable_on_subdivision: + fixes f :: "'n::ordered_euclidean_space \ 'a::banach" + assumes "d division_of i" + and "f integrable_on s" + and "i \ s" shows "f integrable_on i" - apply(rule integrable_combine_division assms)+ -proof safe case goal1 note division_ofD(2,4)[OF assms(1) this] - thus ?case apply safe apply(rule integrable_on_subinterval[OF assms(2)]) - using assms(3) by auto qed - -subsection {* Also tagged divisions. *} - -lemma has_integral_combine_tagged_division: fixes f::"'n::ordered_euclidean_space \ 'a::banach" - assumes "p tagged_division_of s" "\(x,k) \ p. (f has_integral (i k)) k" + apply (rule integrable_combine_division assms)+ +proof safe + case goal1 + note division_ofD(2,4)[OF assms(1) this] + then show ?case + apply safe + apply (rule integrable_on_subinterval[OF assms(2)]) + using assms(3) + apply auto + done +qed + + +subsection {* Also tagged divisions *} + +lemma has_integral_combine_tagged_division: + fixes f :: "'n::ordered_euclidean_space \ 'a::banach" + assumes "p tagged_division_of s" + and "\(x,k) \ p. (f has_integral (i k)) k" shows "(f has_integral (setsum (\(x,k). i k) p)) s" -proof- have *:"(f has_integral (setsum (\k. integral k f) (snd ` p))) s" - apply(rule has_integral_combine_division) apply(rule division_of_tagged_division[OF assms(1)]) - using assms(2) unfolding has_integral_integral[symmetric] by(safe,auto) - thus ?thesis apply- apply(rule subst[where P="\i. (f has_integral i) s"]) defer apply assumption - apply(rule trans[of _ "setsum (\(x,k). integral k f) p"]) apply(subst eq_commute) - apply(rule setsum_over_tagged_division_lemma[OF assms(1)]) apply(rule integral_null,assumption) - apply(rule setsum_cong2) using assms(2) by auto qed - -lemma integral_combine_tagged_division_bottomup: fixes f::"'n::ordered_euclidean_space \ 'a::banach" - assumes "p tagged_division_of {a..b}" "\(x,k)\p. f integrable_on k" +proof - + have *: "(f has_integral (setsum (\k. integral k f) (snd ` p))) s" + apply (rule has_integral_combine_division) + apply (rule division_of_tagged_division[OF assms(1)]) + using assms(2) + unfolding has_integral_integral[symmetric] + apply safe + apply auto + done + then show ?thesis + apply - + apply (rule subst[where P="\i. (f has_integral i) s"]) + defer + apply assumption + apply (rule trans[of _ "setsum (\(x,k). integral k f) p"]) + apply (subst eq_commute) + apply (rule setsum_over_tagged_division_lemma[OF assms(1)]) + apply (rule integral_null) + apply assumption + apply (rule setsum_cong2) + using assms(2) + apply auto + done +qed + +lemma integral_combine_tagged_division_bottomup: + fixes f :: "'n::ordered_euclidean_space \ 'a::banach" + assumes "p tagged_division_of {a..b}" + and "\(x,k)\p. f integrable_on k" shows "integral {a..b} f = setsum (\(x,k). integral k f) p" - apply(rule integral_unique) apply(rule has_integral_combine_tagged_division[OF assms(1)]) - using assms(2) by auto - -lemma has_integral_combine_tagged_division_topdown: fixes f::"'n::ordered_euclidean_space \ 'a::banach" - assumes "f integrable_on {a..b}" "p tagged_division_of {a..b}" + apply (rule integral_unique) + apply (rule has_integral_combine_tagged_division[OF assms(1)]) + using assms(2) + apply auto + done + +lemma has_integral_combine_tagged_division_topdown: + fixes f :: "'n::ordered_euclidean_space \ 'a::banach" + assumes "f integrable_on {a..b}" + and "p tagged_division_of {a..b}" shows "(f has_integral (setsum (\(x,k). integral k f) p)) {a..b}" - apply(rule has_integral_combine_tagged_division[OF assms(2)]) -proof safe case goal1 note tagged_division_ofD(3-4)[OF assms(2) this] - thus ?case using integrable_subinterval[OF assms(1)] by auto qed - -lemma integral_combine_tagged_division_topdown: fixes f::"'n::ordered_euclidean_space \ 'a::banach" - assumes "f integrable_on {a..b}" "p tagged_division_of {a..b}" + apply (rule has_integral_combine_tagged_division[OF assms(2)]) +proof safe + case goal1 + note tagged_division_ofD(3-4)[OF assms(2) this] + then show ?case + using integrable_subinterval[OF assms(1)] by auto +qed + +lemma integral_combine_tagged_division_topdown: + fixes f :: "'n::ordered_euclidean_space \ 'a::banach" + assumes "f integrable_on {a..b}" + and "p tagged_division_of {a..b}" shows "integral {a..b} f = setsum (\(x,k). integral k f) p" - apply(rule integral_unique,rule has_integral_combine_tagged_division_topdown) using assms by auto - -subsection {* Henstock's lemma. *} - -lemma henstock_lemma_part1: fixes f::"'n::ordered_euclidean_space \ 'a::banach" - assumes "f integrable_on {a..b}" "0 < e" "gauge d" - "(\p. p tagged_division_of {a..b} \ d fine p \ norm (setsum (\(x,k). content k *\<^sub>R f x) p - integral({a..b}) f) < e)" - and p:"p tagged_partial_division_of {a..b}" "d fine p" - shows "norm(setsum (\(x,k). content k *\<^sub>R f x - integral k f) p) \ e" (is "?x \ e") -proof- { presume "\k. 0 ?x \ e + k" thus ?thesis by (blast intro: field_le_epsilon) } - fix k::real assume k:"k>0" note p' = tagged_partial_division_ofD[OF p(1)] - have "\(snd ` p) \ {a..b}" using p'(3) by fastforce + apply (rule integral_unique) + apply (rule has_integral_combine_tagged_division_topdown) + using assms + apply auto + done + + +subsection {* Henstock's lemma *} + +lemma henstock_lemma_part1: + fixes f :: "'n::ordered_euclidean_space \ 'a::banach" + assumes "f integrable_on {a..b}" + and "e > 0" + and "gauge d" + and "(\p. p tagged_division_of {a..b} \ d fine p \ + norm (setsum (\(x,k). content k *\<^sub>R f x) p - integral({a..b}) f) < e)" + and p: "p tagged_partial_division_of {a..b}" "d fine p" + shows "norm (setsum (\(x,k). content k *\<^sub>R f x - integral k f) p) \ e" + (is "?x \ e") +proof - + { presume "\k. 0 ?x \ e + k" then show ?thesis by (blast intro: field_le_epsilon) } + fix k :: real + assume k: "k > 0" + note p' = tagged_partial_division_ofD[OF p(1)] + have "\(snd ` p) \ {a..b}" + using p'(3) by fastforce note partial_division_of_tagged_division[OF p(1)] this from partial_division_extend_interval[OF this] guess q . note q=this and q' = division_ofD[OF this(2)] - def r \ "q - snd ` p" have "snd ` p \ r = {}" unfolding r_def by auto - have r:"finite r" using q' unfolding r_def by auto + def r \ "q - snd ` p" + have "snd ` p \ r = {}" + unfolding r_def by auto + have r: "finite r" + using q' unfolding r_def by auto have "\i\r. \p. p tagged_division_of i \ d fine p \ - norm(setsum (\(x,j). content j *\<^sub>R f x) p - integral i f) < k / (real (card r) + 1)" - proof safe case goal1 hence i:"i \ q" unfolding r_def by auto - from q'(4)[OF this] guess u v apply-by(erule exE)+ note uv=this - have *:"k / (real (card r) + 1) > 0" apply(rule divide_pos_pos,rule k) by auto - have "f integrable_on {u..v}" apply(rule integrable_subinterval[OF assms(1)]) - using q'(2)[OF i] unfolding uv by auto + norm (setsum (\(x,j). content j *\<^sub>R f x) p - integral i f) < k / (real (card r) + 1)" + proof safe + case goal1 + then have i: "i \ q" + unfolding r_def by auto + from q'(4)[OF this] guess u v by (elim exE) note uv=this + have *: "k / (real (card r) + 1) > 0" + apply (rule divide_pos_pos) + apply (rule k) + apply auto + done + have "f integrable_on {u..v}" + apply (rule integrable_subinterval[OF assms(1)]) + using q'(2)[OF i] + unfolding uv + apply auto + done note integrable_integral[OF this, unfolded has_integral[of f]] from this[rule_format,OF *] guess dd .. note dd=conjunctD2[OF this,rule_format] - note gauge_inter[OF `gauge d` dd(1)] from fine_division_exists[OF this,of u v] guess qq . - thus ?case apply(rule_tac x=qq in exI) using dd(2)[of qq] unfolding fine_inter uv by auto qed + note gauge_inter[OF `gauge d` dd(1)] + from fine_division_exists[OF this,of u v] guess qq . + then show ?case + apply (rule_tac x=qq in exI) + using dd(2)[of qq] + unfolding fine_inter uv + apply auto + done + qed from bchoice[OF this] guess qq .. note qq=this[rule_format] - let ?p = "p \ \(qq ` r)" have "norm ((\(x, k)\?p. content k *\<^sub>R f x) - integral {a..b} f) < e" - apply(rule assms(4)[rule_format]) - proof show "d fine ?p" apply(rule fine_union,rule p) apply(rule fine_unions) using qq by auto + let ?p = "p \ \(qq ` r)" + have "norm ((\(x, k)\?p. content k *\<^sub>R f x) - integral {a..b} f) < e" + apply (rule assms(4)[rule_format]) + proof + show "d fine ?p" + apply (rule fine_union) + apply (rule p) + apply (rule fine_unions) + using qq + apply auto + done note * = tagged_partial_division_of_union_self[OF p(1)] have "p \ \(qq ` r) tagged_division_of \(snd ` p) \ \r" - proof(rule tagged_division_union[OF * tagged_division_unions]) - show "finite r" by fact case goal2 thus ?case using qq by auto - next case goal3 thus ?case apply(rule,rule,rule) apply(rule q'(5)) unfolding r_def by auto - next case goal4 thus ?case apply(rule inter_interior_unions_intervals) apply(fact,rule) - apply(rule,rule q') defer apply(rule,subst Int_commute) - apply(rule inter_interior_unions_intervals) apply(rule finite_imageI,rule p',rule) defer - apply(rule,rule q') using q(1) p' unfolding r_def by auto qed - moreover have "\(snd ` p) \ \r = {a..b}" "{qq i |i. i \ r} = qq ` r" - unfolding Union_Un_distrib[symmetric] r_def using q by auto - ultimately show "?p tagged_division_of {a..b}" by fastforce qed - - hence "norm ((\(x, k)\p. content k *\<^sub>R f x) + (\(x, k)\\(qq ` r). content k *\<^sub>R f x) - - integral {a..b} f) < e" apply(subst setsum_Un_zero[symmetric]) apply(rule p') prefer 3 - apply assumption apply rule apply(rule finite_imageI,rule r) apply safe apply(drule qq) - proof- fix x l k assume as:"(x,l)\p" "(x,l)\qq k" "k\r" - note qq[OF this(3)] note tagged_division_ofD(3,4)[OF conjunct1[OF this] as(2)] - from this(2) guess u v apply-by(erule exE)+ note uv=this + proof (rule tagged_division_union[OF * tagged_division_unions]) + show "finite r" + by fact + case goal2 + then show ?case + using qq by auto + next + case goal3 + then show ?case + apply rule + apply rule + apply rule + apply(rule q'(5)) + unfolding r_def + apply auto + done + next + case goal4 + then show ?case + apply (rule inter_interior_unions_intervals) + apply fact + apply rule + apply rule + apply (rule q') + defer + apply rule + apply (subst Int_commute) + apply (rule inter_interior_unions_intervals) + apply (rule finite_imageI) + apply (rule p') + apply rule + defer + apply rule + apply (rule q') + using q(1) p' + unfolding r_def + apply auto + done + qed + moreover have "\(snd ` p) \ \r = {a..b}" and "{qq i |i. i \ r} = qq ` r" + unfolding Union_Un_distrib[symmetric] r_def + using q + by auto + ultimately show "?p tagged_division_of {a..b}" + by fastforce + qed + + then have "norm ((\(x, k)\p. content k *\<^sub>R f x) + (\(x, k)\\(qq ` r). content k *\<^sub>R f x) - + integral {a..b} f) < e" + apply (subst setsum_Un_zero[symmetric]) + apply (rule p') + prefer 3 + apply assumption + apply rule + apply (rule finite_imageI) + apply (rule r) + apply safe + apply (drule qq) + proof - + fix x l k + assume as: "(x, l) \ p" "(x, l) \ qq k" "k \ r" + note qq[OF this(3)] + note tagged_division_ofD(3,4)[OF conjunct1[OF this] as(2)] + from this(2) guess u v by (elim exE) note uv=this have "l\snd ` p" unfolding image_iff apply(rule_tac x="(x,l)" in bexI) using as by auto - hence "l\q" "k\q" "l\k" using as(1,3) q(1) unfolding r_def by auto - note q'(5)[OF this] hence "interior l = {}" using interior_mono[OF `l \ k`] by blast - thus "content l *\<^sub>R f x = 0" unfolding uv content_eq_0_interior[symmetric] by auto qed auto - - hence "norm ((\(x, k)\p. content k *\<^sub>R f x) + setsum (setsum (\(x, k). content k *\<^sub>R f x)) - (qq ` r) - integral {a..b} f) < e" apply(subst(asm) setsum_UNION_zero) - prefer 4 apply assumption apply(rule finite_imageI,fact) - unfolding split_paired_all split_conv image_iff defer apply(erule bexE)+ - proof- fix x m k l T1 T2 assume "(x,m)\T1" "(x,m)\T2" "T1\T2" "k\r" "l\r" "T1 = qq k" "T2 = qq l" - note as = this(1-5)[unfolded this(6-)] note kl = tagged_division_ofD(3,4)[OF qq[THEN conjunct1]] - from this(2)[OF as(4,1)] guess u v apply-by(erule exE)+ note uv=this - have *:"interior (k \ l) = {}" unfolding interior_inter apply(rule q') - using as unfolding r_def by auto - have "interior m = {}" unfolding subset_empty[symmetric] unfolding *[symmetric] - apply(rule interior_mono) using kl(1)[OF as(4,1)] kl(1)[OF as(5,2)] by auto - thus "content m *\<^sub>R f x = 0" unfolding uv content_eq_0_interior[symmetric] by auto - qed(insert qq, auto) - - hence **:"norm ((\(x, k)\p. content k *\<^sub>R f x) + setsum (setsum (\(x, k). content k *\<^sub>R f x) \ qq) r - - integral {a..b} f) < e" apply(subst(asm) setsum_reindex_nonzero) apply fact - apply(rule setsum_0',rule) unfolding split_paired_all split_conv defer apply assumption - proof- fix k l x m assume as:"k\r" "l\r" "k\l" "qq k = qq l" "(x,m)\qq k" - note tagged_division_ofD(6)[OF qq[THEN conjunct1]] from this[OF as(1)] this[OF as(2)] - show "content m *\<^sub>R f x = 0" using as(3) unfolding as by auto qed - - have *:"\ir ip i cr cp. norm((cp + cr) - i) < e \ norm(cr - ir) < k \ - ip + ir = i \ norm(cp - ip) \ e + k" - proof- case goal1 thus ?case using norm_triangle_le[of "cp + cr - i" "- (cr - ir)"] - unfolding goal1(3)[symmetric] norm_minus_cancel by(auto simp add:algebra_simps) qed + then have "l \ q" "k \ q" "l \ k" + using as(1,3) q(1) unfolding r_def by auto + note q'(5)[OF this] + then have "interior l = {}" + using interior_mono[OF `l \ k`] by blast + then show "content l *\<^sub>R f x = 0" + unfolding uv content_eq_0_interior[symmetric] by auto + qed auto + + then have "norm ((\(x, k)\p. content k *\<^sub>R f x) + setsum (setsum (\(x, k). content k *\<^sub>R f x)) + (qq ` r) - integral {a..b} f) < e" + apply (subst (asm) setsum_UNION_zero) + prefer 4 + apply assumption + apply (rule finite_imageI) + apply fact + unfolding split_paired_all split_conv image_iff + defer + apply (erule bexE)+ + proof - + fix x m k l T1 T2 + assume "(x, m) \ T1" "(x, m) \ T2" "T1 \ T2" "k \ r" "l \ r" "T1 = qq k" "T2 = qq l" + note as = this(1-5)[unfolded this(6-)] + note kl = tagged_division_ofD(3,4)[OF qq[THEN conjunct1]] + from this(2)[OF as(4,1)] guess u v by (elim exE) note uv=this + have *: "interior (k \ l) = {}" + unfolding interior_inter + apply (rule q') + using as + unfolding r_def + apply auto + done + have "interior m = {}" + unfolding subset_empty[symmetric] + unfolding *[symmetric] + apply (rule interior_mono) + using kl(1)[OF as(4,1)] kl(1)[OF as(5,2)] + apply auto + done + then show "content m *\<^sub>R f x = 0" + unfolding uv content_eq_0_interior[symmetric] + by auto + qed (insert qq, auto) + + then have **: "norm ((\(x, k)\p. content k *\<^sub>R f x) + setsum (setsum (\(x, k). content k *\<^sub>R f x) \ qq) r - + integral {a..b} f) < e" + apply (subst (asm) setsum_reindex_nonzero) + apply fact + apply (rule setsum_0') + apply rule + unfolding split_paired_all split_conv + defer + apply assumption + proof - + fix k l x m + assume as: "k \ r" "l \ r" "k \ l" "qq k = qq l" "(x, m) \ qq k" + note tagged_division_ofD(6)[OF qq[THEN conjunct1]] + from this[OF as(1)] this[OF as(2)] show "content m *\<^sub>R f x = 0" + using as(3) unfolding as by auto + qed + + have *: "\ir ip i cr cp. norm ((cp + cr) - i) < e \ norm(cr - ir) < k \ + ip + ir = i \ norm (cp - ip) \ e + k" + proof - + case goal1 + then show ?case + using norm_triangle_le[of "cp + cr - i" "- (cr - ir)"] + unfolding goal1(3)[symmetric] norm_minus_cancel + by (auto simp add: algebra_simps) + qed have "?x = norm ((\(x, k)\p. content k *\<^sub>R f x) - (\(x, k)\p. integral k f))" unfolding split_def setsum_subtractf .. - also have "... \ e + k" apply(rule *[OF **, where ir="setsum (\k. integral k f) r"]) - proof- case goal2 have *:"(\(x, k)\p. integral k f) = (\k\snd ` p. integral k f)" - apply(subst setsum_reindex_nonzero) apply fact + also have "\ \ e + k" + apply (rule *[OF **, where ir="setsum (\k. integral k f) r"]) + proof - + case goal2 + have *: "(\(x, k)\p. integral k f) = (\k\snd ` p. integral k f)" + apply (subst setsum_reindex_nonzero) + apply fact unfolding split_paired_all snd_conv split_def o_def - proof- fix x l y m assume as:"(x,l)\p" "(y,m)\p" "(x,l)\(y,m)" "l = m" - from p'(4)[OF as(1)] guess u v apply-by(erule exE)+ note uv=this - show "integral l f = 0" unfolding uv apply(rule integral_unique) - apply(rule has_integral_null) unfolding content_eq_0_interior - using p'(5)[OF as(1-3)] unfolding uv as(4)[symmetric] by auto + proof - + fix x l y m + assume as: "(x, l) \ p" "(y, m) \ p" "(x, l) \ (y, m)" "l = m" + from p'(4)[OF as(1)] guess u v by (elim exE) note uv=this + show "integral l f = 0" + unfolding uv + apply (rule integral_unique) + apply (rule has_integral_null) + unfolding content_eq_0_interior + using p'(5)[OF as(1-3)] + unfolding uv as(4)[symmetric] + apply auto + done qed auto - show ?case unfolding integral_combine_division_topdown[OF assms(1) q(2)] * r_def - apply(rule setsum_Un_disjoint'[symmetric]) using q(1) q'(1) p'(1) by auto - next case goal1 have *:"k * real (card r) / (1 + real (card r)) < k" using k by(auto simp add:field_simps) - show ?case apply(rule le_less_trans[of _ "setsum (\x. k / (real (card r) + 1)) r"]) - unfolding setsum_subtractf[symmetric] apply(rule setsum_norm_le) - apply rule apply(drule qq) defer unfolding divide_inverse setsum_left_distrib[symmetric] - unfolding divide_inverse[symmetric] using * by(auto simp add:field_simps real_eq_of_nat) - qed finally show "?x \ e + k" . qed - -lemma henstock_lemma_part2: fixes f::"'m::ordered_euclidean_space \ 'n::ordered_euclidean_space" - assumes "f integrable_on {a..b}" "0 < e" "gauge d" - "\p. p tagged_division_of {a..b} \ d fine p \ norm (setsum (\(x,k). content k *\<^sub>R f x) p - - integral({a..b}) f) < e" "p tagged_partial_division_of {a..b}" "d fine p" - shows "setsum (\(x,k). norm(content k *\<^sub>R f x - integral k f)) p \ 2 * real (DIM('n)) * e" - unfolding split_def apply(rule setsum_norm_allsubsets_bound) defer - apply(rule henstock_lemma_part1[unfolded split_def,OF assms(1-3)]) - apply safe apply(rule assms[rule_format,unfolded split_def]) defer - apply(rule tagged_partial_division_subset,rule assms,assumption) - apply(rule fine_subset,assumption,rule assms) using assms(5) by auto - -lemma henstock_lemma: fixes f::"'m::ordered_euclidean_space \ 'n::ordered_euclidean_space" - assumes "f integrable_on {a..b}" "e>0" + show ?case + unfolding integral_combine_division_topdown[OF assms(1) q(2)] * r_def + apply (rule setsum_Un_disjoint'[symmetric]) + using q(1) q'(1) p'(1) + apply auto + done + next + case goal1 + have *: "k * real (card r) / (1 + real (card r)) < k" + using k by (auto simp add: field_simps) + show ?case + apply (rule le_less_trans[of _ "setsum (\x. k / (real (card r) + 1)) r"]) + unfolding setsum_subtractf[symmetric] + apply (rule setsum_norm_le) + apply rule + apply (drule qq) + defer + unfolding divide_inverse setsum_left_distrib[symmetric] + unfolding divide_inverse[symmetric] + using * + apply (auto simp add: field_simps real_eq_of_nat) + done + qed + finally show "?x \ e + k" . +qed + +lemma henstock_lemma_part2: + fixes f :: "'m::ordered_euclidean_space \ 'n::ordered_euclidean_space" + assumes "f integrable_on {a..b}" + and "e > 0" + and "gauge d" + and "\p. p tagged_division_of {a..b} \ d fine p \ + norm (setsum (\(x,k). content k *\<^sub>R f x) p - integral {a..b} f) < e" + and "p tagged_partial_division_of {a..b}" + and "d fine p" + shows "setsum (\(x,k). norm (content k *\<^sub>R f x - integral k f)) p \ 2 * real (DIM('n)) * e" + unfolding split_def + apply (rule setsum_norm_allsubsets_bound) + defer + apply (rule henstock_lemma_part1[unfolded split_def,OF assms(1-3)]) + apply safe + apply (rule assms[rule_format,unfolded split_def]) + defer + apply (rule tagged_partial_division_subset) + apply (rule assms) + apply assumption + apply (rule fine_subset) + apply assumption + apply (rule assms) + using assms(5) + apply auto + done + +lemma henstock_lemma: + fixes f :: "'m::ordered_euclidean_space \ 'n::ordered_euclidean_space" + assumes "f integrable_on {a..b}" + and "e > 0" obtains d where "gauge d" - "\p. p tagged_partial_division_of {a..b} \ d fine p - \ setsum (\(x,k). norm(content k *\<^sub>R f x - integral k f)) p < e" -proof- have *:"e / (2 * (real DIM('n) + 1)) > 0" apply(rule divide_pos_pos) using assms(2) by auto + and "\p. p tagged_partial_division_of {a..b} \ d fine p \ + setsum (\(x,k). norm(content k *\<^sub>R f x - integral k f)) p < e" +proof - + have *: "e / (2 * (real DIM('n) + 1)) > 0" + apply (rule divide_pos_pos) + using assms(2) + apply auto + done from integrable_integral[OF assms(1),unfolded has_integral[of f],rule_format,OF this] - guess d .. note d = conjunctD2[OF this] show thesis apply(rule that,rule d) - proof safe case goal1 note * = henstock_lemma_part2[OF assms(1) * d this] - show ?case apply(rule le_less_trans[OF *]) using `e>0` by(auto simp add:field_simps) qed qed + guess d .. note d = conjunctD2[OF this] + show thesis + apply (rule that) + apply (rule d) + proof safe + case goal1 + note * = henstock_lemma_part2[OF assms(1) * d this] + show ?case + apply (rule le_less_trans[OF *]) + using `e > 0` + apply (auto simp add: field_simps) + done + qed +qed + subsection {* Geometric progression *} @@ -9914,804 +10316,1754 @@ lemma sum_gp_basic: fixes x :: "'a::ring_1" shows "(1 - x) * setsum (\i. x^i) {0 .. n} = (1 - x^(Suc n))" -proof- +proof - def y \ "1 - x" have "y * (\i=0..n. (1 - y) ^ i) = 1 - (1 - y) ^ Suc n" - by (induct n, simp, simp add: algebra_simps) - thus ?thesis + by (induct n) (simp_all add: algebra_simps) + then show ?thesis unfolding y_def by simp qed -lemma sum_gp_multiplied: assumes mn: "m <= n" +lemma sum_gp_multiplied: + assumes mn: "m \ n" shows "((1::'a::{field}) - x) * setsum (op ^ x) {m..n} = x^m - x^ Suc n" (is "?lhs = ?rhs") -proof- +proof - let ?S = "{0..(n - m)}" - from mn have mn': "n - m \ 0" by arith + from mn have mn': "n - m \ 0" + by arith let ?f = "op + m" - have i: "inj_on ?f ?S" unfolding inj_on_def by auto + have i: "inj_on ?f ?S" + unfolding inj_on_def by auto have f: "?f ` ?S = {m..n}" - using mn apply (auto simp add: image_iff Bex_def) by arith + using mn + apply (auto simp add: image_iff Bex_def) + apply presburger + done have th: "op ^ x o op + m = (\i. x^m * x^i)" - by (rule ext, simp add: power_add power_mult) + by (rule ext) (simp add: power_add power_mult) from setsum_reindex[OF i, of "op ^ x", unfolded f th setsum_right_distrib[symmetric]] - have "?lhs = x^m * ((1 - x) * setsum (op ^ x) {0..n - m})" by simp - then show ?thesis unfolding sum_gp_basic using mn + have "?lhs = x^m * ((1 - x) * setsum (op ^ x) {0..n - m})" + by simp + then show ?thesis + unfolding sum_gp_basic + using mn by (simp add: field_simps power_add[symmetric]) qed -lemma sum_gp: "setsum (op ^ (x::'a::{field})) {m .. n} = - (if n < m then 0 else if x = 1 then of_nat ((n + 1) - m) - else (x^ m - x^ (Suc n)) / (1 - x))" -proof- - {assume nm: "n < m" hence ?thesis by simp} +lemma sum_gp: + "setsum (op ^ (x::'a::{field})) {m .. n} = + (if n < m then 0 + else if x = 1 then of_nat ((n + 1) - m) + else (x^ m - x^ (Suc n)) / (1 - x))" +proof - + { + assume nm: "n < m" + then have ?thesis by simp + } moreover - {assume "\ n < m" hence nm: "m \ n" by arith - {assume x: "x = 1" hence ?thesis by simp} + { + assume "\ n < m" + then have nm: "m \ n" + by arith + { + assume x: "x = 1" + then have ?thesis + by simp + } moreover - {assume x: "x \ 1" hence nz: "1 - x \ 0" by simp - from sum_gp_multiplied[OF nm, of x] nz have ?thesis by (simp add: field_simps)} - ultimately have ?thesis by metis + { + assume x: "x \ 1" + then have nz: "1 - x \ 0" + by simp + from sum_gp_multiplied[OF nm, of x] nz have ?thesis + by (simp add: field_simps) + } + ultimately have ?thesis by blast } - ultimately show ?thesis by metis -qed - -lemma sum_gp_offset: "setsum (op ^ (x::'a::{field})) {m .. m+n} = - (if x = 1 then of_nat n + 1 else x^m * (1 - x^Suc n) / (1 - x))" + ultimately show ?thesis by blast +qed + +lemma sum_gp_offset: + "setsum (op ^ (x::'a::{field})) {m .. m+n} = + (if x = 1 then of_nat n + 1 else x^m * (1 - x^Suc n) / (1 - x))" unfolding sum_gp[of x m "m + n"] power_Suc by (simp add: field_simps power_add) -subsection {* monotone convergence (bounded interval first). *} - -lemma monotone_convergence_interval: fixes f::"nat \ 'n::ordered_euclidean_space \ real" + +subsection {* Monotone convergence (bounded interval first) *} + +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)" - "\x\{a..b}. ((\k. f k x) ---> g x) sequentially" - "bounded {integral {a..b} (f k) | k . k \ UNIV}" + and "\k. \x\{a..b}.(f k x) \ f (Suc k) x" + and "\x\{a..b}. ((\k. f k x) ---> g x) sequentially" + and "bounded {integral {a..b} (f k) | k . k \ UNIV}" shows "g integrable_on {a..b} \ ((\k. integral ({a..b}) (f k)) ---> integral ({a..b}) g) sequentially" -proof(case_tac[!] "content {a..b} = 0") assume as:"content {a..b} = 0" - show ?thesis using integrable_on_null[OF as] unfolding integral_null[OF as] using tendsto_const by auto -next assume ab:"content {a..b} \ 0" - have fg:"\x\{a..b}. \ k. (f k x) \ 1 \ (g x) \ 1" - proof safe case goal1 note assms(3)[rule_format,OF this] +proof (cases "content {a..b} = 0") + case True + show ?thesis + using integrable_on_null[OF True] + unfolding integral_null[OF True] + using tendsto_const + by auto +next + case False + have fg: "\x\{a..b}. \ k. (f k x) \ 1 \ (g x) \ 1" + proof safe + case goal1 + note assms(3)[rule_format,OF this] note * = Lim_component_ge[OF this trivial_limit_sequentially] - show ?case apply(rule *) unfolding eventually_sequentially - apply(rule_tac x=k in exI) apply- apply(rule transitive_stepwise_le) - using assms(2)[rule_format,OF goal1] by auto qed + show ?case + apply (rule *) + unfolding eventually_sequentially + apply (rule_tac x=k in exI) + apply - + apply (rule transitive_stepwise_le) + using assms(2)[rule_format,OF goal1] + apply auto + done + qed have "\i. ((\k. integral ({a..b}) (f k)) ---> i) sequentially" - apply(rule bounded_increasing_convergent) defer - apply rule apply(rule integral_le) apply safe - apply(rule assms(1-2)[rule_format])+ using assms(4) by auto + apply (rule bounded_increasing_convergent) + defer + apply rule + apply (rule integral_le) + apply safe + apply (rule assms(1-2)[rule_format])+ + using assms(4) + apply auto + done then guess i .. note i=this - have i':"\k. (integral({a..b}) (f k)) \ i\1" - apply(rule Lim_component_ge,rule i) apply(rule trivial_limit_sequentially) - unfolding eventually_sequentially apply(rule_tac x=k in exI) - apply(rule transitive_stepwise_le) prefer 3 unfolding inner_simps real_inner_1_right apply(rule integral_le) - apply(rule assms(1-2)[rule_format])+ using assms(2) by auto - - have "(g has_integral i) {a..b}" unfolding has_integral - proof safe case goal1 note e=this - hence "\k. (\d. gauge d \ (\p. p tagged_division_of {a..b} \ d fine p \ - norm ((\(x, ka)\p. content ka *\<^sub>R f k x) - integral {a..b} (f k)) < e / 2 ^ (k + 2)))" - apply-apply(rule,rule assms(1)[unfolded has_integral_integral has_integral,rule_format]) - apply(rule divide_pos_pos) by auto + have i': "\k. (integral({a..b}) (f k)) \ i\1" + apply (rule Lim_component_ge) + apply (rule i) + apply (rule trivial_limit_sequentially) + unfolding eventually_sequentially + apply (rule_tac x=k in exI) + apply (rule transitive_stepwise_le) + prefer 3 + unfolding inner_simps real_inner_1_right + apply (rule integral_le) + apply (rule assms(1-2)[rule_format])+ + using assms(2) + apply auto + done + + have "(g has_integral i) {a..b}" + unfolding has_integral + proof safe + case goal1 + note e=this + then have "\k. (\d. gauge d \ (\p. p tagged_division_of {a..b} \ d fine p \ + norm ((\(x, ka)\p. content ka *\<^sub>R f k x) - integral {a..b} (f k)) < e / 2 ^ (k + 2)))" + apply - + apply rule + apply (rule assms(1)[unfolded has_integral_integral has_integral,rule_format]) + apply (rule divide_pos_pos) + apply auto + done from choice[OF this] guess c .. note c=conjunctD2[OF this[rule_format],rule_format] have "\r. \k\r. 0 \ i\1 - (integral {a..b} (f k)) \ i\1 - (integral {a..b} (f k)) < e / 4" - proof- case goal1 have "e/4 > 0" using e by auto + proof - + case goal1 + have "e/4 > 0" + using e by auto from LIMSEQ_D [OF i this] guess r .. - thus ?case apply(rule_tac x=r in exI) apply rule - apply(erule_tac x=k in allE) - proof- case goal1 thus ?case using i'[of k] by auto qed qed + then show ?case + apply (rule_tac x=r in exI) + apply rule + apply (erule_tac x=k in allE) + proof - + case goal1 + then show ?case + using i'[of k] by auto + qed + qed then guess r .. note r=conjunctD2[OF this[rule_format]] have "\x\{a..b}. \n\r. \k\n. 0 \ (g x)\1 - (f k x)\1 \ - (g x)\1 - (f k x)\1 < e / (4 * content({a..b}))" - proof case goal1 have "e / (4 * content {a..b}) > 0" apply(rule divide_pos_pos,fact) - using ab content_pos_le[of a b] by auto + (g x)\1 - (f k x)\1 < e / (4 * content({a..b}))" + proof + case goal1 + have "e / (4 * content {a..b}) > 0" + apply (rule divide_pos_pos) + apply fact + using False content_pos_le[of a b] + apply auto + done from assms(3)[rule_format, OF goal1, THEN LIMSEQ_D, OF this] guess n .. note n=this - thus ?case apply(rule_tac x="n + r" in exI) apply safe apply(erule_tac[2-3] x=k in allE) - unfolding dist_real_def using fg[rule_format,OF goal1] - by (auto simp add:field_simps) qed + then show ?case + apply (rule_tac x="n + r" in exI) + apply safe + apply (erule_tac[2-3] x=k in allE) + unfolding dist_real_def + using fg[rule_format,OF goal1] + apply (auto simp add: field_simps) + done + qed from bchoice[OF this] guess m .. note m=conjunctD2[OF this[rule_format],rule_format] def d \ "\x. c (m x) x" - show ?case apply(rule_tac x=d in exI) - 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" + show ?case + apply (rule_tac x=d in exI) + 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 (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" - proof safe case goal1 thus ?case using norm_triangle_lt[of "a - b" "b - c" "3* e/4"] - norm_triangle_lt[of "a - b + (b - c)" "c - d" e] unfolding norm_minus_cancel - by(auto simp add:algebra_simps) qed - show "norm ((\(x, k)\p. content k *\<^sub>R g x) - i) < e" apply(rule *[rule_format,where + have *: "\a b c d. norm(a - b) \ e / 4 \ norm(b - c) < e / 2 \ + norm (c - d) < e / 4 \ norm (a - d) < e" + proof safe + case goal1 + then show ?case + using norm_triangle_lt[of "a - b" "b - c" "3* e/4"] + norm_triangle_lt[of "a - b + (b - c)" "c - d" e] + unfolding norm_minus_cancel + by (auto simp add: algebra_simps) + qed + show "norm ((\(x, k)\p. content k *\<^sub>R g x) - i) < e" + apply (rule *[rule_format,where b="\(x, k)\p. content k *\<^sub>R f (m x) x" and c="\(x, k)\p. integral k (f (m x))"]) - proof safe case goal1 - show ?case apply(rule order_trans[of _ "\(x, k)\p. content k * (e / (4 * content {a..b}))"]) - unfolding setsum_subtractf[symmetric] apply(rule order_trans,rule norm_setsum) - apply(rule setsum_mono) unfolding split_paired_all split_conv - unfolding split_def setsum_left_distrib[symmetric] scaleR_diff_right[symmetric] - unfolding additive_content_tagged_division[OF p(1), unfolded split_def] - proof- fix x k assume xk:"(x,k) \ p" hence x:"x\{a..b}" using p'(2-3)[OF xk] by auto - from p'(4)[OF xk] guess u v apply-by(erule exE)+ note uv=this - show " norm (content k *\<^sub>R (g x - f (m x) x)) \ content k * (e / (4 * content {a..b}))" - unfolding norm_scaleR uv unfolding abs_of_nonneg[OF content_pos_le] - apply(rule mult_left_mono) using m(2)[OF x,of "m x"] by auto - qed(insert ab,auto) - - next case goal2 show ?case apply(rule le_less_trans[of _ "norm (\j = 0..s. - \(x, k)\{xk\p. m (fst xk) = j}. content k *\<^sub>R f (m x) x - integral k (f (m x)))"]) - apply(subst setsum_group) apply fact apply(rule finite_atLeastAtMost) defer - apply(subst split_def)+ unfolding setsum_subtractf apply rule - proof- show "norm (\j = 0..s. \(x, k)\{xk \ p. - m (fst xk) = j}. content k *\<^sub>R f (m x) x - integral k (f (m x))) < e / 2" - apply(rule le_less_trans[of _ "setsum (\i. e / 2^(i+2)) {0..s}"]) - apply(rule setsum_norm_le) - proof show "(\i = 0..s. e / 2 ^ (i + 2)) < e / 2" - unfolding power_add divide_inverse inverse_mult_distrib - unfolding setsum_right_distrib[symmetric] setsum_left_distrib[symmetric] - unfolding power_inverse sum_gp apply(rule mult_strict_left_mono[OF _ e]) - unfolding power2_eq_square by auto - fix t assume "t\{0..s}" - show "norm (\(x, k)\{xk \ p. m (fst xk) = t}. content k *\<^sub>R f (m x) x - - integral k (f (m x))) \ e / 2 ^ (t + 2)"apply(rule order_trans[of _ - "norm(setsum (\(x,k). content k *\<^sub>R f t x - integral k (f t)) {xk \ p. m (fst xk) = t})"]) - apply(rule eq_refl) apply(rule arg_cong[where f=norm]) apply(rule setsum_cong2) defer - apply(rule henstock_lemma_part1) apply(rule assms(1)[rule_format]) - apply(rule divide_pos_pos,rule e) defer apply safe apply(rule c)+ - apply rule apply assumption+ apply(rule tagged_partial_division_subset[of p]) - apply(rule p(1)[unfolded tagged_division_of_def,THEN conjunct1]) defer - unfolding fine_def apply safe apply(drule p(2)[unfolded fine_def,rule_format]) - unfolding d_def by auto qed - qed(insert s, auto) - - next case goal3 - note comb = integral_combine_tagged_division_topdown[OF assms(1)[rule_format] p(1)] - have *:"\sr sx ss ks kr::real. kr = sr \ ks = ss \ ks \ i \ sr \ sx \ sx \ ss \ 0 \ i\1 - kr\1 - \ i\1 - kr\1 < e/4 \ abs(sx - i) < e/4" by auto - show ?case unfolding real_norm_def apply(rule *[rule_format],safe) - apply(rule comb[of r],rule comb[of s]) apply(rule i'[unfolded real_inner_1_right]) - apply(rule_tac[1-2] setsum_mono) unfolding split_paired_all split_conv - apply(rule_tac[1-2] integral_le[OF ]) - proof safe show "0 \ i\1 - (integral {a..b} (f r))\1" using r(1) by auto - show "i\1 - (integral {a..b} (f r))\1 < e / 4" using r(2) by auto - fix x k assume xk:"(x,k)\p" from p'(4)[OF this] guess u v apply-by(erule exE)+ note uv=this - show "f r integrable_on k" "f s integrable_on k" "f (m x) integrable_on k" "f (m x) integrable_on k" - unfolding uv apply(rule_tac[!] integrable_on_subinterval[OF assms(1)[rule_format]]) - using p'(3)[OF xk] unfolding uv by auto - fix y assume "y\k" hence "y\{a..b}" using p'(3)[OF xk] by auto - hence *:"\m. \n\m. (f m y) \ (f n y)" apply-apply(rule transitive_stepwise_le) using assms(2) by auto - show "(f r y) \ (f (m x) y)" "(f (m x) y) \ (f s y)" - apply(rule_tac[!] *[rule_format]) using s[rule_format,OF xk] m(1)[of x] p'(2-3)[OF xk] by auto - qed qed qed qed note * = this - - have "integral {a..b} g = i" apply(rule integral_unique) using * . - thus ?thesis using i * by auto qed - -lemma monotone_convergence_increasing: fixes f::"nat \ 'n::ordered_euclidean_space \ real" - assumes "\k. (f k) integrable_on s" "\k. \x\s. (f k x) \ (f (Suc k) x)" - "\x\s. ((\k. f k x) ---> g x) sequentially" "bounded {integral s (f k)| k. True}" + proof safe + case goal1 + show ?case + apply (rule order_trans[of _ "\(x, k)\p. content k * (e / (4 * content {a..b}))"]) + unfolding setsum_subtractf[symmetric] + apply (rule order_trans) + apply (rule norm_setsum) + apply (rule setsum_mono) + unfolding split_paired_all split_conv + unfolding split_def setsum_left_distrib[symmetric] scaleR_diff_right[symmetric] + unfolding additive_content_tagged_division[OF p(1), unfolded split_def] + proof - + fix x k + assume xk: "(x, k) \ p" + then have x: "x \ {a..b}" + using p'(2-3)[OF xk] by auto + from p'(4)[OF xk] guess u v by (elim exE) note uv=this + show "norm (content k *\<^sub>R (g x - f (m x) x)) \ content k * (e / (4 * content {a..b}))" + unfolding norm_scaleR uv + unfolding abs_of_nonneg[OF content_pos_le] + apply (rule mult_left_mono) + using m(2)[OF x,of "m x"] + apply auto + done + qed (insert False, auto) + + next + case goal2 + show ?case + apply (rule le_less_trans[of _ "norm (\j = 0..s. + \(x, k)\{xk\p. m (fst xk) = j}. content k *\<^sub>R f (m x) x - integral k (f (m x)))"]) + apply (subst setsum_group) + apply fact + apply (rule finite_atLeastAtMost) + defer + apply (subst split_def)+ + unfolding setsum_subtractf + apply rule + proof - + show "norm (\j = 0..s. \(x, k)\{xk \ p. + m (fst xk) = j}. content k *\<^sub>R f (m x) x - integral k (f (m x))) < e / 2" + apply (rule le_less_trans[of _ "setsum (\i. e / 2^(i+2)) {0..s}"]) + apply (rule setsum_norm_le) + proof + show "(\i = 0..s. e / 2 ^ (i + 2)) < e / 2" + unfolding power_add divide_inverse inverse_mult_distrib + unfolding setsum_right_distrib[symmetric] setsum_left_distrib[symmetric] + unfolding power_inverse sum_gp + apply(rule mult_strict_left_mono[OF _ e]) + unfolding power2_eq_square + apply auto + done + fix t + assume "t \ {0..s}" + show "norm (\(x, k)\{xk \ p. m (fst xk) = t}. content k *\<^sub>R f (m x) x - + integral k (f (m x))) \ e / 2 ^ (t + 2)" + apply (rule order_trans + [of _ "norm (setsum (\(x,k). content k *\<^sub>R f t x - integral k (f t)) {xk \ p. m (fst xk) = t})"]) + apply (rule eq_refl) + apply (rule arg_cong[where f=norm]) + apply (rule setsum_cong2) + defer + apply (rule henstock_lemma_part1) + apply (rule assms(1)[rule_format]) + apply (rule divide_pos_pos) + apply (rule e) + defer + apply safe + apply (rule c)+ + apply rule + apply assumption+ + apply (rule tagged_partial_division_subset[of p]) + apply (rule p(1)[unfolded tagged_division_of_def,THEN conjunct1]) + defer + unfolding fine_def + apply safe + apply (drule p(2)[unfolded fine_def,rule_format]) + unfolding d_def + apply auto + done + qed + qed (insert s, auto) + next + case goal3 + note comb = integral_combine_tagged_division_topdown[OF assms(1)[rule_format] p(1)] + have *: "\sr sx ss ks kr::real. kr = sr \ ks = ss \ + ks \ i \ sr \ sx \ sx \ ss \ 0 \ i\1 - kr\1 \ i\1 - kr\1 < e/4 \ abs (sx - i) < e/4" + by auto + show ?case + unfolding real_norm_def + apply (rule *[rule_format]) + apply safe + apply (rule comb[of r]) + apply (rule comb[of s]) + apply (rule i'[unfolded real_inner_1_right]) + apply (rule_tac[1-2] setsum_mono) + unfolding split_paired_all split_conv + apply (rule_tac[1-2] integral_le[OF ]) + proof safe + show "0 \ i\1 - (integral {a..b} (f r))\1" + using r(1) by auto + show "i\1 - (integral {a..b} (f r))\1 < e / 4" + using r(2) by auto + fix x k + assume xk: "(x, k) \ p" + from p'(4)[OF this] guess u v by (elim exE) note uv=this + show "f r integrable_on k" + and "f s integrable_on k" + and "f (m x) integrable_on k" + and "f (m x) integrable_on k" + unfolding uv + apply (rule_tac[!] integrable_on_subinterval[OF assms(1)[rule_format]]) + using p'(3)[OF xk] + unfolding uv + apply auto + done + fix y + assume "y \ k" + then have "y \ {a..b}" + using p'(3)[OF xk] by auto + then have *: "\m. \n\m. f m y \ f n y" + apply - + apply (rule transitive_stepwise_le) + using assms(2) + apply auto + done + show "f r y \ f (m x) y" and "f (m x) y \ f s y" + apply (rule_tac[!] *[rule_format]) + using s[rule_format,OF xk] m(1)[of x] p'(2-3)[OF xk] + apply auto + done + qed + qed + qed + qed note * = this + + have "integral {a..b} g = i" + by (rule integral_unique) (rule *) + then show ?thesis + using i * by auto +qed + +lemma monotone_convergence_increasing: + fixes f :: "nat \ 'n::ordered_euclidean_space \ real" + assumes "\k. (f k) integrable_on s" + and "\k. \x\s. (f k x) \ (f (Suc k) x)" + and "\x\s. ((\k. f k x) ---> g x) sequentially" + and "bounded {integral s (f k)| k. True}" shows "g integrable_on s \ ((\k. integral s (f k)) ---> integral s g) sequentially" -proof- have lem:"\f::nat \ 'n::ordered_euclidean_space \ real. \ g s. \k.\x\s. 0 \ (f k x) \ \k. (f k) integrable_on s \ - \k. \x\s. (f k x) \ (f (Suc k) x) \ \x\s. ((\k. f k x) ---> g x) sequentially \ - bounded {integral s (f k)| k. True} \ g integrable_on s \ ((\k. integral s (f k)) ---> integral s g) sequentially" - proof- case goal1 note assms=this[rule_format] - have "\x\s. \k. (f k x)\1 \ (g x)\1" apply safe apply(rule Lim_component_ge) - apply(rule goal1(4)[rule_format],assumption) apply(rule trivial_limit_sequentially) - unfolding eventually_sequentially apply(rule_tac x=k in exI) - apply(rule transitive_stepwise_le) using goal1(3) by auto note fg=this[rule_format] - - have "\i. ((\k. integral s (f k)) ---> i) sequentially" apply(rule bounded_increasing_convergent) - apply(rule goal1(5)) apply(rule,rule integral_le) apply(rule goal1(2)[rule_format])+ - using goal1(3) by auto then guess i .. note i=this - have "\k. \x\s. \n\k. f k x \ f n x" apply(rule,rule transitive_stepwise_le) using goal1(3) by auto - hence i':"\k. (integral s (f k))\1 \ i\1" apply-apply(rule,rule Lim_component_ge) - apply(rule i,rule trivial_limit_sequentially) unfolding eventually_sequentially - apply(rule_tac x=k in exI,safe) apply(rule integral_component_le) +proof - + have lem: "\f::nat \ 'n::ordered_euclidean_space \ real. + \g s. \k.\x\s. 0 \ f k x \ \k. (f k) integrable_on s \ + \k. \x\s. f k x \ f (Suc k) x \ \x\s. ((\k. f k x) ---> g x) sequentially \ + bounded {integral s (f k)| k. True} \ + g integrable_on s \ ((\k. integral s (f k)) ---> integral s g) sequentially" + proof - + case goal1 + note assms=this[rule_format] + have "\x\s. \k. (f k x)\1 \ (g x)\1" + apply safe + apply (rule Lim_component_ge) + apply (rule goal1(4)[rule_format]) + apply assumption + apply (rule trivial_limit_sequentially) + unfolding eventually_sequentially + apply (rule_tac x=k in exI) + apply (rule transitive_stepwise_le) + using goal1(3) + apply auto + done + note fg=this[rule_format] + + have "\i. ((\k. integral s (f k)) ---> i) sequentially" + apply (rule bounded_increasing_convergent) + apply (rule goal1(5)) + apply rule + apply (rule integral_le) + apply (rule goal1(2)[rule_format])+ + using goal1(3) + apply auto + done + then guess i .. note i=this + have "\k. \x\s. \n\k. f k x \ f n x" + apply rule + apply (rule transitive_stepwise_le) + using goal1(3) + apply auto + done + then have i': "\k. (integral s (f k))\1 \ i\1" + apply - + apply rule + apply (rule Lim_component_ge) + apply (rule i) + apply (rule trivial_limit_sequentially) + unfolding eventually_sequentially + apply (rule_tac x=k in exI) + apply safe + apply (rule integral_component_le) apply simp - apply(rule goal1(2)[rule_format])+ by auto + apply (rule goal1(2)[rule_format])+ + apply auto + done note int = assms(2)[unfolded integrable_alt[of _ s],THEN conjunct1,rule_format] - have ifif:"\k t. (\x. if x \ t then if x \ s then f k x else 0 else 0) = - (\x. if x \ t\s then f k x else 0)" apply(rule ext) by auto - have int':"\k a b. f k integrable_on {a..b} \ s" apply(subst integrable_restrict_univ[symmetric]) - apply(subst ifif[symmetric]) apply(subst integrable_restrict_univ) using int . + have ifif: "\k t. (\x. if x \ t then if x \ s then f k x else 0 else 0) = + (\x. if x \ t \ s then f k x else 0)" + by (rule ext) auto + have int': "\k a b. f k integrable_on {a..b} \ s" + apply (subst integrable_restrict_univ[symmetric]) + apply (subst ifif[symmetric]) + apply (subst integrable_restrict_univ) + apply (rule int) + done have "\a b. (\x. if x \ s then g x else 0) integrable_on {a..b} \ ((\k. integral {a..b} (\x. if x \ s then f k x else 0)) ---> integral {a..b} (\x. if x \ s then g x else 0)) sequentially" - proof(rule monotone_convergence_interval,safe) - case goal1 show ?case using int . - next case goal2 thus ?case apply-apply(cases "x\s") using assms(3) by auto - next case goal3 thus ?case apply-apply(cases "x\s") - using assms(4) by auto - next case goal4 note * = integral_nonneg + proof (rule monotone_convergence_interval, safe) + case goal1 + show ?case by (rule int) + next + case goal2 + then show ?case + apply (cases "x \ s") + using assms(3) + apply auto + done + next + case goal3 + then show ?case + apply (cases "x \ s") + using assms(4) + apply auto + done + next + case goal4 + note * = integral_nonneg have "\k. norm (integral {a..b} (\x. if x \ s then f k x else 0)) \ norm (integral s (f k))" - unfolding real_norm_def apply(subst abs_of_nonneg) apply(rule *[OF int]) - apply(safe,case_tac "x\s") apply(drule assms(1)) prefer 3 - apply(subst abs_of_nonneg) apply(rule *[OF assms(2) goal1(1)[THEN spec]]) - apply(subst integral_restrict_univ[symmetric,OF int]) - unfolding ifif unfolding integral_restrict_univ[OF int'] - apply(rule integral_subset_le[OF _ int' assms(2)]) using assms(1) by auto - thus ?case using assms(5) unfolding bounded_iff apply safe - apply(rule_tac x=aa in exI,safe) apply(erule_tac x="integral s (f k)" in ballE) - apply(rule order_trans) apply assumption by auto qed note g = conjunctD2[OF this] - - have "(g has_integral i) s" unfolding has_integral_alt' apply safe apply(rule g(1)) - proof- case goal1 hence "e/4>0" by auto + unfolding real_norm_def + apply (subst abs_of_nonneg) + apply (rule *[OF int]) + apply safe + apply (case_tac "x \ s") + apply (drule assms(1)) + prefer 3 + apply (subst abs_of_nonneg) + apply (rule *[OF assms(2) goal1(1)[THEN spec]]) + apply (subst integral_restrict_univ[symmetric,OF int]) + unfolding ifif + unfolding integral_restrict_univ[OF int'] + apply (rule integral_subset_le[OF _ int' assms(2)]) + using assms(1) + apply auto + done + then show ?case + using assms(5) + unfolding bounded_iff + apply safe + apply (rule_tac x=aa in exI) + apply safe + apply (erule_tac x="integral s (f k)" in ballE) + apply (rule order_trans) + apply assumption + apply auto + done + qed + note g = conjunctD2[OF this] + + have "(g has_integral i) s" + unfolding has_integral_alt' + apply safe + apply (rule g(1)) + proof - + case goal1 + then have "e/4>0" + by auto from LIMSEQ_D [OF i this] guess N .. note N=this note assms(2)[of N,unfolded has_integral_integral has_integral_alt'[of "f N"]] from this[THEN conjunct2,rule_format,OF `e/4>0`] guess B .. note B=conjunctD2[OF this] - show ?case apply(rule,rule,rule B,safe) - proof- fix a b::"'n::ordered_euclidean_space" assume ab:"ball 0 B \ {a..b}" - from `e>0` have "e/2>0" by auto + show ?case + apply rule + apply rule + apply (rule B) + apply safe + proof - + fix a b :: 'n + assume ab: "ball 0 B \ {a..b}" + from `e > 0` have "e/2 > 0" + by auto from LIMSEQ_D [OF g(2)[of a b] this] guess M .. note M=this - have **:"norm (integral {a..b} (\x. if x \ s then f N x else 0) - i) < e/2" - apply(rule norm_triangle_half_l) using B(2)[rule_format,OF ab] N[rule_format,of N] - apply-defer apply(subst norm_minus_commute) by auto - have *:"\f1 f2 g. abs(f1 - i) < e / 2 \ abs(f2 - g) < e / 2 \ f1 \ f2 \ f2 \ i - \ abs(g - i) < e" unfolding real_inner_1_right by arith + have **: "norm (integral {a..b} (\x. if x \ s then f N x else 0) - i) < e/2" + apply (rule norm_triangle_half_l) + using B(2)[rule_format,OF ab] N[rule_format,of N] + apply - + defer + apply (subst norm_minus_commute) + apply auto + done + have *: "\f1 f2 g. abs (f1 - i) < e / 2 \ abs (f2 - g) < e / 2 \ + f1 \ f2 \ f2 \ i \ abs (g - i) < e" + unfolding real_inner_1_right by arith show "norm (integral {a..b} (\x. if x \ s then g x else 0) - i) < e" - unfolding real_norm_def apply(rule *[rule_format]) - apply(rule **[unfolded real_norm_def]) - apply(rule M[rule_format,of "M + N",unfolded real_norm_def]) apply(rule le_add1) - apply(rule integral_le[OF int int]) defer - apply(rule order_trans[OF _ i'[rule_format,of "M + N",unfolded real_inner_1_right]]) - proof safe case goal2 have "\m. x\s \ \n\m. (f m x)\1 \ (f n x)\1" - apply(rule transitive_stepwise_le) using assms(3) by auto thus ?case by auto - next case goal1 show ?case apply(subst integral_restrict_univ[symmetric,OF int]) + unfolding real_norm_def + apply (rule *[rule_format]) + apply (rule **[unfolded real_norm_def]) + apply (rule M[rule_format,of "M + N",unfolded real_norm_def]) + apply (rule le_add1) + apply (rule integral_le[OF int int]) + defer + apply (rule order_trans[OF _ i'[rule_format,of "M + N",unfolded real_inner_1_right]]) + proof safe + case goal2 + have "\m. x \ s \ \n\m. (f m x)\1 \ (f n x)\1" + apply (rule transitive_stepwise_le) + using assms(3) + apply auto + done + then show ?case + by auto + next + case goal1 + show ?case + apply (subst integral_restrict_univ[symmetric,OF int]) unfolding ifif integral_restrict_univ[OF int'] - apply(rule integral_subset_le[OF _ int']) using assms by auto - qed qed qed - thus ?case apply safe defer apply(drule integral_unique) using i by auto qed - - have sub:"\k. integral s (\x. f k x - f 0 x) = integral s (f k) - integral s (f 0)" - apply(subst integral_sub) apply(rule assms(1)[rule_format])+ by rule - have "\x m. x\s \ \n\m. (f m x) \ (f n x)" apply(rule transitive_stepwise_le) - using assms(2) by auto note * = this[rule_format] - have "(\x. g x - f 0 x) integrable_on s \((\k. integral s (\x. f (Suc k) x - f 0 x)) ---> - integral s (\x. g x - f 0 x)) sequentially" apply(rule lem,safe) - proof- case goal1 thus ?case using *[of x 0 "Suc k"] by auto - next case goal2 thus ?case apply(rule integrable_sub) using assms(1) by auto - next case goal3 thus ?case using *[of x "Suc k" "Suc (Suc k)"] by auto - next case goal4 thus ?case apply-apply(rule tendsto_diff) - using LIMSEQ_ignore_initial_segment[OF assms(3)[rule_format],of x 1] by auto - next case goal5 thus ?case using assms(4) unfolding bounded_iff - apply safe apply(rule_tac x="a + norm (integral s (\x. f 0 x))" in exI) - apply safe apply(erule_tac x="integral s (\x. f (Suc k) x)" in ballE) unfolding sub - apply(rule order_trans[OF norm_triangle_ineq4]) by auto qed - note conjunctD2[OF this] note tendsto_add[OF this(2) tendsto_const[of "integral s (f 0)"]] + apply (rule integral_subset_le[OF _ int']) + using assms + apply auto + done + qed + qed + qed + then show ?case + apply safe + defer + apply (drule integral_unique) + using i + apply auto + done + qed + + have sub: "\k. integral s (\x. f k x - f 0 x) = integral s (f k) - integral s (f 0)" + apply (subst integral_sub) + apply (rule assms(1)[rule_format])+ + apply rule + done + have "\x m. x \ s \ \n\m. f m x \ f n x" + apply (rule transitive_stepwise_le) + using assms(2) + apply auto + done + note * = this[rule_format] + have "(\x. g x - f 0 x) integrable_on s \ ((\k. integral s (\x. f (Suc k) x - f 0 x)) ---> + integral s (\x. g x - f 0 x)) sequentially" + apply (rule lem) + apply safe + proof - + case goal1 + then show ?case + using *[of x 0 "Suc k"] by auto + next + case goal2 + then show ?case + apply (rule integrable_sub) + using assms(1) + apply auto + done + next + case goal3 + then show ?case + using *[of x "Suc k" "Suc (Suc k)"] by auto + next + case goal4 + then show ?case + apply - + apply (rule tendsto_diff) + using LIMSEQ_ignore_initial_segment[OF assms(3)[rule_format],of x 1] + apply auto + done + next + case goal5 + then show ?case + using assms(4) + unfolding bounded_iff + apply safe + apply (rule_tac x="a + norm (integral s (\x. f 0 x))" in exI) + apply safe + apply (erule_tac x="integral s (\x. f (Suc k) x)" in ballE) + unfolding sub + apply (rule order_trans[OF norm_triangle_ineq4]) + apply auto + done + qed + note conjunctD2[OF this] + note tendsto_add[OF this(2) tendsto_const[of "integral s (f 0)"]] integrable_add[OF this(1) assms(1)[rule_format,of 0]] - thus ?thesis unfolding sub apply-apply rule defer apply(subst(asm) integral_sub) - using assms(1) apply auto by(rule LIMSEQ_imp_Suc) qed - -lemma monotone_convergence_decreasing: fixes f::"nat \ 'n::ordered_euclidean_space \ real" - assumes "\k. (f k) integrable_on s" "\k. \x\s. (f (Suc k) x) \ (f k x)" - "\x\s. ((\k. f k x) ---> g x) sequentially" "bounded {integral s (f k)| k. True}" + then show ?thesis + unfolding sub + apply - + apply rule + defer + apply (subst(asm) integral_sub) + using assms(1) + apply auto + apply (rule LIMSEQ_imp_Suc) + apply assumption + done +qed + +lemma monotone_convergence_decreasing: + fixes f :: "nat \ 'n::ordered_euclidean_space \ real" + assumes "\k. (f k) integrable_on s" + and "\k. \x\s. f (Suc k) x \ f k x" + and "\x\s. ((\k. f k x) ---> g x) sequentially" + and "bounded {integral s (f k)| k. True}" shows "g integrable_on s \ ((\k. integral s (f k)) ---> integral s g) sequentially" -proof- note assm = assms[rule_format] - have *:"{integral s (\x. - f k x) |k. True} = op *\<^sub>R -1 ` {integral s (f k)| k. True}" - apply safe unfolding image_iff apply(rule_tac x="integral s (f k)" in bexI) prefer 3 - apply(rule_tac x=k in exI) unfolding integral_neg[OF assm(1)] by auto - have "(\x. - g x) integrable_on s \ ((\k. integral s (\x. - f k x)) - ---> integral s (\x. - g x)) sequentially" apply(rule monotone_convergence_increasing) - apply(safe,rule integrable_neg) apply(rule assm) defer apply(rule tendsto_minus) - apply(rule assm,assumption) unfolding * apply(rule bounded_scaling) using assm by auto +proof - + note assm = assms[rule_format] + have *: "{integral s (\x. - f k x) |k. True} = op *\<^sub>R -1 ` {integral s (f k)| k. True}" + apply safe + unfolding image_iff + apply (rule_tac x="integral s (f k)" in bexI) + prefer 3 + apply (rule_tac x=k in exI) + unfolding integral_neg[OF assm(1)] + apply auto + done + have "(\x. - g x) integrable_on s \ + ((\k. integral s (\x. - f k x)) ---> integral s (\x. - g x)) sequentially" + apply (rule monotone_convergence_increasing) + apply safe + apply (rule integrable_neg) + apply (rule assm) + defer + apply (rule tendsto_minus) + apply (rule assm) + apply assumption + unfolding * + apply (rule bounded_scaling) + using assm + apply auto + done note * = conjunctD2[OF this] - show ?thesis apply rule using integrable_neg[OF *(1)] defer - using tendsto_minus[OF *(2)] apply- unfolding integral_neg[OF assm(1)] - unfolding integral_neg[OF *(1),symmetric] by auto qed - -subsection {* absolute integrability (this is the same as Lebesgue integrability). *} - -definition absolutely_integrable_on (infixr "absolutely'_integrable'_on" 46) where - "f absolutely_integrable_on s \ f integrable_on s \ (\x. (norm(f x))) integrable_on s" + show ?thesis + apply rule + using integrable_neg[OF *(1)] + defer + using tendsto_minus[OF *(2)] + unfolding integral_neg[OF assm(1)] + unfolding integral_neg[OF *(1),symmetric] + apply auto + done +qed + + +subsection {* Absolute integrability (this is the same as Lebesgue integrability) *} + +definition absolutely_integrable_on (infixr "absolutely'_integrable'_on" 46) + where "f absolutely_integrable_on s \ f integrable_on s \ (\x. (norm(f x))) integrable_on s" lemma absolutely_integrable_onI[intro?]: - "f integrable_on s \ (\x. (norm(f x))) integrable_on s \ f absolutely_integrable_on s" - unfolding absolutely_integrable_on_def by auto - -lemma absolutely_integrable_onD[dest]: assumes "f absolutely_integrable_on s" - shows "f integrable_on s" "(\x. (norm(f x))) integrable_on s" - using assms unfolding absolutely_integrable_on_def by auto - -(*lemma absolutely_integrable_on_trans[simp]: fixes f::"'n::ordered_euclidean_space \ real" shows - "(vec1 o f) absolutely_integrable_on s \ f absolutely_integrable_on s" + "f integrable_on s \ + (\x. (norm(f x))) integrable_on s \ f absolutely_integrable_on s" + unfolding absolutely_integrable_on_def + by auto + +lemma absolutely_integrable_onD[dest]: + assumes "f absolutely_integrable_on s" + shows "f integrable_on s" + and "(\x. norm (f x)) integrable_on s" + using assms + unfolding absolutely_integrable_on_def + by auto + +(*lemma absolutely_integrable_on_trans[simp]: + fixes f::"'n::ordered_euclidean_space \ real" + shows "(vec1 o f) absolutely_integrable_on s \ f absolutely_integrable_on s" unfolding absolutely_integrable_on_def o_def by auto*) -lemma integral_norm_bound_integral: fixes f::"'n::ordered_euclidean_space \ 'a::banach" - assumes "f integrable_on s" "g integrable_on s" "\x\s. norm(f x) \ g x" - shows "norm(integral s f) \ (integral s g)" -proof- have *:"\x y. (\e::real. 0 < e \ x < y + e) \ x \ y" apply(safe,rule ccontr) - apply(erule_tac x="x - y" in allE) by auto - have "\e sg dsa dia ig. norm(sg) \ dsa \ abs(dsa - dia) < e / 2 \ norm(sg - ig) < e / 2 - \ norm(ig) < dia + e" - proof safe case goal1 show ?case apply(rule le_less_trans[OF norm_triangle_sub[of ig sg]]) - apply(subst real_sum_of_halves[of e,symmetric]) unfolding add_assoc[symmetric] - apply(rule add_le_less_mono) defer apply(subst norm_minus_commute,rule goal1) - apply(rule order_trans[OF goal1(1)]) using goal1(2) by arith - qed note norm=this[rule_format] - have lem:"\f::'n::ordered_euclidean_space \ 'a. \ g a b. f integrable_on {a..b} \ g integrable_on {a..b} \ - \x\{a..b}. norm(f x) \ (g x) \ norm(integral({a..b}) f) \ (integral({a..b}) g)" - proof(rule *[rule_format]) case goal1 hence *:"e/2>0" by auto +lemma integral_norm_bound_integral: + fixes f :: "'n::ordered_euclidean_space \ 'a::banach" + assumes "f integrable_on s" + and "g integrable_on s" + and "\x\s. norm (f x) \ g x" + shows "norm (integral s f) \ integral s g" +proof - + have *: "\x y. (\e::real. 0 < e \ x < y + e) \ x \ y" + apply safe + apply (rule ccontr) + apply (erule_tac x="x - y" in allE) + apply auto + done + have "\e sg dsa dia ig. + norm sg \ dsa \ abs (dsa - dia) < e / 2 \ norm (sg - ig) < e / 2 \ norm ig < dia + e" + proof safe + case goal1 + show ?case + apply (rule le_less_trans[OF norm_triangle_sub[of ig sg]]) + apply (subst real_sum_of_halves[of e,symmetric]) + unfolding add_assoc[symmetric] + apply (rule add_le_less_mono) + defer + apply (subst norm_minus_commute) + apply (rule goal1) + apply (rule order_trans[OF goal1(1)]) + using goal1(2) + apply arith + done + qed + note norm=this[rule_format] + have lem: "\f::'n \ 'a. \g a b. f integrable_on {a..b} \ g integrable_on {a..b} \ + \x\{a..b}. norm (f x) \ g x \ norm (integral({a..b}) f) \ integral {a..b} g" + proof (rule *[rule_format]) + case goal1 + then have *: "e/2 > 0" + by auto from integrable_integral[OF goal1(1),unfolded has_integral[of f],rule_format,OF *] guess d1 .. note d1 = conjunctD2[OF this,rule_format] from integrable_integral[OF goal1(2),unfolded has_integral[of g],rule_format,OF *] guess d2 .. note d2 = conjunctD2[OF this,rule_format] note gauge_inter[OF d1(1) d2(1)] from fine_division_exists[OF this, of a b] guess p . note p=this - show ?case apply(rule norm) defer - apply(rule d2(2)[OF conjI[OF p(1)],unfolded real_norm_def]) defer - apply(rule d1(2)[OF conjI[OF p(1)]]) defer apply(rule setsum_norm_le) - proof safe fix x k assume "(x,k)\p" note as = tagged_division_ofD(2-4)[OF p(1) this] - from this(3) guess u v apply-by(erule exE)+ note uv=this - show "norm (content k *\<^sub>R f x) \ content k *\<^sub>R g x" unfolding uv norm_scaleR + show ?case + apply (rule norm) + defer + apply (rule d2(2)[OF conjI[OF p(1)],unfolded real_norm_def]) + defer + apply (rule d1(2)[OF conjI[OF p(1)]]) + defer + apply (rule setsum_norm_le) + proof safe + fix x k + assume "(x, k) \ p" + note as = tagged_division_ofD(2-4)[OF p(1) this] + from this(3) guess u v by (elim exE) note uv=this + show "norm (content k *\<^sub>R f x) \ content k *\<^sub>R g x" + unfolding uv norm_scaleR unfolding abs_of_nonneg[OF content_pos_le] real_scaleR_def - apply(rule mult_left_mono) using goal1(3) as by auto - qed(insert p[unfolded fine_inter],auto) qed + apply (rule mult_left_mono) + using goal1(3) as + apply auto + done + qed (insert p[unfolded fine_inter], auto) + qed { presume "\e. 0 < e \ norm (integral s f) < integral s g + e" - thus ?thesis apply-apply(rule *[rule_format]) by auto } - fix e::real assume "e>0" hence e:"e/2 > 0" by auto + then show ?thesis by (rule *[rule_format]) auto } + fix e :: real + assume "e > 0" + then have e: "e/2 > 0" + by auto note assms(1)[unfolded integrable_alt[of f]] note f=this[THEN conjunct1,rule_format] note assms(2)[unfolded integrable_alt[of g]] note g=this[THEN conjunct1,rule_format] from integrable_integral[OF assms(1),unfolded has_integral'[of f],rule_format,OF e] guess B1 .. note B1=conjunctD2[OF this[rule_format],rule_format] from integrable_integral[OF assms(2),unfolded has_integral'[of g],rule_format,OF e] guess B2 .. note B2=conjunctD2[OF this[rule_format],rule_format] - from bounded_subset_closed_interval[OF bounded_ball, of "0::'n::ordered_euclidean_space" "max B1 B2"] - guess a b apply-by(erule exE)+ note ab=this[unfolded ball_max_Un] - - have "ball 0 B1 \ {a..b}" using ab by auto + from bounded_subset_closed_interval[OF bounded_ball, of "0::'n" "max B1 B2"] + guess a b by (elim exE) note ab=this[unfolded ball_max_Un] + + have "ball 0 B1 \ {a..b}" + using ab by auto from B1(2)[OF this] guess z .. note z=conjunctD2[OF this] - have "ball 0 B2 \ {a..b}" using ab by auto + have "ball 0 B2 \ {a..b}" + using ab by auto from B2(2)[OF this] guess w .. note w=conjunctD2[OF this] - show "norm (integral s f) < integral s g + e" apply(rule norm) - apply(rule lem[OF f g, of a b]) unfolding integral_unique[OF z(1)] integral_unique[OF w(1)] - defer apply(rule w(2)[unfolded real_norm_def],rule z(2)) - apply safe apply(case_tac "x\s") unfolding if_P apply(rule assms(3)[rule_format]) by auto qed - -lemma integral_norm_bound_integral_component: fixes f::"'n::ordered_euclidean_space \ 'a::banach" - fixes g::"'n => 'b::ordered_euclidean_space" - assumes "f integrable_on s" "g integrable_on s" "\x\s. norm(f x) \ (g x)\k" - shows "norm(integral s f) \ (integral s g)\k" -proof- have "norm (integral s f) \ integral s ((\x. x \ k) o g)" - apply(rule integral_norm_bound_integral[OF assms(1)]) - apply(rule integrable_linear[OF assms(2)],rule) - unfolding o_def by(rule assms) - thus ?thesis unfolding o_def integral_component_eq[OF assms(2)] . qed - -lemma has_integral_norm_bound_integral_component: fixes f::"'n::ordered_euclidean_space \ 'a::banach" - fixes g::"'n => 'b::ordered_euclidean_space" - assumes "(f has_integral i) s" "(g has_integral j) s" "\x\s. norm(f x) \ (g x)\k" - shows "norm(i) \ j\k" using integral_norm_bound_integral_component[of f s g k] + show "norm (integral s f) < integral s g + e" + apply (rule norm) + apply (rule lem[OF f g, of a b]) + unfolding integral_unique[OF z(1)] integral_unique[OF w(1)] + defer + apply (rule w(2)[unfolded real_norm_def]) + apply (rule z(2)) + apply safe + apply (case_tac "x \ s") + unfolding if_P + apply (rule assms(3)[rule_format]) + apply auto + done +qed + +lemma integral_norm_bound_integral_component: + fixes f :: "'n::ordered_euclidean_space \ 'a::banach" + fixes g :: "'n \ 'b::ordered_euclidean_space" + assumes "f integrable_on s" + and "g integrable_on s" + and "\x\s. norm(f x) \ (g x)\k" + shows "norm (integral s f) \ (integral s g)\k" +proof - + have "norm (integral s f) \ integral s ((\x. x \ k) \ g)" + apply (rule integral_norm_bound_integral[OF assms(1)]) + apply (rule integrable_linear[OF assms(2)]) + apply rule + unfolding o_def + apply (rule assms) + done + then show ?thesis + unfolding o_def integral_component_eq[OF assms(2)] . +qed + +lemma has_integral_norm_bound_integral_component: + fixes f :: "'n::ordered_euclidean_space \ 'a::banach" + fixes g :: "'n \ 'b::ordered_euclidean_space" + assumes "(f has_integral i) s" + and "(g has_integral j) s" + and "\x\s. norm (f x) \ (g x)\k" + shows "norm i \ j\k" + using integral_norm_bound_integral_component[of f s g k] unfolding integral_unique[OF assms(1)] integral_unique[OF assms(2)] - using assms by auto - -lemma absolutely_integrable_le: fixes f::"'n::ordered_euclidean_space \ 'a::banach" + using assms + by auto + +lemma absolutely_integrable_le: + fixes f :: "'n::ordered_euclidean_space \ 'a::banach" assumes "f absolutely_integrable_on s" - shows "norm(integral s f) \ integral s (\x. norm(f x))" - apply(rule integral_norm_bound_integral) using assms by auto - -lemma absolutely_integrable_0[intro]: "(\x. 0) absolutely_integrable_on s" - unfolding absolutely_integrable_on_def by auto + shows "norm (integral s f) \ integral s (\x. norm (f x))" + apply (rule integral_norm_bound_integral) + using assms + apply auto + done + +lemma absolutely_integrable_0[intro]: + "(\x. 0) absolutely_integrable_on s" + unfolding absolutely_integrable_on_def + by auto lemma absolutely_integrable_cmul[intro]: - "f absolutely_integrable_on s \ (\x. c *\<^sub>R f x) absolutely_integrable_on s" - unfolding absolutely_integrable_on_def using integrable_cmul[of f s c] - using integrable_cmul[of "\x. norm (f x)" s "abs c"] by auto + "f absolutely_integrable_on s \ + (\x. c *\<^sub>R f x) absolutely_integrable_on s" + unfolding absolutely_integrable_on_def + using integrable_cmul[of f s c] + using integrable_cmul[of "\x. norm (f x)" s "abs c"] + by auto lemma absolutely_integrable_neg[intro]: - "f absolutely_integrable_on s \ (\x. -f(x)) absolutely_integrable_on s" - apply(drule absolutely_integrable_cmul[where c="-1"]) by auto + "f absolutely_integrable_on s \ + (\x. -f(x)) absolutely_integrable_on s" + apply (drule absolutely_integrable_cmul[where c="-1"]) + apply auto + done lemma absolutely_integrable_norm[intro]: - "f absolutely_integrable_on s \ (\x. norm(f x)) absolutely_integrable_on s" - unfolding absolutely_integrable_on_def by auto + "f absolutely_integrable_on s \ + (\x. norm (f x)) absolutely_integrable_on s" + unfolding absolutely_integrable_on_def + by auto lemma absolutely_integrable_abs[intro]: - "f absolutely_integrable_on s \ (\x. abs(f x::real)) absolutely_integrable_on s" - apply(drule absolutely_integrable_norm) unfolding real_norm_def . - -lemma absolutely_integrable_on_subinterval: fixes f::"'n::ordered_euclidean_space \ 'a::banach" shows - "f absolutely_integrable_on s \ {a..b} \ s \ f absolutely_integrable_on {a..b}" - unfolding absolutely_integrable_on_def by(meson integrable_on_subinterval) - -lemma absolutely_integrable_bounded_variation: fixes f::"'n::ordered_euclidean_space \ 'a::banach" + "f absolutely_integrable_on s \ + (\x. abs(f x::real)) absolutely_integrable_on s" + apply (drule absolutely_integrable_norm) + unfolding real_norm_def + apply assumption + done + +lemma absolutely_integrable_on_subinterval: + fixes f :: "'n::ordered_euclidean_space \ 'a::banach" + shows "f absolutely_integrable_on s \ + {a..b} \ s \ f absolutely_integrable_on {a..b}" + unfolding absolutely_integrable_on_def + by (metis integrable_on_subinterval) + +lemma absolutely_integrable_bounded_variation: + fixes f :: "'n::ordered_euclidean_space \ 'a::banach" assumes "f absolutely_integrable_on UNIV" obtains B where "\d. d division_of (\d) \ setsum (\k. norm(integral k f)) d \ B" - apply(rule that[of "integral UNIV (\x. norm (f x))"]) -proof safe case goal1 note d = division_ofD[OF this(2)] + apply (rule that[of "integral UNIV (\x. norm (f x))"]) +proof safe + case goal1 + note d = division_ofD[OF this(2)] have "(\k\d. norm (integral k f)) \ (\i\d. integral i (\x. norm (f x)))" - apply(rule setsum_mono,rule absolutely_integrable_le) apply(drule d(4),safe) - apply(rule absolutely_integrable_on_subinterval[OF assms]) by auto - also have "... \ integral (\d) (\x. norm (f x))" - apply(subst integral_combine_division_topdown[OF _ goal1(2)]) - using integrable_on_subdivision[OF goal1(2)] using assms by auto - also have "... \ integral UNIV (\x. norm (f x))" - apply(rule integral_subset_le) - using integrable_on_subdivision[OF goal1(2)] using assms by auto - finally show ?case . qed + apply (rule setsum_mono,rule absolutely_integrable_le) + apply (drule d(4)) + apply safe + apply (rule absolutely_integrable_on_subinterval[OF assms]) + apply auto + done + also have "\ \ integral (\d) (\x. norm (f x))" + apply (subst integral_combine_division_topdown[OF _ goal1(2)]) + using integrable_on_subdivision[OF goal1(2)] + using assms + apply auto + done + also have "\ \ integral UNIV (\x. norm (f x))" + apply (rule integral_subset_le) + using integrable_on_subdivision[OF goal1(2)] + using assms + apply auto + done + finally show ?case . +qed lemma helplemma: - assumes "setsum (\x. norm(f x - g x)) s < e" "finite s" - shows "abs(setsum (\x. norm(f x)) s - setsum (\x. norm(g x)) s) < e" - unfolding setsum_subtractf[symmetric] apply(rule le_less_trans[OF setsum_abs]) - apply(rule le_less_trans[OF _ assms(1)]) apply(rule setsum_mono) - using norm_triangle_ineq3 . + assumes "setsum (\x. norm (f x - g x)) s < e" + and "finite s" + shows "abs (setsum (\x. norm(f x)) s - setsum (\x. norm(g x)) s) < e" + unfolding setsum_subtractf[symmetric] + apply (rule le_less_trans[OF setsum_abs]) + apply (rule le_less_trans[OF _ assms(1)]) + apply (rule setsum_mono) + apply (rule norm_triangle_ineq3) + done lemma bounded_variation_absolutely_integrable_interval: - fixes f::"'n::ordered_euclidean_space \ 'm::ordered_euclidean_space" assumes "f integrable_on {a..b}" - "\d. d division_of {a..b} \ setsum (\k. norm(integral k f)) d \ B" + fixes f :: "'n::ordered_euclidean_space \ 'm::ordered_euclidean_space" + assumes "f integrable_on {a..b}" + and "\d. d division_of {a..b} \ setsum (\k. norm(integral k f)) d \ B" shows "f absolutely_integrable_on {a..b}" -proof- let ?S = "(\d. setsum (\k. norm(integral k f)) d) ` {d. d division_of {a..b} }" def i \ "Sup ?S" - have i:"isLub UNIV ?S i" unfolding i_def apply(rule isLub_cSup) - apply(rule elementary_interval) defer apply(rule_tac x=B in exI) - apply(rule setleI) using assms(2) by auto - show ?thesis apply(rule,rule assms) apply rule apply(subst has_integral[of _ i]) - proof safe case goal1 hence "i - e / 2 \ Collect (isUb UNIV (setsum (\k. norm (integral k f)) ` - {d. d division_of {a..b}}))" using isLub_ubs[OF i,rule_format] - unfolding setge_def ubs_def by auto - hence " \y. y division_of {a..b} \ i - e / 2 < (\k\y. norm (integral k f))" - unfolding mem_Collect_eq isUb_def setle_def by(simp add:not_le) then guess d .. note d=conjunctD2[OF this] +proof - + let ?S = "(\d. setsum (\k. norm(integral k f)) d) ` {d. d division_of {a..b} }" + def i \ "Sup ?S" + have i: "isLub UNIV ?S i" + unfolding i_def + apply (rule isLub_cSup) + apply (rule elementary_interval) + defer + apply (rule_tac x=B in exI) + apply (rule setleI) + using assms(2) + apply auto + done + show ?thesis + apply rule + apply (rule assms) + apply rule + apply (subst has_integral[of _ i]) + proof safe + case goal1 + then have "i - e / 2 \ Collect (isUb UNIV (setsum (\k. norm (integral k f)) ` + {d. d division_of {a..b}}))" + using isLub_ubs[OF i,rule_format] + unfolding setge_def ubs_def + by auto + then have "\y. y division_of {a..b} \ i - e / 2 < (\k\y. norm (integral k f))" + unfolding mem_Collect_eq isUb_def setle_def + by (simp add: not_le) + then guess d .. note d=conjunctD2[OF this] note d' = division_ofD[OF this(1)] have "\x. \e>0. \i\d. x \ i \ ball x e \ i = {}" - proof case goal1 have "\da>0. \xa\\{i \ d. x \ i}. da \ dist x xa" - apply(rule separate_point_closed) apply(rule closed_Union) - apply(rule finite_subset[OF _ d'(1)]) apply safe apply(drule d'(4)) by auto - thus ?case apply safe apply(rule_tac x=da in exI,safe) - apply(erule_tac x=xa in ballE) by auto - qed from choice[OF this] guess k .. note k=conjunctD2[OF this[rule_format],rule_format] - - have "e/2 > 0" using goal1 by auto + proof + case goal1 + have "\da>0. \xa\\{i \ d. x \ i}. da \ dist x xa" + apply (rule separate_point_closed) + apply (rule closed_Union) + apply (rule finite_subset[OF _ d'(1)]) + apply safe + apply (drule d'(4)) + apply auto + done + then show ?case + apply safe + apply (rule_tac x=da in exI) + apply safe + apply (erule_tac x=xa in ballE) + apply auto + done + qed + from choice[OF this] guess k .. note k=conjunctD2[OF this[rule_format],rule_format] + + have "e/2 > 0" + using goal1 by auto from henstock_lemma[OF assms(1) this] guess g . note g=this[rule_format] let ?g = "\x. g x \ ball x (k x)" - show ?case apply(rule_tac x="?g" in exI) apply safe - proof- show "gauge ?g" using g(1) unfolding gauge_def using k(1) by auto - fix p assume "p tagged_division_of {a..b}" "?g fine p" + show ?case + apply (rule_tac x="?g" in exI) + apply safe + proof - + show "gauge ?g" + using g(1) + unfolding gauge_def + using k(1) + by auto + fix p + assume "p tagged_division_of {a..b}" and "?g fine p" note p = this(1) conjunctD2[OF this(2)[unfolded fine_inter]] note p' = tagged_division_ofD[OF p(1)] def p' \ "{(x,k) | x k. \i l. x \ i \ i \ d \ (x,l) \ p \ k = i \ l}" - have gp':"g fine p'" using p(2) unfolding p'_def fine_def by auto - have p'':"p' tagged_division_of {a..b}" apply(rule tagged_division_ofI) - proof- show "finite p'" apply(rule finite_subset[of _ "(\(k,(x,l)). (x,k \ l)) - ` {(k,xl) | k xl. k \ d \ xl \ p}"]) unfolding p'_def - defer apply(rule finite_imageI,rule finite_product_dependent[OF d'(1) p'(1)]) - apply safe unfolding image_iff apply(rule_tac x="(i,x,l)" in bexI) by auto - fix x k assume "(x,k)\p'" - hence "\i l. x \ i \ i \ d \ (x, l) \ p \ k = i \ l" unfolding p'_def by auto - then guess i l apply-by(erule exE)+ note il=conjunctD4[OF this] - show "x\k" "k\{a..b}" using p'(2-3)[OF il(3)] il by auto - show "\a b. k = {a..b}" unfolding il using p'(4)[OF il(3)] d'(4)[OF il(2)] - apply safe unfolding inter_interval by auto - next fix x1 k1 assume "(x1,k1)\p'" - hence "\i l. x1 \ i \ i \ d \ (x1, l) \ p \ k1 = i \ l" unfolding p'_def by auto - then guess i1 l1 apply-by(erule exE)+ note il1=conjunctD4[OF this] - fix x2 k2 assume "(x2,k2)\p'" - hence "\i l. x2 \ i \ i \ d \ (x2, l) \ p \ k2 = i \ l" unfolding p'_def by auto - then guess i2 l2 apply-by(erule exE)+ note il2=conjunctD4[OF this] + have gp': "g fine p'" + using p(2) + unfolding p'_def fine_def + by auto + have p'': "p' tagged_division_of {a..b}" + apply (rule tagged_division_ofI) + proof - + show "finite p'" + apply (rule finite_subset[of _ "(\(k,(x,l)). (x,k \ l)) ` + {(k,xl) | k xl. k \ d \ xl \ p}"]) + unfolding p'_def + defer + apply (rule finite_imageI,rule finite_product_dependent[OF d'(1) p'(1)]) + apply safe + unfolding image_iff + apply (rule_tac x="(i,x,l)" in bexI) + apply auto + done + fix x k + assume "(x, k) \ p'" + then have "\i l. x \ i \ i \ d \ (x, l) \ p \ k = i \ l" + unfolding p'_def by auto + then guess i l by (elim exE) note il=conjunctD4[OF this] + show "x \ k" and "k \ {a..b}" + using p'(2-3)[OF il(3)] il by auto + show "\a b. k = {a..b}" + unfolding il using p'(4)[OF il(3)] d'(4)[OF il(2)] + apply safe + unfolding inter_interval + apply auto + done + next + fix x1 k1 + assume "(x1, k1) \ p'" + then have "\i l. x1 \ i \ i \ d \ (x1, l) \ p \ k1 = i \ l" + unfolding p'_def by auto + then guess i1 l1 by (elim exE) note il1=conjunctD4[OF this] + fix x2 k2 + assume "(x2,k2)\p'" + then have "\i l. x2 \ i \ i \ d \ (x2, l) \ p \ k2 = i \ l" + unfolding p'_def by auto + then guess i2 l2 by (elim exE) note il2=conjunctD4[OF this] assume "(x1, k1) \ (x2, k2)" - hence "interior(i1) \ interior(i2) = {} \ interior(l1) \ interior(l2) = {}" - using d'(5)[OF il1(2) il2(2)] p'(5)[OF il1(3) il2(3)] unfolding il1 il2 by auto - thus "interior k1 \ interior k2 = {}" unfolding il1 il2 by auto - next have *:"\(x, X) \ p'. X \ {a..b}" unfolding p'_def using d' by auto - show "\{k. \x. (x, k) \ p'} = {a..b}" apply rule apply(rule Union_least) - unfolding mem_Collect_eq apply(erule exE) apply(drule *[rule_format]) apply safe - proof- fix y assume y:"y\{a..b}" - hence "\x l. (x, l) \ p \ y\l" unfolding p'(6)[symmetric] by auto - then guess x l apply-by(erule exE)+ note xl=conjunctD2[OF this] - hence "\k. k\d \ y\k" using y unfolding d'(6)[symmetric] by auto + then have "interior i1 \ interior i2 = {} \ interior l1 \ interior l2 = {}" + using d'(5)[OF il1(2) il2(2)] p'(5)[OF il1(3) il2(3)] + unfolding il1 il2 + by auto + then show "interior k1 \ interior k2 = {}" + unfolding il1 il2 by auto + next + have *: "\(x, X) \ p'. X \ {a..b}" + unfolding p'_def using d' by auto + show "\{k. \x. (x, k) \ p'} = {a..b}" + apply rule + apply (rule Union_least) + unfolding mem_Collect_eq + apply (erule exE) + apply (drule *[rule_format]) + apply safe + proof - + fix y + assume y: "y \ {a..b}" + then have "\x l. (x, l) \ p \ y\l" + unfolding p'(6)[symmetric] by auto + then guess x l by (elim exE) note xl=conjunctD2[OF this] + then have "\k. k \ d \ y \ k" + using y unfolding d'(6)[symmetric] by auto then guess i .. note i = conjunctD2[OF this] - have "x\i" using fineD[OF p(3) xl(1)] using k(2)[OF i(1), of x] using i(2) xl(2) by auto - thus "y\\{k. \x. (x, k) \ p'}" unfolding p'_def Union_iff apply(rule_tac x="i \ l" in bexI) - defer unfolding mem_Collect_eq apply(rule_tac x=x in exI)+ apply(rule_tac x="i\l" in exI) - apply safe apply(rule_tac x=i in exI) apply(rule_tac x=l in exI) using i xl by auto - qed qed - - hence "(\(x, k)\p'. norm (content k *\<^sub>R f x - integral k f)) < e / 2" - apply-apply(rule g(2)[rule_format]) unfolding tagged_division_of_def apply safe using gp' . - hence **:" \(\(x,k)\p'. norm (content k *\<^sub>R f x)) - (\(x,k)\p'. norm (integral k f))\ < e / 2" - unfolding split_def apply(rule helplemma) using p'' by auto - - have p'alt:"p' = {(x,(i \ l)) | x i l. (x,l) \ p \ i \ d \ ~(i \ l = {})}" - proof safe case goal2 - have "x\i" using fineD[OF p(3) goal2(1)] k(2)[OF goal2(2), of x] goal2(4-) by auto - hence "(x, i \ l) \ p'" unfolding p'_def apply safe - apply(rule_tac x=x in exI,rule_tac x="i\l" in exI) apply safe using goal2 by auto - thus ?case using goal2(3) by auto - next fix x k assume "(x,k)\p'" - hence "\i l. x \ i \ i \ d \ (x, l) \ p \ k = i \ l" unfolding p'_def by auto - then guess i l apply-by(erule exE)+ note il=conjunctD4[OF this] - thus "\y i l. (x, k) = (y, i \ l) \ (y, l) \ p \ i \ d \ i \ l \ {}" - apply(rule_tac x=x in exI,rule_tac x=i in exI,rule_tac x=l in exI) - using p'(2)[OF il(3)] by auto + have "x \ i" + using fineD[OF p(3) xl(1)] + using k(2)[OF i(1), of x] + using i(2) xl(2) + by auto + then show "y \ \{k. \x. (x, k) \ p'}" + unfolding p'_def Union_iff + apply (rule_tac x="i \ l" in bexI) + defer + unfolding mem_Collect_eq + apply (rule_tac x=x in exI)+ + apply (rule_tac x="i\l" in exI) + apply safe + apply (rule_tac x=i in exI) + apply (rule_tac x=l in exI) + using i xl + apply auto + done + qed qed - have sum_p':"(\(x, k)\p'. norm (integral k f)) = (\k\snd ` p'. norm (integral k f))" - apply(subst setsum_over_tagged_division_lemma[OF p'',of "\k. norm (integral k f)"]) - unfolding norm_eq_zero apply(rule integral_null,assumption) .. + + then have "(\(x, k)\p'. norm (content k *\<^sub>R f x - integral k f)) < e / 2" + apply - + apply (rule g(2)[rule_format]) + unfolding tagged_division_of_def + apply safe + apply (rule gp') + done + then have **: "\(\(x,k)\p'. norm (content k *\<^sub>R f x)) - (\(x,k)\p'. norm (integral k f))\ < e / 2" + unfolding split_def + apply (rule helplemma) + using p'' + apply auto + done + + have p'alt: "p' = {(x,(i \ l)) | x i l. (x,l) \ p \ i \ d \ i \ l \ {}}" + proof safe + case goal2 + have "x \ i" + using fineD[OF p(3) goal2(1)] k(2)[OF goal2(2), of x] goal2(4-) + by auto + then have "(x, i \ l) \ p'" + unfolding p'_def + apply safe + apply (rule_tac x=x in exI) + apply (rule_tac x="i \ l" in exI) + apply safe + using goal2 + apply auto + done + then show ?case + using goal2(3) by auto + next + fix x k + assume "(x, k) \ p'" + then have "\i l. x \ i \ i \ d \ (x, l) \ p \ k = i \ l" + unfolding p'_def by auto + then guess i l by (elim exE) note il=conjunctD4[OF this] + then show "\y i l. (x, k) = (y, i \ l) \ (y, l) \ p \ i \ d \ i \ l \ {}" + apply (rule_tac x=x in exI) + apply (rule_tac x=i in exI) + apply (rule_tac x=l in exI) + using p'(2)[OF il(3)] + apply auto + done + qed + have sum_p': "(\(x, k)\p'. norm (integral k f)) = (\k\snd ` p'. norm (integral k f))" + apply (subst setsum_over_tagged_division_lemma[OF p'',of "\k. norm (integral k f)"]) + unfolding norm_eq_zero + apply (rule integral_null) + apply assumption + apply rule + done note snd_p = division_ofD[OF division_of_tagged_division[OF p(1)]] - have *:"\sni sni' sf sf'. abs(sf' - sni') < e / 2 \ i - e / 2 < sni \ sni' \ i \ - sni \ sni' \ sf' = sf \ abs(sf - i) < e" by arith + have *: "\sni sni' sf sf'. abs (sf' - sni') < e / 2 \ i - e / 2 < sni \ sni' \ i \ + sni \ sni' \ sf' = sf \ abs (sf - i) < e" + by arith show "norm ((\(x, k)\p. content k *\<^sub>R norm (f x)) - i) < e" - unfolding real_norm_def apply(rule *[rule_format,OF **],safe) apply(rule d(2)) - proof- case goal1 show ?case unfolding sum_p' - apply(rule isLubD2[OF i]) using division_of_tagged_division[OF p''] by auto - next case goal2 have *:"{k \ l | k l. k \ d \ l \ snd ` p} = - (\(k,l). k \ l) ` {(k,l)|k l. k \ d \ l \ snd ` p}" by auto + unfolding real_norm_def + apply (rule *[rule_format,OF **]) + apply safe + apply(rule d(2)) + proof - + case goal1 + show ?case unfolding sum_p' + apply (rule isLubD2[OF i]) + using division_of_tagged_division[OF p''] + apply auto + done + next + case goal2 + have *: "{k \ l | k l. k \ d \ l \ snd ` p} = + (\(k,l). k \ l) ` {(k,l)|k l. k \ d \ l \ snd ` p}" + by auto have "(\k\d. norm (integral k f)) \ (\i\d. \l\snd ` p. norm (integral (i \ l) f))" - proof(rule setsum_mono) case goal1 note k=this - from d'(4)[OF this] guess u v apply-by(erule exE)+ note uv=this - def d' \ "{{u..v} \ l |l. l \ snd ` p \ ~({u..v} \ l = {})}" note uvab = d'(2)[OF k[unfolded uv]] - have "d' division_of {u..v}" apply(subst d'_def) apply(rule division_inter_1) - apply(rule division_of_tagged_division[OF p(1)]) using uvab . - hence "norm (integral k f) \ setsum (\k. norm (integral k f)) d'" - unfolding uv apply(subst integral_combine_division_topdown[of _ _ d']) - apply(rule integrable_on_subinterval[OF assms(1) uvab]) apply assumption - apply(rule setsum_norm_le) by auto - also have "... = (\k\{k \ l |l. l \ snd ` p}. norm (integral k f))" - apply(rule setsum_mono_zero_left) apply(subst simple_image) - apply(rule finite_imageI)+ apply fact unfolding d'_def uv apply blast - proof case goal1 hence "i \ {{u..v} \ l |l. l \ snd ` p}" by auto + proof (rule setsum_mono) + case goal1 + note k=this + from d'(4)[OF this] guess u v by (elim exE) note uv=this + def d' \ "{{u..v} \ l |l. l \ snd ` p \ {u..v} \ l \ {}}" + note uvab = d'(2)[OF k[unfolded uv]] + have "d' division_of {u..v}" + apply (subst d'_def) + apply (rule division_inter_1) + apply (rule division_of_tagged_division[OF p(1)]) + apply (rule uvab) + done + then have "norm (integral k f) \ setsum (\k. norm (integral k f)) d'" + unfolding uv + apply (subst integral_combine_division_topdown[of _ _ d']) + apply (rule integrable_on_subinterval[OF assms(1) uvab]) + apply assumption + apply (rule setsum_norm_le) + apply auto + done + also have "\ = (\k\{k \ l |l. l \ snd ` p}. norm (integral k f))" + apply (rule setsum_mono_zero_left) + apply (subst simple_image) + apply (rule finite_imageI)+ + apply fact + unfolding d'_def uv + apply blast + proof + case goal1 + then have "i \ {{u..v} \ l |l. l \ snd ` p}" + by auto from this[unfolded mem_Collect_eq] guess l .. note l=this - hence "{u..v} \ l = {}" using goal1 by auto thus ?case using l by auto - qed also have "... = (\l\snd ` p. norm (integral (k \ l) f))" unfolding simple_image - apply(rule setsum_reindex_nonzero[unfolded o_def])apply(rule finite_imageI,rule p') - proof- case goal1 have "interior (k \ l) \ interior (l \ y)" apply(subst(2) interior_inter) - apply(rule Int_greatest) defer apply(subst goal1(4)) by auto - hence *:"interior (k \ l) = {}" using snd_p(5)[OF goal1(1-3)] by auto - from d'(4)[OF k] snd_p(4)[OF goal1(1)] guess u1 v1 u2 v2 apply-by(erule exE)+ note uv=this - show ?case using * unfolding uv inter_interval content_eq_0_interior[symmetric] by auto - qed finally show ?case . - qed also have "... = (\(i,l)\{(i, l) |i l. i \ d \ l \ snd ` p}. norm (integral (i\l) f))" - apply(subst sum_sum_product[symmetric],fact) using p'(1) by auto - also have "... = (\x\{(i, l) |i l. i \ d \ l \ snd ` p}. norm (integral (split op \ x) f))" + then have "{u..v} \ l = {}" + using goal1 by auto + then show ?case + using l by auto + qed + also have "\ = (\l\snd ` p. norm (integral (k \ l) f))" + unfolding simple_image + apply (rule setsum_reindex_nonzero[unfolded o_def]) + apply (rule finite_imageI) + apply (rule p') + proof - + case goal1 + have "interior (k \ l) \ interior (l \ y)" + apply (subst(2) interior_inter) + apply (rule Int_greatest) + defer + apply (subst goal1(4)) + apply auto + done + then have *: "interior (k \ l) = {}" + using snd_p(5)[OF goal1(1-3)] by auto + from d'(4)[OF k] snd_p(4)[OF goal1(1)] guess u1 v1 u2 v2 by (elim exE) note uv=this + show ?case + using * + unfolding uv inter_interval content_eq_0_interior[symmetric] + by auto + qed + finally show ?case . + qed + also have "\ = (\(i,l)\{(i, l) |i l. i \ d \ l \ snd ` p}. norm (integral (i\l) f))" + apply (subst sum_sum_product[symmetric]) + apply fact + using p'(1) + apply auto + done + also have "\ = (\x\{(i, l) |i l. i \ d \ l \ snd ` p}. norm (integral (split op \ x) f))" unfolding split_def .. - also have "... = (\k\{i \ l |i l. i \ d \ l \ snd ` p}. norm (integral k f))" - unfolding * apply(rule setsum_reindex_nonzero[symmetric,unfolded o_def]) - apply(rule finite_product_dependent) apply(fact,rule finite_imageI,rule p') + also have "\ = (\k\{i \ l |i l. i \ d \ l \ snd ` p}. norm (integral k f))" + unfolding * + apply (rule setsum_reindex_nonzero[symmetric,unfolded o_def]) + apply (rule finite_product_dependent) + apply fact + apply (rule finite_imageI) + apply (rule p') unfolding split_paired_all mem_Collect_eq split_conv o_def - proof- note * = division_ofD(4,5)[OF division_of_tagged_division,OF p(1)] - fix l1 l2 k1 k2 assume as:"(l1, k1) \ (l2, k2)" "l1 \ k1 = l2 \ k2" + proof - + note * = division_ofD(4,5)[OF division_of_tagged_division,OF p(1)] + fix l1 l2 k1 k2 + assume as: + "(l1, k1) \ (l2, k2)" + "l1 \ k1 = l2 \ k2" "\i l. (l1, k1) = (i, l) \ i \ d \ l \ snd ` p" "\i l. (l2, k2) = (i, l) \ i \ d \ l \ snd ` p" - hence "l1 \ d" "k1 \ snd ` p" by auto from d'(4)[OF this(1)] *(1)[OF this(2)] - guess u1 v1 u2 v2 apply-by(erule exE)+ note uv=this - have "l1 \ l2 \ k1 \ k2" using as by auto - hence "(interior(k1) \ interior(k2) = {} \ interior(l1) \ interior(l2) = {})" apply- - apply(erule disjE) apply(rule disjI2) apply(rule d'(5)) prefer 4 apply(rule disjI1) - apply(rule *) using as by auto - moreover have "interior(l1 \ k1) = interior(l2 \ k2)" using as(2) by auto - ultimately have "interior(l1 \ k1) = {}" by auto - thus "norm (integral (l1 \ k1) f) = 0" unfolding uv inter_interval - unfolding content_eq_0_interior[symmetric] by auto - qed also have "... = (\(x, k)\p'. norm (integral k f))" unfolding sum_p' - apply(rule setsum_mono_zero_right) apply(subst *) - apply(rule finite_imageI[OF finite_product_dependent]) apply fact - apply(rule finite_imageI[OF p'(1)]) apply safe - proof- case goal2 have "ia \ b = {}" using goal2 unfolding p'alt image_iff Bex_def not_ex - apply(erule_tac x="(a,ia\b)" in allE) by auto thus ?case by auto - next case goal1 thus ?case unfolding p'_def apply safe - apply(rule_tac x=i in exI,rule_tac x=l in exI) unfolding snd_conv image_iff - apply safe apply(rule_tac x="(a,l)" in bexI) by auto - qed finally show ?case . - - next case goal3 + then have "l1 \ d" and "k1 \ snd ` p" + by auto from d'(4)[OF this(1)] *(1)[OF this(2)] + guess u1 v1 u2 v2 by (elim exE) note uv=this + have "l1 \ l2 \ k1 \ k2" + using as by auto + then have "interior k1 \ interior k2 = {} \ interior l1 \ interior l2 = {}" + apply - + apply (erule disjE) + apply (rule disjI2) + apply (rule d'(5)) + prefer 4 + apply (rule disjI1) + apply (rule *) + using as + apply auto + done + moreover have "interior (l1 \ k1) = interior (l2 \ k2)" + using as(2) by auto + ultimately have "interior(l1 \ k1) = {}" + by auto + then show "norm (integral (l1 \ k1) f) = 0" + unfolding uv inter_interval + unfolding content_eq_0_interior[symmetric] + by auto + qed + also have "\ = (\(x, k)\p'. norm (integral k f))" + unfolding sum_p' + apply (rule setsum_mono_zero_right) + apply (subst *) + apply (rule finite_imageI[OF finite_product_dependent]) + apply fact + apply (rule finite_imageI[OF p'(1)]) + apply safe + proof - + case goal2 + have "ia \ b = {}" + using goal2 + unfolding p'alt image_iff Bex_def not_ex + apply (erule_tac x="(a, ia \ b)" in allE) + apply auto + done + then show ?case + by auto + next + case goal1 + then show ?case + unfolding p'_def + apply safe + apply (rule_tac x=i in exI) + apply (rule_tac x=l in exI) + unfolding snd_conv image_iff + apply safe + apply (rule_tac x="(a,l)" in bexI) + apply auto + done + qed + finally show ?case . + next + case goal3 let ?S = "{(x, i \ l) |x i l. (x, l) \ p \ i \ d}" - have Sigma_alt:"\s t. s \ t = {(i, j) |i j. i \ s \ j \ t}" by auto - have *:"?S = (\(xl,i). (fst xl, snd xl \ i)) ` (p \ d)" (*{(xl,i)|xl i. xl\p \ i\d}"**) - apply safe unfolding image_iff apply(rule_tac x="((x,l),i)" in bexI) by auto + have Sigma_alt: "\s t. s \ t = {(i, j) |i j. i \ s \ j \ t}" + by auto + have *: "?S = (\(xl,i). (fst xl, snd xl \ i)) ` (p \ d)" (*{(xl,i)|xl i. xl\p \ i\d}"**) + apply safe + unfolding image_iff + apply (rule_tac x="((x,l),i)" in bexI) + apply auto + done note pdfin = finite_cartesian_product[OF p'(1) d'(1)] have "(\(x, k)\p'. norm (content k *\<^sub>R f x)) = (\(x, k)\?S. \content k\ * norm (f x))" - unfolding norm_scaleR apply(rule setsum_mono_zero_left) - apply(subst *, rule finite_imageI) apply fact unfolding p'alt apply blast - apply safe apply(rule_tac x=x in exI,rule_tac x=i in exI,rule_tac x=l in exI) by auto - also have "... = (\((x,l),i)\p \ d. \content (l \ i)\ * norm (f x))" unfolding * - apply(subst setsum_reindex_nonzero,fact) unfolding split_paired_all - unfolding o_def split_def snd_conv fst_conv mem_Sigma_iff Pair_eq apply(erule_tac conjE)+ - proof- fix x1 l1 k1 x2 l2 k2 assume as:"(x1,l1)\p" "(x2,l2)\p" "k1\d" "k2\d" + unfolding norm_scaleR + apply (rule setsum_mono_zero_left) + apply (subst *) + apply (rule finite_imageI) + apply fact + unfolding p'alt + apply blast + apply safe + apply (rule_tac x=x in exI) + apply (rule_tac x=i in exI) + apply (rule_tac x=l in exI) + apply auto + done + also have "\ = (\((x,l),i)\p \ d. \content (l \ i)\ * norm (f x))" + unfolding * + apply (subst setsum_reindex_nonzero) + apply fact + unfolding split_paired_all + unfolding o_def split_def snd_conv fst_conv mem_Sigma_iff Pair_eq + apply (elim conjE) + proof - + fix x1 l1 k1 x2 l2 k2 + assume as: "(x1, l1) \ p" "(x2, l2) \ p" "k1 \ d" "k2 \ d" "x1 = x2" "l1 \ k1 = l2 \ k2" "\ ((x1 = x2 \ l1 = l2) \ k1 = k2)" - from d'(4)[OF as(3)] p'(4)[OF as(1)] guess u1 v1 u2 v2 apply-by(erule exE)+ note uv=this - from as have "l1 \ l2 \ k1 \ k2" by auto - hence "(interior(k1) \ interior(k2) = {} \ interior(l1) \ interior(l2) = {})" - apply-apply(erule disjE) apply(rule disjI2) defer apply(rule disjI1) - apply(rule d'(5)[OF as(3-4)],assumption) apply(rule p'(5)[OF as(1-2)]) by auto - moreover have "interior(l1 \ k1) = interior(l2 \ k2)" unfolding as .. - ultimately have "interior (l1 \ k1) = {}" by auto - thus "\content (l1 \ k1)\ * norm (f x1) = 0" unfolding uv inter_interval - unfolding content_eq_0_interior[symmetric] by auto - qed safe also have "... = (\(x, k)\p. content k *\<^sub>R norm (f x))" unfolding Sigma_alt - apply(subst sum_sum_product[symmetric]) apply(rule p', rule,rule d') - apply(rule setsum_cong2) unfolding split_paired_all split_conv - proof- fix x l assume as:"(x,l)\p" - note xl = p'(2-4)[OF this] from this(3) guess u v apply-by(erule exE)+ note uv=this + from d'(4)[OF as(3)] p'(4)[OF as(1)] guess u1 v1 u2 v2 by (elim exE) note uv=this + from as have "l1 \ l2 \ k1 \ k2" + by auto + then have "interior k1 \ interior k2 = {} \ interior l1 \ interior l2 = {}" + apply - + apply (erule disjE) + apply (rule disjI2) + defer + apply (rule disjI1) + apply (rule d'(5)[OF as(3-4)]) + apply assumption + apply (rule p'(5)[OF as(1-2)]) + apply auto + done + moreover have "interior (l1 \ k1) = interior (l2 \ k2)" + unfolding as .. + ultimately have "interior (l1 \ k1) = {}" + by auto + then show "\content (l1 \ k1)\ * norm (f x1) = 0" + unfolding uv inter_interval + unfolding content_eq_0_interior[symmetric] + by auto + qed safe + also have "\ = (\(x, k)\p. content k *\<^sub>R norm (f x))" + unfolding Sigma_alt + apply (subst sum_sum_product[symmetric]) + apply (rule p') + apply rule + apply (rule d') + apply (rule setsum_cong2) + unfolding split_paired_all split_conv + proof - + fix x l + assume as: "(x, l) \ p" + note xl = p'(2-4)[OF this] + from this(3) guess u v by (elim exE) note uv=this have "(\i\d. \content (l \ i)\) = (\k\d. content (k \ {u..v}))" - apply(rule setsum_cong2) apply(drule d'(4),safe) apply(subst Int_commute) - unfolding inter_interval uv apply(subst abs_of_nonneg) by auto - also have "... = setsum content {k\{u..v}| k. k\d}" unfolding simple_image - apply(rule setsum_reindex_nonzero[unfolded o_def,symmetric]) apply(rule d') - proof- case goal1 from d'(4)[OF this(1)] d'(4)[OF this(2)] - guess u1 v1 u2 v2 apply- by(erule exE)+ note uv=this - have "{} = interior ((k \ y) \ {u..v})" apply(subst interior_inter) - using d'(5)[OF goal1(1-3)] by auto - also have "... = interior (y \ (k \ {u..v}))" by auto - also have "... = interior (k \ {u..v})" unfolding goal1(4) by auto - finally show ?case unfolding uv inter_interval content_eq_0_interior .. - qed also have "... = setsum content {{u..v} \ k |k. k \ d \ ~({u..v} \ k = {})}" - apply(rule setsum_mono_zero_right) unfolding simple_image - apply(rule finite_imageI,rule d') apply blast apply safe - apply(rule_tac x=k in exI) - proof- case goal1 from d'(4)[OF this(1)] guess a b apply-by(erule exE)+ note ab=this - have "interior (k \ {u..v}) \ {}" using goal1(2) - unfolding ab inter_interval content_eq_0_interior by auto - thus ?case using goal1(1) using interior_subset[of "k \ {u..v}"] by auto - qed finally show "(\i\d. \content (l \ i)\ * norm (f x)) = content l *\<^sub>R norm (f x)" - unfolding setsum_left_distrib[symmetric] real_scaleR_def apply - - apply(subst(asm) additive_content_division[OF division_inter_1[OF d(1)]]) - using xl(2)[unfolded uv] unfolding uv by auto - qed finally show ?case . - qed qed qed qed - -lemma bounded_variation_absolutely_integrable: fixes f::"'n::ordered_euclidean_space \ 'm::ordered_euclidean_space" - assumes "f integrable_on UNIV" "\d. d division_of (\d) \ setsum (\k. norm(integral k f)) d \ B" + apply (rule setsum_cong2) + apply (drule d'(4)) + apply safe + apply (subst Int_commute) + unfolding inter_interval uv + apply (subst abs_of_nonneg) + apply auto + done + also have "\ = setsum content {k \ {u..v}| k. k \ d}" + unfolding simple_image + apply (rule setsum_reindex_nonzero[unfolded o_def,symmetric]) + apply (rule d') + proof - + case goal1 + from d'(4)[OF this(1)] d'(4)[OF this(2)] + guess u1 v1 u2 v2 by (elim exE) note uv=this + have "{} = interior ((k \ y) \ {u..v})" + apply (subst interior_inter) + using d'(5)[OF goal1(1-3)] + apply auto + done + also have "\ = interior (y \ (k \ {u..v}))" + by auto + also have "\ = interior (k \ {u..v})" + unfolding goal1(4) by auto + finally show ?case + unfolding uv inter_interval content_eq_0_interior .. + qed + also have "\ = setsum content {{u..v} \ k |k. k \ d \ {u..v} \ k \ {}}" + apply (rule setsum_mono_zero_right) + unfolding simple_image + apply (rule finite_imageI) + apply (rule d') + apply blast + apply safe + apply (rule_tac x=k in exI) + proof - + case goal1 + from d'(4)[OF this(1)] guess a b by (elim exE) note ab=this + have "interior (k \ {u..v}) \ {}" + using goal1(2) + unfolding ab inter_interval content_eq_0_interior + by auto + then show ?case + using goal1(1) + using interior_subset[of "k \ {u..v}"] + by auto + qed + finally show "(\i\d. \content (l \ i)\ * norm (f x)) = content l *\<^sub>R norm (f x)" + unfolding setsum_left_distrib[symmetric] real_scaleR_def + apply (subst(asm) additive_content_division[OF division_inter_1[OF d(1)]]) + using xl(2)[unfolded uv] + unfolding uv + apply auto + done + qed + finally show ?case . + qed + qed + qed +qed + +lemma bounded_variation_absolutely_integrable: + fixes f :: "'n::ordered_euclidean_space \ 'm::ordered_euclidean_space" + assumes "f integrable_on UNIV" + and "\d. d division_of (\d) \ setsum (\k. norm (integral k f)) d \ B" shows "f absolutely_integrable_on UNIV" -proof(rule absolutely_integrable_onI,fact,rule) - let ?S = "(\d. setsum (\k. norm(integral k f)) d) ` {d. d division_of (\d)}" def i \ "Sup ?S" - have i:"isLub UNIV ?S i" unfolding i_def apply(rule isLub_cSup) - apply(rule elementary_interval) defer apply(rule_tac x=B in exI) - apply(rule setleI) using assms(2) by auto - have f_int:"\a b. f absolutely_integrable_on {a..b}" - apply(rule bounded_variation_absolutely_integrable_interval[where B=B]) - apply(rule integrable_on_subinterval[OF assms(1)]) defer apply safe - apply(rule assms(2)[rule_format]) by auto - show "((\x. norm (f x)) has_integral i) UNIV" apply(subst has_integral_alt',safe) - proof- case goal1 show ?case using f_int[of a b] by auto - next case goal2 have "\y\setsum (\k. norm (integral k f)) ` {d. d division_of \d}. \ y \ i - e" - proof(rule ccontr) case goal1 hence "i \ i - e" apply- - apply(rule isLub_le_isUb[OF i]) apply(rule isUbI) unfolding setle_def by auto - thus False using goal2 by auto - qed then guess K .. note * = this[unfolded image_iff not_le] +proof (rule absolutely_integrable_onI, fact, rule) + let ?S = "(\d. setsum (\k. norm(integral k f)) d) ` {d. d division_of (\d)}" + def i \ "Sup ?S" + have i: "isLub UNIV ?S i" + unfolding i_def + apply (rule isLub_cSup) + apply (rule elementary_interval) + defer + apply (rule_tac x=B in exI) + apply (rule setleI) + using assms(2) + apply auto + done + have f_int: "\a b. f absolutely_integrable_on {a..b}" + apply (rule bounded_variation_absolutely_integrable_interval[where B=B]) + apply (rule integrable_on_subinterval[OF assms(1)]) + defer + apply safe + apply (rule assms(2)[rule_format]) + apply auto + done + show "((\x. norm (f x)) has_integral i) UNIV" + apply (subst has_integral_alt') + apply safe + proof - + case goal1 + show ?case + using f_int[of a b] by auto + next + case goal2 + have "\y\setsum (\k. norm (integral k f)) ` {d. d division_of \d}. \ y \ i - e" + proof (rule ccontr) + case goal1 + then have "i \ i - e" + apply - + apply (rule isLub_le_isUb[OF i]) + apply (rule isUbI) + unfolding setle_def + apply auto + done + then show False + using goal2 by auto + qed + then guess K .. note * = this[unfolded image_iff not_le] from this(1) guess d .. note this[unfolded mem_Collect_eq] - note d = this(1) *(2)[unfolded this(2)] note d'=division_ofD[OF this(1)] - have "bounded (\d)" by(rule elementary_bounded,fact) + note d = this(1) *(2)[unfolded this(2)] + note d'=division_ofD[OF this(1)] + have "bounded (\d)" + by (rule elementary_bounded,fact) from this[unfolded bounded_pos] guess K .. note K=conjunctD2[OF this] - show ?case apply(rule_tac x="K + 1" in exI,safe) - proof- fix a b assume ab:"ball 0 (K + 1) \ {a..b::'n::ordered_euclidean_space}" - have *:"\s s1. i - e < s1 \ s1 \ s \ s < i + e \ abs(s - i) < (e::real)" by arith + show ?case + apply (rule_tac x="K + 1" in exI) + apply safe + proof - + fix a b :: 'n + assume ab: "ball 0 (K + 1) \ {a..b}" + have *: "\s s1. i - e < s1 \ s1 \ s \ s < i + e \ abs (s - i) < e" + by arith show "norm (integral {a..b} (\x. if x \ UNIV then norm (f x) else 0) - i) < e" - unfolding real_norm_def apply(rule *[rule_format],safe) apply(rule d(2)) - proof- case goal1 have "(\k\d. norm (integral k f)) \ setsum (\k. integral k (\x. norm (f x))) d" - apply(rule setsum_mono) apply(rule absolutely_integrable_le) - apply(drule d'(4),safe) by(rule f_int) - also have "... = integral (\d) (\x. norm(f x))" - apply(rule integral_combine_division_bottomup[symmetric]) - apply(rule d) unfolding forall_in_division[OF d(1)] using f_int by auto - also have "... \ integral {a..b} (\x. if x \ UNIV then norm (f x) else 0)" - proof- case goal1 have "\d \ {a..b}" apply rule apply(drule K(2)[rule_format]) - apply(rule ab[unfolded subset_eq,rule_format]) by(auto simp add:dist_norm) - thus ?case apply- apply(subst if_P,rule) apply(rule integral_subset_le) defer - apply(rule integrable_on_subdivision[of _ _ _ "{a..b}"]) - apply(rule d) using f_int[of a b] by auto - qed finally show ?case . - - next note f = absolutely_integrable_onD[OF f_int[of a b]] + unfolding real_norm_def + apply (rule *[rule_format]) + apply safe + apply (rule d(2)) + proof - + case goal1 + have "(\k\d. norm (integral k f)) \ setsum (\k. integral k (\x. norm (f x))) d" + apply (rule setsum_mono) + apply (rule absolutely_integrable_le) + apply (drule d'(4)) + apply safe + apply (rule f_int) + done + also have "\ = integral (\d) (\x. norm (f x))" + apply (rule integral_combine_division_bottomup[symmetric]) + apply (rule d) + unfolding forall_in_division[OF d(1)] + using f_int + apply auto + done + also have "\ \ integral {a..b} (\x. if x \ UNIV then norm (f x) else 0)" + proof - + case goal1 + have "\d \ {a..b}" + apply rule + apply (drule K(2)[rule_format]) + apply (rule ab[unfolded subset_eq,rule_format]) + apply (auto simp add: dist_norm) + done + then show ?case + apply - + apply (subst if_P) + apply rule + apply (rule integral_subset_le) + defer + apply (rule integrable_on_subdivision[of _ _ _ "{a..b}"]) + apply (rule d) + using f_int[of a b] + apply auto + done + qed + finally show ?case . + next + note f = absolutely_integrable_onD[OF f_int[of a b]] note * = this(2)[unfolded has_integral_integral has_integral[of "\x. norm (f x)"],rule_format] - have "e/2>0" using `e>0` by auto from *[OF this] guess d1 .. note d1=conjunctD2[OF this] + have "e/2>0" + using `e > 0` by auto + from *[OF this] guess d1 .. note d1=conjunctD2[OF this] from henstock_lemma[OF f(1) `e/2>0`] guess d2 . note d2=this from fine_division_exists[OF gauge_inter[OF d1(1) d2(1)], of a b] guess p . note p=this(1) conjunctD2[OF this(2)[unfolded fine_inter]] - have *:"\sf sf' si di. sf' = sf \ si \ i \ abs(sf - si) < e / 2 - \ abs(sf' - di) < e / 2 \ di < i + e" by arith - show "integral {a..b} (\x. if x \ UNIV then norm (f x) else 0) < i + e" apply(subst if_P,rule) - proof(rule *[rule_format]) + have *: "\sf sf' si di. sf' = sf \ si \ i \ abs (sf - si) < e / 2 \ + abs (sf' - di) < e / 2 \ di < i + e" + by arith + show "integral {a..b} (\x. if x \ UNIV then norm (f x) else 0) < i + e" + apply (subst if_P) + apply rule + proof (rule *[rule_format]) show "\(\(x,k)\p. norm (content k *\<^sub>R f x)) - (\(x,k)\p. norm (integral k f))\ < e / 2" - unfolding split_def apply(rule helplemma) using d2(2)[rule_format,of p] - using p(1,3) unfolding tagged_division_of_def split_def by auto + unfolding split_def + apply (rule helplemma) + using d2(2)[rule_format,of p] + using p(1,3) + unfolding tagged_division_of_def split_def + apply auto + done show "abs ((\(x, k)\p. content k *\<^sub>R norm (f x)) - integral {a..b} (\x. norm(f x))) < e / 2" - using d1(2)[rule_format,OF conjI[OF p(1,2)]] unfolding real_norm_def . + using d1(2)[rule_format,OF conjI[OF p(1,2)]] + by (simp only: real_norm_def) show "(\(x, k)\p. content k *\<^sub>R norm (f x)) = (\(x, k)\p. norm (content k *\<^sub>R f x))" - apply(rule setsum_cong2) unfolding split_paired_all split_conv - apply(drule tagged_division_ofD(4)[OF p(1)]) unfolding norm_scaleR - apply(subst abs_of_nonneg) by auto + apply (rule setsum_cong2) + unfolding split_paired_all split_conv + apply (drule tagged_division_ofD(4)[OF p(1)]) + unfolding norm_scaleR + apply (subst abs_of_nonneg) + apply auto + done show "(\(x, k)\p. norm (integral k f)) \ i" - apply(subst setsum_over_tagged_division_lemma[OF p(1)]) defer apply(rule isLubD2[OF i]) - unfolding image_iff apply(rule_tac x="snd ` p" in bexI) unfolding mem_Collect_eq defer - apply(rule partial_division_of_tagged_division[of _ "{a..b}"]) - using p(1) unfolding tagged_division_of_def by auto - qed qed qed(insert K,auto) qed qed + apply (subst setsum_over_tagged_division_lemma[OF p(1)]) + defer + apply (rule isLubD2[OF i]) + unfolding image_iff + apply (rule_tac x="snd ` p" in bexI) + unfolding mem_Collect_eq + defer + apply (rule partial_division_of_tagged_division[of _ "{a..b}"]) + using p(1) + unfolding tagged_division_of_def + apply auto + done + qed + qed + qed (insert K, auto) + qed +qed lemma absolutely_integrable_restrict_univ: - "(\x. if x \ s then f x else (0::'a::banach)) absolutely_integrable_on UNIV \ f absolutely_integrable_on s" + "(\x. if x \ s then f x else (0::'a::banach)) absolutely_integrable_on UNIV \ + f absolutely_integrable_on s" unfolding absolutely_integrable_on_def if_distrib norm_zero integrable_restrict_univ .. -lemma absolutely_integrable_add[intro]: fixes f g::"'n::ordered_euclidean_space \ 'm::ordered_euclidean_space" - assumes "f absolutely_integrable_on s" "g absolutely_integrable_on s" - shows "(\x. f(x) + g(x)) absolutely_integrable_on s" -proof- let ?P = "\f g::'n::ordered_euclidean_space \ 'm::ordered_euclidean_space. f absolutely_integrable_on UNIV \ - g absolutely_integrable_on UNIV \ (\x. f(x) + g(x)) absolutely_integrable_on UNIV" - { presume as:"PROP ?P" note a = absolutely_integrable_restrict_univ[symmetric] - have *:"\x. (if x \ s then f x else 0) + (if x \ s then g x else 0) - = (if x \ s then f x + g x else 0)" by auto - show ?thesis apply(subst a) using as[OF assms[unfolded a[of f] a[of g]]] unfolding * . } - fix f g::"'n::ordered_euclidean_space \ 'm::ordered_euclidean_space" assume assms:"f absolutely_integrable_on UNIV" - "g absolutely_integrable_on UNIV" +lemma absolutely_integrable_add[intro]: + fixes f g :: "'n::ordered_euclidean_space \ 'm::ordered_euclidean_space" + assumes "f absolutely_integrable_on s" + and "g absolutely_integrable_on s" + shows "(\x. f x + g x) absolutely_integrable_on s" +proof - + let ?P = "\f g::'n \ 'm. f absolutely_integrable_on UNIV \ + g absolutely_integrable_on UNIV \ (\x. f x + g x) absolutely_integrable_on UNIV" + { + presume as: "PROP ?P" + note a = absolutely_integrable_restrict_univ[symmetric] + have *: "\x. (if x \ s then f x else 0) + (if x \ s then g x else 0) = + (if x \ s then f x + g x else 0)" by auto + show ?thesis + apply (subst a) + using as[OF assms[unfolded a[of f] a[of g]]] + apply (simp only: *) + done + } + fix f g :: "'n \ 'm" + assume assms: "f absolutely_integrable_on UNIV" "g absolutely_integrable_on UNIV" note absolutely_integrable_bounded_variation from this[OF assms(1)] this[OF assms(2)] guess B1 B2 . note B=this[rule_format] - show "(\x. f(x) + g(x)) absolutely_integrable_on UNIV" - apply(rule bounded_variation_absolutely_integrable[of _ "B1+B2"]) - apply(rule integrable_add) prefer 3 - proof safe case goal1 have "\k. k \ d \ f integrable_on k \ g integrable_on k" - apply(drule division_ofD(4)[OF goal1]) apply safe - apply(rule_tac[!] integrable_on_subinterval[of _ UNIV]) using assms by auto - hence "(\k\d. norm (integral k (\x. f x + g x))) \ - (\k\d. norm (integral k f)) + (\k\d. norm (integral k g))" apply- - unfolding setsum_addf[symmetric] apply(rule setsum_mono) - apply(subst integral_add) prefer 3 apply(rule norm_triangle_ineq) by auto - also have "... \ B1 + B2" using B(1)[OF goal1] B(2)[OF goal1] by auto + show "(\x. f x + g x) absolutely_integrable_on UNIV" + apply (rule bounded_variation_absolutely_integrable[of _ "B1+B2"]) + apply (rule integrable_add) + prefer 3 + proof safe + case goal1 + have "\k. k \ d \ f integrable_on k \ g integrable_on k" + apply (drule division_ofD(4)[OF goal1]) + apply safe + apply (rule_tac[!] integrable_on_subinterval[of _ UNIV]) + using assms + apply auto + done + then have "(\k\d. norm (integral k (\x. f x + g x))) \ + (\k\d. norm (integral k f)) + (\k\d. norm (integral k g))" + apply - + unfolding setsum_addf[symmetric] + apply (rule setsum_mono) + apply (subst integral_add) + prefer 3 + apply (rule norm_triangle_ineq) + apply auto + done + also have "\ \ B1 + B2" + using B(1)[OF goal1] B(2)[OF goal1] by auto finally show ?case . - qed(insert assms,auto) qed - -lemma absolutely_integrable_sub[intro]: fixes f g::"'n::ordered_euclidean_space \ 'm::ordered_euclidean_space" - assumes "f absolutely_integrable_on s" "g absolutely_integrable_on s" - shows "(\x. f(x) - g(x)) absolutely_integrable_on s" + qed (insert assms, auto) +qed + +lemma absolutely_integrable_sub[intro]: + fixes f g :: "'n::ordered_euclidean_space \ 'm::ordered_euclidean_space" + assumes "f absolutely_integrable_on s" + and "g absolutely_integrable_on s" + shows "(\x. f x - g x) absolutely_integrable_on s" using absolutely_integrable_add[OF assms(1) absolutely_integrable_neg[OF assms(2)]] - unfolding algebra_simps . - -lemma absolutely_integrable_linear: fixes f::"'m::ordered_euclidean_space \ 'n::ordered_euclidean_space" and h::"'n::ordered_euclidean_space \ 'p::ordered_euclidean_space" - assumes "f absolutely_integrable_on s" "bounded_linear h" - shows "(h o f) absolutely_integrable_on s" -proof- { presume as:"\f::'m::ordered_euclidean_space \ 'n::ordered_euclidean_space. \h::'n::ordered_euclidean_space \ 'p::ordered_euclidean_space. - f absolutely_integrable_on UNIV \ bounded_linear h \ - (h o f) absolutely_integrable_on UNIV" note a = absolutely_integrable_restrict_univ[symmetric] - show ?thesis apply(subst a) using as[OF assms[unfolded a[of f] a[of g]]] - unfolding o_def if_distrib linear_simps[OF assms(2)] . } - fix f::"'m::ordered_euclidean_space \ 'n::ordered_euclidean_space" and h::"'n::ordered_euclidean_space \ 'p::ordered_euclidean_space" - assume assms:"f absolutely_integrable_on UNIV" "bounded_linear h" + by (simp only: algebra_simps) + +lemma absolutely_integrable_linear: + fixes f :: "'m::ordered_euclidean_space \ 'n::ordered_euclidean_space" + and h :: "'n::ordered_euclidean_space \ 'p::ordered_euclidean_space" + assumes "f absolutely_integrable_on s" + and "bounded_linear h" + shows "(h \ f) absolutely_integrable_on s" +proof - + { + presume as: "\f::'m \ 'n. \h::'n \ 'p. f absolutely_integrable_on UNIV \ + bounded_linear h \ (h \ f) absolutely_integrable_on UNIV" + note a = absolutely_integrable_restrict_univ[symmetric] + show ?thesis + apply (subst a) + using as[OF assms[unfolded a[of f] a[of g]]] + apply (simp only: o_def if_distrib linear_simps[OF assms(2)]) + done + } + fix f :: "'m \ 'n" + fix h :: "'n \ 'p" + assume assms: "f absolutely_integrable_on UNIV" "bounded_linear h" from absolutely_integrable_bounded_variation[OF assms(1)] guess B . note B=this from bounded_linear.pos_bounded[OF assms(2)] guess b .. note b=conjunctD2[OF this] - show "(h o f) absolutely_integrable_on UNIV" - apply(rule bounded_variation_absolutely_integrable[of _ "B * b"]) - apply(rule integrable_linear[OF _ assms(2)]) - proof safe case goal2 + show "(h \ f) absolutely_integrable_on UNIV" + apply (rule bounded_variation_absolutely_integrable[of _ "B * b"]) + apply (rule integrable_linear[OF _ assms(2)]) + proof safe + case goal2 have "(\k\d. norm (integral k (h \ f))) \ setsum (\k. norm(integral k f)) d * b" - unfolding setsum_left_distrib apply(rule setsum_mono) - proof- case goal1 from division_ofD(4)[OF goal2 this] - guess u v apply-by(erule exE)+ note uv=this - have *:"f integrable_on k" unfolding uv apply(rule integrable_on_subinterval[of _ UNIV]) - using assms by auto note this[unfolded has_integral_integral] + unfolding setsum_left_distrib + apply (rule setsum_mono) + proof - + case goal1 + from division_ofD(4)[OF goal2 this] + guess u v by (elim exE) note uv=this + have *: "f integrable_on k" + unfolding uv + apply (rule integrable_on_subinterval[of _ UNIV]) + using assms + apply auto + done + note this[unfolded has_integral_integral] note has_integral_linear[OF this assms(2)] integrable_linear[OF * assms(2)] note * = has_integral_unique[OF this(2)[unfolded has_integral_integral] this(1)] - show ?case unfolding * using b by auto - qed also have "... \ B * b" apply(rule mult_right_mono) using B goal2 b by auto + show ?case + unfolding * using b by auto + qed + also have "\ \ B * b" + apply (rule mult_right_mono) + using B goal2 b + apply auto + done finally show ?case . - qed(insert assms,auto) qed - -lemma absolutely_integrable_setsum: fixes f::"'a \ 'n::ordered_euclidean_space \ 'm::ordered_euclidean_space" - assumes "finite t" "\a. a \ t \ (f a) absolutely_integrable_on s" + qed (insert assms, auto) +qed + +lemma absolutely_integrable_setsum: + fixes f :: "'a \ 'n::ordered_euclidean_space \ 'm::ordered_euclidean_space" + assumes "finite t" + and "\a. a \ t \ (f a) absolutely_integrable_on s" shows "(\x. setsum (\a. f a x) t) absolutely_integrable_on s" - using assms(1,2) apply induct defer apply(subst setsum.insert) apply assumption+ by(rule,auto) + using assms(1,2) + apply induct + defer + apply (subst setsum.insert) + apply assumption+ + apply rule + apply auto + done lemma bounded_linear_setsum: fixes f :: "'i \ 'a::real_normed_vector \ 'b::real_normed_vector" - assumes f: "\i. i\I \ bounded_linear (f i)" + assumes f: "\i. i \ I \ bounded_linear (f i)" shows "bounded_linear (\x. \i\I. f i x)" -proof cases - assume "finite I" from this f show ?thesis +proof (cases "finite I") + case True + from this f show ?thesis by (induct I) (auto intro!: bounded_linear_add bounded_linear_zero) -qed (simp add: bounded_linear_zero) +next + case False + then show ?thesis by (simp add: bounded_linear_zero) +qed lemma absolutely_integrable_vector_abs: - fixes f::"'a::ordered_euclidean_space => 'b::ordered_euclidean_space" - fixes T :: "'c::ordered_euclidean_space \ 'b" + fixes f :: "'a::ordered_euclidean_space => 'b::ordered_euclidean_space" + and T :: "'c::ordered_euclidean_space \ 'b" assumes f: "f absolutely_integrable_on s" shows "(\x. (\i\Basis. abs(f x\T i) *\<^sub>R i)) absolutely_integrable_on s" - (is "?Tf absolutely_integrable_on s") + (is "?Tf absolutely_integrable_on s") proof - have if_distrib: "\P A B x. (if P then A else B) *\<^sub>R x = (if P then A *\<^sub>R x else B *\<^sub>R x)" by simp @@ -10730,8 +12082,9 @@ qed lemma absolutely_integrable_max: - fixes f g::"'m::ordered_euclidean_space \ 'n::ordered_euclidean_space" - assumes "f absolutely_integrable_on s" "g absolutely_integrable_on s" + fixes f g :: "'m::ordered_euclidean_space \ 'n::ordered_euclidean_space" + assumes "f absolutely_integrable_on s" + and "g absolutely_integrable_on s" shows "(\x. (\i\Basis. max (f(x)\i) (g(x)\i) *\<^sub>R i)::'n) absolutely_integrable_on s" proof - have *:"\x. (1 / 2) *\<^sub>R (((\i\Basis. \(f x - g x) \ i\ *\<^sub>R i)::'n) + (f x + g x)) = @@ -10741,12 +12094,13 @@ note absolutely_integrable_vector_abs[OF this(1), where T="\x. x"] this(2) note absolutely_integrable_add[OF this] note absolutely_integrable_cmul[OF this, of "1/2"] - thus ?thesis unfolding * . + then show ?thesis unfolding * . qed lemma absolutely_integrable_min: fixes f g::"'m::ordered_euclidean_space \ 'n::ordered_euclidean_space" - assumes "f absolutely_integrable_on s" "g absolutely_integrable_on s" + assumes "f absolutely_integrable_on s" + and "g absolutely_integrable_on s" shows "(\x. (\i\Basis. min (f(x)\i) (g(x)\i) *\<^sub>R i)::'n) absolutely_integrable_on s" proof - have *:"\x. (1 / 2) *\<^sub>R ((f x + g x) - (\i\Basis. \(f x - g x) \ i\ *\<^sub>R i::'n)) = @@ -10757,58 +12111,100 @@ note this(1) absolutely_integrable_vector_abs[OF this(2), where T="\x. x"] note absolutely_integrable_sub[OF this] note absolutely_integrable_cmul[OF this,of "1/2"] - thus ?thesis unfolding * . + then show ?thesis unfolding * . qed lemma absolutely_integrable_abs_eq: fixes f::"'n::ordered_euclidean_space \ 'm::ordered_euclidean_space" shows "f absolutely_integrable_on s \ f integrable_on s \ - (\x. (\i\Basis. abs(f x\i) *\<^sub>R i)::'m) integrable_on s" (is "?l = ?r") + (\x. (\i\Basis. abs(f x\i) *\<^sub>R i)::'m) integrable_on s" + (is "?l = ?r") proof - assume ?l thus ?r apply-apply rule defer - apply(drule absolutely_integrable_vector_abs) by auto + assume ?l + then show ?r + apply - + apply rule + defer + apply (drule absolutely_integrable_vector_abs) + apply auto + done next assume ?r - { presume lem:"\f::'n \ 'm. f integrable_on UNIV \ - (\x. (\i\Basis. \f x\i\ *\<^sub>R i)::'m) integrable_on UNIV \ f absolutely_integrable_on UNIV" - have *:"\x. (\i\Basis. \(if x \ s then f x else 0) \ i\ *\<^sub>R i) = - (if x\s then (\i\Basis. \f x \ i\ *\<^sub>R i) else (0::'m))" - unfolding euclidean_eq_iff[where 'a='m] by auto - show ?l apply(subst absolutely_integrable_restrict_univ[symmetric]) apply(rule lem) - unfolding integrable_restrict_univ * using `?r` by auto } - fix f::"'n::ordered_euclidean_space \ 'm::ordered_euclidean_space" - assume assms:"f integrable_on UNIV" "(\x. (\i\Basis. \f x\i\ *\<^sub>R i)::'m) integrable_on UNIV" + { + presume lem: "\f::'n \ 'm. f integrable_on UNIV \ + (\x. (\i\Basis. \f x\i\ *\<^sub>R i)::'m) integrable_on UNIV \ + f absolutely_integrable_on UNIV" + have *: "\x. (\i\Basis. \(if x \ s then f x else 0) \ i\ *\<^sub>R i) = + (if x \ s then (\i\Basis. \f x \ i\ *\<^sub>R i) else (0::'m))" + unfolding euclidean_eq_iff[where 'a='m] + by auto + show ?l + apply (subst absolutely_integrable_restrict_univ[symmetric]) + apply (rule lem) + unfolding integrable_restrict_univ * + using `?r` + apply auto + done + } + fix f :: "'n \ 'm" + assume assms: "f integrable_on UNIV" "(\x. (\i\Basis. \f x\i\ *\<^sub>R i)::'m) integrable_on UNIV" let ?B = "\i\Basis. integral UNIV (\x. (\i\Basis. \f x\i\ *\<^sub>R i)::'m) \ i" show "f absolutely_integrable_on UNIV" - apply(rule bounded_variation_absolutely_integrable[OF assms(1), where B="?B"],safe) - proof- case goal1 note d=this and d'=division_ofD[OF this] + apply (rule bounded_variation_absolutely_integrable[OF assms(1), where B="?B"]) + apply safe + proof - + case goal1 + note d=this and d'=division_ofD[OF this] have "(\k\d. norm (integral k f)) \ (\k\d. setsum (op \ (integral k (\x. (\i\Basis. \f x\i\ *\<^sub>R i)::'m))) Basis)" - apply(rule setsum_mono) - apply(rule order_trans[OF norm_le_l1]) apply(rule setsum_mono) unfolding lessThan_iff - proof- fix k and i :: 'm assume "k\d" and i:"i\Basis" - from d'(4)[OF this(1)] guess a b apply-by(erule exE)+ note ab=this + apply (rule setsum_mono) + apply (rule order_trans[OF norm_le_l1]) + apply (rule setsum_mono) + unfolding lessThan_iff + proof - + fix k + fix i :: 'm + assume "k \ d" and i: "i \ Basis" + from d'(4)[OF this(1)] guess a b by (elim exE) note ab=this show "\integral k f \ i\ \ integral k (\x. (\i\Basis. \f x\i\ *\<^sub>R i)::'m) \ i" apply (rule abs_leI) - unfolding inner_minus_left[symmetric] defer apply(subst integral_neg[symmetric]) - defer apply(rule_tac[1-2] integral_component_le[OF i]) apply(rule integrable_neg) + unfolding inner_minus_left[symmetric] + defer + apply (subst integral_neg[symmetric]) + defer + apply (rule_tac[1-2] integral_component_le[OF i]) + apply (rule integrable_neg) using integrable_on_subinterval[OF assms(1),of a b] - integrable_on_subinterval[OF assms(2),of a b] i unfolding ab by auto - qed also have "... \ setsum (op \ (integral UNIV (\x. (\i\Basis. \f x\i\ *\<^sub>R i)::'m))) Basis" - apply(subst setsum_commute,rule setsum_mono) - proof- case goal1 have *:"(\x. \i\Basis. \f x\i\ *\<^sub>R i::'m) integrable_on \d" + integrable_on_subinterval[OF assms(2),of a b] i + unfolding ab + apply auto + done + qed + also have "\ \ setsum (op \ (integral UNIV (\x. (\i\Basis. \f x\i\ *\<^sub>R i)::'m))) Basis" + apply (subst setsum_commute) + apply (rule setsum_mono) + proof - + case goal1 + have *: "(\x. \i\Basis. \f x\i\ *\<^sub>R i::'m) integrable_on \d" using integrable_on_subdivision[OF d assms(2)] by auto - have "(\i\d. integral i (\x. \i\Basis. \f x\i\ *\<^sub>R i::'m) \ j) - = integral (\d) (\x. \i\Basis. \f x\i\ *\<^sub>R i::'m) \ j" + have "(\i\d. integral i (\x. \i\Basis. \f x\i\ *\<^sub>R i::'m) \ j) = + integral (\d) (\x. \i\Basis. \f x\i\ *\<^sub>R i::'m) \ j" unfolding inner_setsum_left[symmetric] integral_combine_division_topdown[OF * d] .. - also have "... \ integral UNIV (\x. \i\Basis. \f x\i\ *\<^sub>R i::'m) \ j" - apply(rule integral_subset_component_le) using assms * `j\Basis` by auto + also have "\ \ integral UNIV (\x. \i\Basis. \f x\i\ *\<^sub>R i::'m) \ j" + apply (rule integral_subset_component_le) + using assms * `j \ Basis` + apply auto + done finally show ?case . - qed finally show ?case . qed qed + qed + finally show ?case . + qed +qed lemma nonnegative_absolutely_integrable: - fixes f::"'n::ordered_euclidean_space \ 'm::ordered_euclidean_space" - assumes "\x\s. \i\Basis. 0 \ f(x)\i" "f integrable_on s" + fixes f :: "'n::ordered_euclidean_space \ 'm::ordered_euclidean_space" + assumes "\x\s. \i\Basis. 0 \ f x \ i" + and "f integrable_on s" shows "f absolutely_integrable_on s" unfolding absolutely_integrable_abs_eq apply rule @@ -10818,83 +12214,175 @@ apply (auto simp: euclidean_eq_iff[where 'a='m]) done -lemma absolutely_integrable_integrable_bound: fixes f::"'n::ordered_euclidean_space \ 'm::ordered_euclidean_space" - assumes "\x\s. norm(f x) \ g x" "f integrable_on s" "g integrable_on s" +lemma absolutely_integrable_integrable_bound: + fixes f :: "'n::ordered_euclidean_space \ 'm::ordered_euclidean_space" + assumes "\x\s. norm (f x) \ g x" + and "f integrable_on s" + and "g integrable_on s" shows "f absolutely_integrable_on s" -proof- { presume *:"\f::'n::ordered_euclidean_space \ 'm::ordered_euclidean_space. \ g. \x. norm(f x) \ g x \ f integrable_on UNIV - \ g integrable_on UNIV \ f absolutely_integrable_on UNIV" - show ?thesis apply(subst absolutely_integrable_restrict_univ[symmetric]) - apply(rule *[of _ "\x. if x\s then g x else 0"]) - using assms unfolding integrable_restrict_univ by auto } - fix g and f :: "'n::ordered_euclidean_space \ 'm::ordered_euclidean_space" - assume assms:"\x. norm(f x) \ g x" "f integrable_on UNIV" "g integrable_on UNIV" +proof - + { + presume *: "\f::'n \ 'm. \g. \x. norm (f x) \ g x \ f integrable_on UNIV \ + g integrable_on UNIV \ f absolutely_integrable_on UNIV" + show ?thesis + apply (subst absolutely_integrable_restrict_univ[symmetric]) + apply (rule *[of _ "\x. if x\s then g x else 0"]) + using assms + unfolding integrable_restrict_univ + apply auto + done + } + fix g + fix f :: "'n \ 'm" + assume assms: "\x. norm (f x) \ g x" "f integrable_on UNIV" "g integrable_on UNIV" show "f absolutely_integrable_on UNIV" - apply(rule bounded_variation_absolutely_integrable[OF assms(2),where B="integral UNIV g"]) - proof safe case goal1 note d=this and d'=division_ofD[OF this] + apply (rule bounded_variation_absolutely_integrable[OF assms(2),where B="integral UNIV g"]) + proof safe + case goal1 + note d=this and d'=division_ofD[OF this] have "(\k\d. norm (integral k f)) \ (\k\d. integral k g)" - apply(rule setsum_mono) apply(rule integral_norm_bound_integral) apply(drule_tac[!] d'(4),safe) - apply(rule_tac[1-2] integrable_on_subinterval) using assms by auto - also have "... = integral (\d) g" apply(rule integral_combine_division_bottomup[symmetric]) - apply(rule d,safe) apply(drule d'(4),safe) - apply(rule integrable_on_subinterval[OF assms(3)]) by auto - also have "... \ integral UNIV g" apply(rule integral_subset_le) defer - apply(rule integrable_on_subdivision[OF d,of _ UNIV]) prefer 4 - apply(rule,rule_tac y="norm (f x)" in order_trans) using assms by auto - finally show ?case . qed qed - -lemma absolutely_integrable_integrable_bound_real: fixes f::"'n::ordered_euclidean_space \ real" - assumes "\x\s. norm(f x) \ g x" "f integrable_on s" "g integrable_on s" + apply (rule setsum_mono) + apply (rule integral_norm_bound_integral) + apply (drule_tac[!] d'(4)) + apply safe + apply (rule_tac[1-2] integrable_on_subinterval) + using assms + apply auto + done + also have "\ = integral (\d) g" + apply (rule integral_combine_division_bottomup[symmetric]) + apply (rule d) + apply safe + apply (drule d'(4)) + apply safe + apply (rule integrable_on_subinterval[OF assms(3)]) + apply auto + done + also have "\ \ integral UNIV g" + apply (rule integral_subset_le) + defer + apply (rule integrable_on_subdivision[OF d,of _ UNIV]) + prefer 4 + apply rule + apply (rule_tac y="norm (f x)" in order_trans) + using assms + apply auto + done + finally show ?case . + qed +qed + +lemma absolutely_integrable_integrable_bound_real: + fixes f :: "'n::ordered_euclidean_space \ real" + assumes "\x\s. norm (f x) \ g x" + and "f integrable_on s" + and "g integrable_on s" shows "f absolutely_integrable_on s" - apply(rule absolutely_integrable_integrable_bound[where g=g]) - using assms unfolding o_def by auto + apply (rule absolutely_integrable_integrable_bound[where g=g]) + using assms + unfolding o_def + apply auto + done lemma absolutely_integrable_absolutely_integrable_bound: - fixes f::"'n::ordered_euclidean_space \ 'm::ordered_euclidean_space" and g::"'n::ordered_euclidean_space \ 'p::ordered_euclidean_space" - assumes "\x\s. norm(f x) \ norm(g x)" "f integrable_on s" "g absolutely_integrable_on s" + fixes f :: "'n::ordered_euclidean_space \ 'm::ordered_euclidean_space" + and g :: "'n::ordered_euclidean_space \ 'p::ordered_euclidean_space" + assumes "\x\s. norm (f x) \ norm (g x)" + and "f integrable_on s" + and "g absolutely_integrable_on s" shows "f absolutely_integrable_on s" - apply(rule absolutely_integrable_integrable_bound[of s f "\x. norm (g x)"]) - using assms by auto + apply (rule absolutely_integrable_integrable_bound[of s f "\x. norm (g x)"]) + using assms + apply auto + done lemma absolutely_integrable_inf_real: - assumes "finite k" "k \ {}" - "\i\k. (\x. (fs x i)::real) absolutely_integrable_on s" - shows "(\x. (Inf ((fs x) ` k))) absolutely_integrable_on s" using assms -proof induct case (insert a k) let ?P = " (\x. if fs x ` k = {} then fs x a - else min (fs x a) (Inf (fs x ` k))) absolutely_integrable_on s" - show ?case unfolding image_insert - apply(subst Inf_insert_finite) apply(rule finite_imageI[OF insert(1)]) - proof(cases "k={}") case True - thus ?P apply(subst if_P) defer apply(rule insert(5)[rule_format]) by auto - next case False thus ?P apply(subst if_not_P) defer + assumes "finite k" + and "k \ {}" + and "\i\k. (\x. (fs x i)::real) absolutely_integrable_on s" + shows "(\x. (Inf ((fs x) ` k))) absolutely_integrable_on s" + using assms +proof induct + case (insert a k) + let ?P = "(\x. + if fs x ` k = {} then fs x a + else min (fs x a) (Inf (fs x ` k))) absolutely_integrable_on s" + show ?case + unfolding image_insert + apply (subst Inf_insert_finite) + apply (rule finite_imageI[OF insert(1)]) + proof (cases "k = {}") + case True + then show ?P + apply (subst if_P) + defer + apply (rule insert(5)[rule_format]) + apply auto + done + next + case False + then show ?P + apply (subst if_not_P) + defer apply (rule absolutely_integrable_min[where 'n=real, unfolded Basis_real_def, simplified]) - defer apply(rule insert(3)[OF False]) using insert(5) by auto - qed qed auto + defer + apply(rule insert(3)[OF False]) + using insert(5) + apply auto + done + qed +next + case empty + then show ?case by auto +qed lemma absolutely_integrable_sup_real: - assumes "finite k" "k \ {}" - "\i\k. (\x. (fs x i)::real) absolutely_integrable_on s" - shows "(\x. (Sup ((fs x) ` k))) absolutely_integrable_on s" using assms -proof induct case (insert a k) let ?P = " (\x. if fs x ` k = {} then fs x a - else max (fs x a) (Sup (fs x ` k))) absolutely_integrable_on s" - show ?case unfolding image_insert - apply(subst Sup_insert_finite) apply(rule finite_imageI[OF insert(1)]) - proof(cases "k={}") case True - thus ?P apply(subst if_P) defer apply(rule insert(5)[rule_format]) by auto - next case False thus ?P apply(subst if_not_P) defer + assumes "finite k" + and "k \ {}" + and "\i\k. (\x. (fs x i)::real) absolutely_integrable_on s" + shows "(\x. (Sup ((fs x) ` k))) absolutely_integrable_on s" + using assms +proof induct + case (insert a k) + let ?P = "(\x. + if fs x ` k = {} then fs x a + else max (fs x a) (Sup (fs x ` k))) absolutely_integrable_on s" + show ?case + unfolding image_insert + apply (subst Sup_insert_finite) + apply (rule finite_imageI[OF insert(1)]) + proof (cases "k = {}") + case True + then show ?P + apply (subst if_P) + defer + apply (rule insert(5)[rule_format]) + apply auto + done + next + case False + then show ?P + apply (subst if_not_P) + defer apply (rule absolutely_integrable_max[where 'n=real, unfolded Basis_real_def, simplified]) - defer apply(rule insert(3)[OF False]) using insert(5) by auto - qed qed auto - - -subsection {* Dominated convergence. *} + defer + apply (rule insert(3)[OF False]) + using insert(5) + apply auto + done + qed +qed auto + + +subsection {* Dominated convergence *} lemma dominated_convergence: fixes f :: "nat \ 'n::ordered_euclidean_space \ real" assumes "\k. (f k) integrable_on s" "h integrable_on s" - "\k. \x \ s. norm(f k x) \ (h x)" - "\x \ s. ((\k. f k x) ---> g x) sequentially" + and "\k. \x \ s. norm(f k x) \ (h x)" + and "\x \ s. ((\k. f k x) ---> g x) sequentially" shows "g integrable_on s" - "((\k. integral s (f k)) ---> integral s g) sequentially" + and "((\k. integral s (f k)) ---> integral s g) sequentially" proof - have "\m. (\x. Inf {f j x |j. m \ j}) integrable_on s \ ((\k. integral s (\x. Inf {f j x |j. j \ {m..m + k}})) ---> @@ -10958,20 +12446,20 @@ unfolding setge_def proof safe case goal1 - thus ?case using assms(3)[rule_format,OF x, of j] by auto + then show ?case using assms(3)[rule_format,OF x, of j] by auto qed auto have "\y\?S. \ y \ i + r" proof(rule ccontr) case goal1 - hence "i \ i + r" + then have "i \ i + r" apply - apply (rule isGlb_le_isLb[OF i]) apply (rule isLbI) unfolding setge_def apply fastforce+ done - thus False using r by auto + then show False using r by auto qed then guess y .. note y=this[unfolded not_le] from this(1)[unfolded mem_Collect_eq] guess N .. note N=conjunctD2[OF this] @@ -11060,20 +12548,22 @@ unfolding setle_def proof safe case goal1 - thus ?case using assms(3)[rule_format,OF x, of j] by auto + then show ?case + using assms(3)[rule_format,OF x, of j] by auto qed auto have "\y\?S. \ y \ i - r" proof (rule ccontr) case goal1 - hence "i \ i - r" + then have "i \ i - r" apply - apply (rule isLub_le_isUb[OF i]) apply (rule isUbI) unfolding setle_def apply fastforce+ done - thus False using r by auto + then show False + using r by auto qed then guess y .. note y=this[unfolded not_le] from this(1)[unfolded mem_Collect_eq] guess N .. note N=conjunctD2[OF this] @@ -11142,7 +12632,8 @@ show "(\k::nat. Inf {f j x |j. k \ j}) ----> g x" proof (rule LIMSEQ_I) case goal1 - hence "0 s" show "Sup {f j x |j. k \ j} \ Sup {f j x |j. Suc k \ j}" @@ -11196,7 +12688,8 @@ show "((\k. Sup {f j x |j. k \ j}) ---> g x) sequentially" proof (rule LIMSEQ_I) case goal1 - hence "0 'a::topological_space) \ bool" - where "path g \ continuous_on {0 .. 1} g" + where "path g \ continuous_on {0..1} g" definition pathstart :: "(real \ 'a::topological_space) \ 'a" where "pathstart g = g 0" @@ -22,10 +22,10 @@ definition path_image :: "(real \ 'a::topological_space) \ 'a set" where "path_image g = g ` {0 .. 1}" -definition reversepath :: "(real \ 'a::topological_space) \ (real \ 'a)" +definition reversepath :: "(real \ 'a::topological_space) \ real \ 'a" where "reversepath g = (\x. g(1 - x))" -definition joinpaths :: "(real \ 'a::topological_space) \ (real \ 'a) \ (real \ 'a)" +definition joinpaths :: "(real \ 'a::topological_space) \ (real \ 'a) \ real \ 'a" (infixr "+++" 75) where "g1 +++ g2 = (\x. if x \ 1/2 then g1 (2 * x) else g2 (2 * x - 1))" @@ -40,62 +40,77 @@ subsection {* Some lemmas about these concepts. *} lemma injective_imp_simple_path: "injective_path g \ simple_path g" - unfolding injective_path_def simple_path_def by auto + unfolding injective_path_def simple_path_def + by auto lemma path_image_nonempty: "path_image g \ {}" - unfolding path_image_def image_is_empty interval_eq_empty by auto - -lemma pathstart_in_path_image[intro]: "(pathstart g) \ path_image g" - unfolding pathstart_def path_image_def by auto + unfolding path_image_def image_is_empty interval_eq_empty + by auto -lemma pathfinish_in_path_image[intro]: "(pathfinish g) \ path_image g" - unfolding pathfinish_def path_image_def by auto +lemma pathstart_in_path_image[intro]: "pathstart g \ path_image g" + unfolding pathstart_def path_image_def + by auto -lemma connected_path_image[intro]: "path g \ connected(path_image g)" +lemma pathfinish_in_path_image[intro]: "pathfinish g \ path_image g" + unfolding pathfinish_def path_image_def + by auto + +lemma connected_path_image[intro]: "path g \ connected (path_image g)" unfolding path_def path_image_def apply (erule connected_continuous_image) apply (rule convex_connected, rule convex_real_interval) done -lemma compact_path_image[intro]: "path g \ compact(path_image g)" +lemma compact_path_image[intro]: "path g \ compact (path_image g)" unfolding path_def path_image_def - by (erule compact_continuous_image, rule compact_interval) + apply (erule compact_continuous_image) + apply (rule compact_interval) + done -lemma reversepath_reversepath[simp]: "reversepath(reversepath g) = g" - unfolding reversepath_def by auto +lemma reversepath_reversepath[simp]: "reversepath (reversepath g) = g" + unfolding reversepath_def + by auto -lemma pathstart_reversepath[simp]: "pathstart(reversepath g) = pathfinish g" - unfolding pathstart_def reversepath_def pathfinish_def by auto +lemma pathstart_reversepath[simp]: "pathstart (reversepath g) = pathfinish g" + unfolding pathstart_def reversepath_def pathfinish_def + by auto -lemma pathfinish_reversepath[simp]: "pathfinish(reversepath g) = pathstart g" - unfolding pathstart_def reversepath_def pathfinish_def by auto +lemma pathfinish_reversepath[simp]: "pathfinish (reversepath g) = pathstart g" + unfolding pathstart_def reversepath_def pathfinish_def + by auto lemma pathstart_join[simp]: "pathstart (g1 +++ g2) = pathstart g1" - unfolding pathstart_def joinpaths_def pathfinish_def by auto + unfolding pathstart_def joinpaths_def pathfinish_def + by auto lemma pathfinish_join[simp]: "pathfinish (g1 +++ g2) = pathfinish g2" - unfolding pathstart_def joinpaths_def pathfinish_def by auto + unfolding pathstart_def joinpaths_def pathfinish_def + by auto -lemma path_image_reversepath[simp]: "path_image(reversepath g) = path_image g" +lemma path_image_reversepath[simp]: "path_image (reversepath g) = path_image g" proof - - have *: "\g. path_image(reversepath g) \ path_image g" + have *: "\g. path_image (reversepath g) \ path_image g" unfolding path_image_def subset_eq reversepath_def Ball_def image_iff - apply(rule,rule,erule bexE) - apply(rule_tac x="1 - xa" in bexI) + apply rule + apply rule + apply (erule bexE) + apply (rule_tac x="1 - xa" in bexI) apply auto done show ?thesis using *[of g] *[of "reversepath g"] - unfolding reversepath_reversepath by auto + unfolding reversepath_reversepath + by auto qed -lemma path_reversepath[simp]: "path (reversepath g) \ path g" +lemma path_reversepath [simp]: "path (reversepath g) \ path g" proof - have *: "\g. path g \ path (reversepath g)" unfolding path_def reversepath_def apply (rule continuous_on_compose[unfolded o_def, of _ "\x. 1 - x"]) apply (intro continuous_on_intros) - apply (rule continuous_on_subset[of "{0..1}"], assumption) + apply (rule continuous_on_subset[of "{0..1}"]) + apply assumption apply auto done show ?thesis @@ -116,43 +131,59 @@ have g1: "continuous_on {0..1} g1 \ continuous_on {0..1} ((g1 +++ g2) \ (\x. x / 2))" by (intro continuous_on_cong refl) (auto simp: joinpaths_def) have g2: "continuous_on {0..1} g2 \ continuous_on {0..1} ((g1 +++ g2) \ (\x. x / 2 + 1/2))" - using assms by (intro continuous_on_cong refl) (auto simp: joinpaths_def pathfinish_def pathstart_def) - show "continuous_on {0..1} g1" "continuous_on {0..1} g2" + using assms + by (intro continuous_on_cong refl) (auto simp: joinpaths_def pathfinish_def pathstart_def) + show "continuous_on {0..1} g1" and "continuous_on {0..1} g2" unfolding g1 g2 by (auto intro!: continuous_on_intros continuous_on_subset[OF cont] simp del: o_apply) next assume g1g2: "continuous_on {0..1} g1" "continuous_on {0..1} g2" have 01: "{0 .. 1} = {0..1/2} \ {1/2 .. 1::real}" by auto - { fix x :: real assume "0 \ x" "x \ 1" then have "x \ (\x. x * 2) ` {0..1 / 2}" - by (intro image_eqI[where x="x/2"]) auto } + { + fix x :: real + assume "0 \ x" and "x \ 1" + then have "x \ (\x. x * 2) ` {0..1 / 2}" + by (intro image_eqI[where x="x/2"]) auto + } note 1 = this - { fix x :: real assume "0 \ x" "x \ 1" then have "x \ (\x. x * 2 - 1) ` {1 / 2..1}" - by (intro image_eqI[where x="x/2 + 1/2"]) auto } + { + fix x :: real + assume "0 \ x" and "x \ 1" + then have "x \ (\x. x * 2 - 1) ` {1 / 2..1}" + by (intro image_eqI[where x="x/2 + 1/2"]) auto + } note 2 = this show "continuous_on {0..1} (g1 +++ g2)" - using assms unfolding joinpaths_def 01 - by (intro continuous_on_cases closed_atLeastAtMost g1g2[THEN continuous_on_compose2] continuous_on_intros) - (auto simp: field_simps pathfinish_def pathstart_def intro!: 1 2) + using assms + unfolding joinpaths_def 01 + apply (intro continuous_on_cases closed_atLeastAtMost g1g2[THEN continuous_on_compose2] continuous_on_intros) + apply (auto simp: field_simps pathfinish_def pathstart_def intro!: 1 2) + done qed -lemma path_image_join_subset: "path_image(g1 +++ g2) \ (path_image g1 \ path_image g2)" - unfolding path_image_def joinpaths_def by auto +lemma path_image_join_subset: "path_image (g1 +++ g2) \ path_image g1 \ path_image g2" + unfolding path_image_def joinpaths_def + by auto lemma subset_path_image_join: - assumes "path_image g1 \ s" "path_image g2 \ s" - shows "path_image(g1 +++ g2) \ s" - using path_image_join_subset[of g1 g2] and assms by auto + assumes "path_image g1 \ s" + and "path_image g2 \ s" + shows "path_image (g1 +++ g2) \ s" + using path_image_join_subset[of g1 g2] and assms + by auto lemma path_image_join: assumes "pathfinish g1 = pathstart g2" - shows "path_image(g1 +++ g2) = (path_image g1) \ (path_image g2)" - apply (rule, rule path_image_join_subset, rule) + shows "path_image (g1 +++ g2) = path_image g1 \ path_image g2" + apply rule + apply (rule path_image_join_subset) + apply rule unfolding Un_iff proof (erule disjE) fix x assume "x \ path_image g1" - then obtain y where y: "y\{0..1}" "x = g1 y" + then obtain y where y: "y \ {0..1}" "x = g1 y" unfolding path_image_def image_iff by auto then show "x \ path_image (g1 +++ g2)" unfolding joinpaths_def path_image_def image_iff @@ -162,20 +193,22 @@ next fix x assume "x \ path_image g2" - then obtain y where y: "y\{0..1}" "x = g2 y" + then obtain y where y: "y \ {0..1}" "x = g2 y" unfolding path_image_def image_iff by auto then show "x \ path_image (g1 +++ g2)" unfolding joinpaths_def path_image_def image_iff - apply(rule_tac x="(1/2) *\<^sub>R (y + 1)" in bexI) + apply (rule_tac x="(1/2) *\<^sub>R (y + 1)" in bexI) using assms(1)[unfolded pathfinish_def pathstart_def] - apply (auto simp add: add_divide_distrib) + apply (auto simp add: add_divide_distrib) done qed lemma not_in_path_image_join: - assumes "x \ path_image g1" "x \ path_image g2" - shows "x \ path_image(g1 +++ g2)" - using assms and path_image_join_subset[of g1 g2] by auto + assumes "x \ path_image g1" + and "x \ path_image g2" + shows "x \ path_image (g1 +++ g2)" + using assms and path_image_join_subset[of g1 g2] + by auto lemma simple_path_reversepath: assumes "simple_path g" @@ -184,82 +217,111 @@ unfolding simple_path_def reversepath_def apply - apply (rule ballI)+ - apply (erule_tac x="1-x" in ballE, erule_tac x="1-y" in ballE) + apply (erule_tac x="1-x" in ballE) + apply (erule_tac x="1-y" in ballE) apply auto done lemma simple_path_join_loop: - assumes "injective_path g1" "injective_path g2" "pathfinish g2 = pathstart g1" - "(path_image g1 \ path_image g2) \ {pathstart g1,pathstart g2}" - shows "simple_path(g1 +++ g2)" + assumes "injective_path g1" + and "injective_path g2" + and "pathfinish g2 = pathstart g1" + and "path_image g1 \ path_image g2 \ {pathstart g1, pathstart g2}" + shows "simple_path (g1 +++ g2)" unfolding simple_path_def -proof ((rule ballI)+, rule impI) +proof (intro ballI impI) let ?g = "g1 +++ g2" note inj = assms(1,2)[unfolded injective_path_def, rule_format] fix x y :: real assume xy: "x \ {0..1}" "y \ {0..1}" "?g x = ?g y" show "x = y \ x = 0 \ y = 1 \ x = 1 \ y = 0" - proof (case_tac "x \ 1/2", case_tac[!] "y \ 1/2", unfold not_le) + proof (cases "x \ 1/2", case_tac[!] "y \ 1/2", unfold not_le) assume as: "x \ 1 / 2" "y \ 1 / 2" then have "g1 (2 *\<^sub>R x) = g1 (2 *\<^sub>R y)" - using xy(3) unfolding joinpaths_def by auto - moreover - have "2 *\<^sub>R x \ {0..1}" "2 *\<^sub>R y \ {0..1}" using xy(1,2) as + using xy(3) + unfolding joinpaths_def + by auto + moreover have "2 *\<^sub>R x \ {0..1}" "2 *\<^sub>R y \ {0..1}" + using xy(1,2) as by auto - ultimately - show ?thesis using inj(1)[of "2*\<^sub>R x" "2*\<^sub>R y"] by auto + ultimately show ?thesis + using inj(1)[of "2*\<^sub>R x" "2*\<^sub>R y"] + by auto next - assume as:"x > 1 / 2" "y > 1 / 2" + assume as: "x > 1 / 2" "y > 1 / 2" then have "g2 (2 *\<^sub>R x - 1) = g2 (2 *\<^sub>R y - 1)" - using xy(3) unfolding joinpaths_def by auto - moreover - have "2 *\<^sub>R x - 1 \ {0..1}" "2 *\<^sub>R y - 1 \ {0..1}" - using xy(1,2) as by auto - ultimately - show ?thesis using inj(2)[of "2*\<^sub>R x - 1" "2*\<^sub>R y - 1"] by auto + using xy(3) + unfolding joinpaths_def + by auto + moreover have "2 *\<^sub>R x - 1 \ {0..1}" "2 *\<^sub>R y - 1 \ {0..1}" + using xy(1,2) as + by auto + ultimately show ?thesis + using inj(2)[of "2*\<^sub>R x - 1" "2*\<^sub>R y - 1"] by auto next - assume as:"x \ 1 / 2" "y > 1 / 2" + assume as: "x \ 1 / 2" "y > 1 / 2" then have "?g x \ path_image g1" "?g y \ path_image g2" unfolding path_image_def joinpaths_def using xy(1,2) by auto - moreover - have "?g y \ pathstart g2" using as(2) unfolding pathstart_def joinpaths_def + moreover have "?g y \ pathstart g2" + using as(2) + unfolding pathstart_def joinpaths_def using inj(2)[of "2 *\<^sub>R y - 1" 0] and xy(2) by (auto simp add: field_simps) - ultimately - have *:"?g x = pathstart g1" using assms(4) unfolding xy(3) by auto - then have "x = 0" unfolding pathstart_def joinpaths_def using as(1) and xy(1) - using inj(1)[of "2 *\<^sub>R x" 0] by auto - moreover - have "y = 1" using * unfolding xy(3) assms(3)[THEN sym] - unfolding joinpaths_def pathfinish_def using as(2) and xy(2) - using inj(2)[of "2 *\<^sub>R y - 1" 1] by auto - ultimately show ?thesis by auto + ultimately have *: "?g x = pathstart g1" + using assms(4) + unfolding xy(3) + by auto + then have "x = 0" + unfolding pathstart_def joinpaths_def + using as(1) and xy(1) + using inj(1)[of "2 *\<^sub>R x" 0] + by auto + moreover have "y = 1" + using * + unfolding xy(3) assms(3)[symmetric] + unfolding joinpaths_def pathfinish_def + using as(2) and xy(2) + using inj(2)[of "2 *\<^sub>R y - 1" 1] + by auto + ultimately show ?thesis + by auto next assume as: "x > 1 / 2" "y \ 1 / 2" - then have "?g x \ path_image g2" "?g y \ path_image g1" + then have "?g x \ path_image g2" and "?g y \ path_image g1" unfolding path_image_def joinpaths_def using xy(1,2) by auto - moreover - have "?g x \ pathstart g2" using as(1) unfolding pathstart_def joinpaths_def + moreover have "?g x \ pathstart g2" + using as(1) + unfolding pathstart_def joinpaths_def using inj(2)[of "2 *\<^sub>R x - 1" 0] and xy(1) by (auto simp add: field_simps) - ultimately - have *: "?g y = pathstart g1" using assms(4) unfolding xy(3) by auto - then have "y = 0" unfolding pathstart_def joinpaths_def using as(2) and xy(2) - using inj(1)[of "2 *\<^sub>R y" 0] by auto - moreover - have "x = 1" using * unfolding xy(3)[THEN sym] assms(3)[THEN sym] + ultimately have *: "?g y = pathstart g1" + using assms(4) + unfolding xy(3) + by auto + then have "y = 0" + unfolding pathstart_def joinpaths_def + using as(2) and xy(2) + using inj(1)[of "2 *\<^sub>R y" 0] + by auto + moreover have "x = 1" + using * + unfolding xy(3)[symmetric] assms(3)[symmetric] unfolding joinpaths_def pathfinish_def using as(1) and xy(1) - using inj(2)[of "2 *\<^sub>R x - 1" 1] by auto - ultimately show ?thesis by auto + using inj(2)[of "2 *\<^sub>R x - 1" 1] + by auto + ultimately show ?thesis + by auto qed qed lemma injective_path_join: - assumes "injective_path g1" "injective_path g2" "pathfinish g1 = pathstart g2" - "(path_image g1 \ path_image g2) \ {pathstart g2}" - shows "injective_path(g1 +++ g2)" + assumes "injective_path g1" + and "injective_path g2" + and "pathfinish g1 = pathstart g2" + and "path_image g1 \ path_image g2 \ {pathstart g2}" + shows "injective_path (g1 +++ g2)" unfolding injective_path_def proof (rule, rule, rule) let ?g = "g1 +++ g2" @@ -268,31 +330,39 @@ assume xy: "x \ {0..1}" "y \ {0..1}" "(g1 +++ g2) x = (g1 +++ g2) y" show "x = y" proof (cases "x \ 1/2", case_tac[!] "y \ 1/2", unfold not_le) - assume "x \ 1 / 2" "y \ 1 / 2" - then show ?thesis using inj(1)[of "2*\<^sub>R x" "2*\<^sub>R y"] and xy + assume "x \ 1 / 2" and "y \ 1 / 2" + then show ?thesis + using inj(1)[of "2*\<^sub>R x" "2*\<^sub>R y"] and xy unfolding joinpaths_def by auto next - assume "x > 1 / 2" "y > 1 / 2" - then show ?thesis using inj(2)[of "2*\<^sub>R x - 1" "2*\<^sub>R y - 1"] and xy + assume "x > 1 / 2" and "y > 1 / 2" + then show ?thesis + using inj(2)[of "2*\<^sub>R x - 1" "2*\<^sub>R y - 1"] and xy unfolding joinpaths_def by auto next assume as: "x \ 1 / 2" "y > 1 / 2" - then have "?g x \ path_image g1" "?g y \ path_image g2" + then have "?g x \ path_image g1" and "?g y \ path_image g2" unfolding path_image_def joinpaths_def - using xy(1,2) by auto - then have "?g x = pathfinish g1" "?g y = pathstart g2" - using assms(4) unfolding assms(3) xy(3) by auto + using xy(1,2) + by auto + then have "?g x = pathfinish g1" and "?g y = pathstart g2" + using assms(4) + unfolding assms(3) xy(3) + by auto then show ?thesis using as and inj(1)[of "2 *\<^sub>R x" 1] inj(2)[of "2 *\<^sub>R y - 1" 0] and xy(1,2) unfolding pathstart_def pathfinish_def joinpaths_def by auto next - assume as:"x > 1 / 2" "y \ 1 / 2" - then have "?g x \ path_image g2" "?g y \ path_image g1" + assume as:"x > 1 / 2" "y \ 1 / 2" + then have "?g x \ path_image g2" and "?g y \ path_image g1" unfolding path_image_def joinpaths_def - using xy(1,2) by auto - then have "?g x = pathstart g2" "?g y = pathfinish g1" - using assms(4) unfolding assms(3) xy(3) by auto + using xy(1,2) + by auto + then have "?g x = pathstart g2" and "?g y = pathfinish g1" + using assms(4) + unfolding assms(3) xy(3) + by auto then show ?thesis using as and inj(2)[of "2 *\<^sub>R x - 1" 0] inj(1)[of "2 *\<^sub>R y" 1] and xy(1,2) unfolding pathstart_def pathfinish_def joinpaths_def by auto @@ -300,64 +370,85 @@ qed lemmas join_paths_simps = path_join path_image_join pathstart_join pathfinish_join - + -subsection {* Reparametrizing a closed curve to start at some chosen point. *} +subsection {* Reparametrizing a closed curve to start at some chosen point *} -definition "shiftpath a (f::real \ 'a::topological_space) = - (\x. if (a + x) \ 1 then f(a + x) else f(a + x - 1))" +definition shiftpath :: "real \ (real \ 'a::topological_space) \ real \ 'a" + where "shiftpath a f = (\x. if (a + x) \ 1 then f (a + x) else f (a + x - 1))" -lemma pathstart_shiftpath: "a \ 1 \ pathstart(shiftpath a g) = g a" +lemma pathstart_shiftpath: "a \ 1 \ pathstart (shiftpath a g) = g a" unfolding pathstart_def shiftpath_def by auto lemma pathfinish_shiftpath: - assumes "0 \ a" "pathfinish g = pathstart g" - shows "pathfinish(shiftpath a g) = g a" - using assms unfolding pathstart_def pathfinish_def shiftpath_def + assumes "0 \ a" + and "pathfinish g = pathstart g" + shows "pathfinish (shiftpath a g) = g a" + using assms + unfolding pathstart_def pathfinish_def shiftpath_def by auto lemma endpoints_shiftpath: - assumes "pathfinish g = pathstart g" "a \ {0 .. 1}" - shows "pathfinish(shiftpath a g) = g a" "pathstart(shiftpath a g) = g a" - using assms by(auto intro!:pathfinish_shiftpath pathstart_shiftpath) + assumes "pathfinish g = pathstart g" + and "a \ {0 .. 1}" + shows "pathfinish (shiftpath a g) = g a" + and "pathstart (shiftpath a g) = g a" + using assms + by (auto intro!: pathfinish_shiftpath pathstart_shiftpath) lemma closed_shiftpath: - assumes "pathfinish g = pathstart g" "a \ {0..1}" - shows "pathfinish(shiftpath a g) = pathstart(shiftpath a g)" - using endpoints_shiftpath[OF assms] by auto + assumes "pathfinish g = pathstart g" + and "a \ {0..1}" + shows "pathfinish (shiftpath a g) = pathstart (shiftpath a g)" + using endpoints_shiftpath[OF assms] + by auto lemma path_shiftpath: - assumes "path g" "pathfinish g = pathstart g" "a \ {0..1}" - shows "path(shiftpath a g)" + assumes "path g" + and "pathfinish g = pathstart g" + and "a \ {0..1}" + shows "path (shiftpath a g)" proof - - have *: "{0 .. 1} = {0 .. 1-a} \ {1-a .. 1}" using assms(3) by auto + have *: "{0 .. 1} = {0 .. 1-a} \ {1-a .. 1}" + using assms(3) by auto have **: "\x. x + a = 1 \ g (x + a - 1) = g (x + a)" - using assms(2)[unfolded pathfinish_def pathstart_def] by auto + using assms(2)[unfolded pathfinish_def pathstart_def] + by auto show ?thesis unfolding path_def shiftpath_def * apply (rule continuous_on_union) apply (rule closed_real_atLeastAtMost)+ - apply (rule continuous_on_eq[of _ "g \ (\x. a + x)"]) prefer 3 - apply (rule continuous_on_eq[of _ "g \ (\x. a - 1 + x)"]) defer prefer 3 - apply (rule continuous_on_intros)+ prefer 2 + apply (rule continuous_on_eq[of _ "g \ (\x. a + x)"]) + prefer 3 + apply (rule continuous_on_eq[of _ "g \ (\x. a - 1 + x)"]) + defer + prefer 3 + apply (rule continuous_on_intros)+ + prefer 2 apply (rule continuous_on_intros)+ apply (rule_tac[1-2] continuous_on_subset[OF assms(1)[unfolded path_def]]) using assms(3) and ** - apply (auto, auto simp add: field_simps) + apply auto + apply (auto simp add: field_simps) done qed lemma shiftpath_shiftpath: - assumes "pathfinish g = pathstart g" "a \ {0..1}" "x \ {0..1}" + assumes "pathfinish g = pathstart g" + and "a \ {0..1}" + and "x \ {0..1}" shows "shiftpath (1 - a) (shiftpath a g) x = g x" - using assms unfolding pathfinish_def pathstart_def shiftpath_def by auto + using assms + unfolding pathfinish_def pathstart_def shiftpath_def + by auto lemma path_image_shiftpath: - assumes "a \ {0..1}" "pathfinish g = pathstart g" - shows "path_image(shiftpath a g) = path_image g" + assumes "a \ {0..1}" + and "pathfinish g = pathstart g" + shows "path_image (shiftpath a g) = path_image g" proof - { fix x - assume as:"g 1 = g 0" "x \ {0..1::real}" " \y\{0..1} \ {x. \ a + x \ 1}. g x \ g (a + y - 1)" + assume as: "g 1 = g 0" "x \ {0..1::real}" " \y\{0..1} \ {x. \ a + x \ 1}. g x \ g (a + y - 1)" then have "\y\{0..1} \ {x. a + x \ 1}. g x = g (a + y)" proof (cases "a \ x") case False @@ -368,46 +459,57 @@ done next case True - then show ?thesis using as(1-2) and assms(1) apply(rule_tac x="x - a" in bexI) - by(auto simp add: field_simps) + then show ?thesis + using as(1-2) and assms(1) + apply (rule_tac x="x - a" in bexI) + apply (auto simp add: field_simps) + done qed } then show ?thesis - using assms unfolding shiftpath_def path_image_def pathfinish_def pathstart_def - by(auto simp add: image_iff) + using assms + unfolding shiftpath_def path_image_def pathfinish_def pathstart_def + by (auto simp add: image_iff) qed -subsection {* Special case of straight-line paths. *} +subsection {* Special case of straight-line paths *} definition linepath :: "'a::real_normed_vector \ 'a \ real \ 'a" where "linepath a b = (\x. (1 - x) *\<^sub>R a + x *\<^sub>R b)" -lemma pathstart_linepath[simp]: "pathstart(linepath a b) = a" - unfolding pathstart_def linepath_def by auto +lemma pathstart_linepath[simp]: "pathstart (linepath a b) = a" + unfolding pathstart_def linepath_def + by auto -lemma pathfinish_linepath[simp]: "pathfinish(linepath a b) = b" - unfolding pathfinish_def linepath_def by auto +lemma pathfinish_linepath[simp]: "pathfinish (linepath a b) = b" + unfolding pathfinish_def linepath_def + by auto lemma continuous_linepath_at[intro]: "continuous (at x) (linepath a b)" - unfolding linepath_def by (intro continuous_intros) + unfolding linepath_def + by (intro continuous_intros) lemma continuous_on_linepath[intro]: "continuous_on s (linepath a b)" - using continuous_linepath_at by(auto intro!: continuous_at_imp_continuous_on) + using continuous_linepath_at + by (auto intro!: continuous_at_imp_continuous_on) -lemma path_linepath[intro]: "path(linepath a b)" - unfolding path_def by(rule continuous_on_linepath) +lemma path_linepath[intro]: "path (linepath a b)" + unfolding path_def + by (rule continuous_on_linepath) -lemma path_image_linepath[simp]: "path_image(linepath a b) = (closed_segment a b)" +lemma path_image_linepath[simp]: "path_image (linepath a b) = closed_segment a b" unfolding path_image_def segment linepath_def - apply (rule set_eqI, rule) defer + apply (rule set_eqI) + apply rule + defer unfolding mem_Collect_eq image_iff - apply(erule exE) - apply(rule_tac x="u *\<^sub>R 1" in bexI) + apply (erule exE) + apply (rule_tac x="u *\<^sub>R 1" in bexI) apply auto done -lemma reversepath_linepath[simp]: "reversepath(linepath a b) = linepath b a" +lemma reversepath_linepath[simp]: "reversepath (linepath a b) = linepath b a" unfolding reversepath_def linepath_def by auto @@ -415,25 +517,30 @@ assumes "a \ b" shows "injective_path (linepath a b)" proof - - { fix x y :: "real" + { + fix x y :: "real" assume "x *\<^sub>R b + y *\<^sub>R a = x *\<^sub>R a + y *\<^sub>R b" - then have "(x - y) *\<^sub>R a = (x - y) *\<^sub>R b" by (simp add: algebra_simps) - with assms have "x = y" by simp } + then have "(x - y) *\<^sub>R a = (x - y) *\<^sub>R b" + by (simp add: algebra_simps) + with assms have "x = y" + by simp + } then show ?thesis unfolding injective_path_def linepath_def by (auto simp add: algebra_simps) qed -lemma simple_path_linepath[intro]: "a \ b \ simple_path(linepath a b)" - by(auto intro!: injective_imp_simple_path injective_path_linepath) +lemma simple_path_linepath[intro]: "a \ b \ simple_path (linepath a b)" + by (auto intro!: injective_imp_simple_path injective_path_linepath) -subsection {* Bounding a point away from a path. *} +subsection {* Bounding a point away from a path *} lemma not_on_path_ball: fixes g :: "real \ 'a::heine_borel" - assumes "path g" "z \ path_image g" - shows "\e > 0. ball z e \ (path_image g) = {}" + assumes "path g" + and "z \ path_image g" + shows "\e > 0. ball z e \ path_image g = {}" proof - obtain a where "a \ path_image g" "\y \ path_image g. dist z a \ dist z y" using distance_attains_inf[OF _ path_image_nonempty, of g z] @@ -447,34 +554,43 @@ lemma not_on_path_cball: fixes g :: "real \ 'a::heine_borel" - assumes "path g" "z \ path_image g" + assumes "path g" + and "z \ path_image g" shows "\e>0. cball z e \ (path_image g) = {}" proof - - obtain e where "ball z e \ path_image g = {}" "e>0" + obtain e where "ball z e \ path_image g = {}" "e > 0" using not_on_path_ball[OF assms] by auto - moreover have "cball z (e/2) \ ball z e" using `e>0` by auto - ultimately show ?thesis apply(rule_tac x="e/2" in exI) by auto + moreover have "cball z (e/2) \ ball z e" + using `e > 0` by auto + ultimately show ?thesis + apply (rule_tac x="e/2" in exI) + apply auto + done qed -subsection {* Path component, considered as a "joinability" relation (from Tom Hales). *} +subsection {* Path component, considered as a "joinability" relation (from Tom Hales) *} definition "path_component s x y \ (\g. path g \ path_image g \ s \ pathstart g = x \ pathfinish g = y)" -lemmas path_defs = path_def pathstart_def pathfinish_def path_image_def path_component_def +lemmas path_defs = path_def pathstart_def pathfinish_def path_image_def path_component_def lemma path_component_mem: assumes "path_component s x y" - shows "x \ s" "y \ s" - using assms unfolding path_defs by auto + shows "x \ s" and "y \ s" + using assms + unfolding path_defs + by auto lemma path_component_refl: assumes "x \ s" shows "path_component s x x" unfolding path_defs apply (rule_tac x="\u. x" in exI) - using assms apply (auto intro!:continuous_on_intros) done + using assms + apply (auto intro!: continuous_on_intros) + done lemma path_component_refl_eq: "path_component s x x \ x \ s" by (auto intro!: path_component_mem path_component_refl) @@ -488,21 +604,21 @@ done lemma path_component_trans: - assumes "path_component s x y" "path_component s y z" + assumes "path_component s x y" + and "path_component s y z" shows "path_component s x z" using assms unfolding path_component_def - apply - - apply (erule exE)+ + apply (elim exE) apply (rule_tac x="g +++ ga" in exI) apply (auto simp add: path_image_join) done -lemma path_component_of_subset: "s \ t \ path_component s x y \ path_component t x y" +lemma path_component_of_subset: "s \ t \ path_component s x y \ path_component t x y" unfolding path_component_def by auto -subsection {* Can also consider it as a set, as the name suggests. *} +text {* Can also consider it as a set, as the name suggests. *} lemma path_component_set: "{y. path_component s x y} = @@ -514,13 +630,15 @@ done lemma path_component_subset: "{y. path_component s x y} \ s" - apply (rule, rule path_component_mem(2)) + apply rule + apply (rule path_component_mem(2)) apply auto done lemma path_component_eq_empty: "{y. path_component s x y} = {} \ x \ s" apply rule - apply (drule equals0D[of _ x]) defer + apply (drule equals0D[of _ x]) + defer apply (rule equals0I) unfolding mem_Collect_eq apply (drule path_component_mem(1)) @@ -529,29 +647,35 @@ done -subsection {* Path connectedness of a space. *} +subsection {* Path connectedness of a space *} definition "path_connected s \ - (\x\s. \y\s. \g. path g \ (path_image g) \ s \ pathstart g = x \ pathfinish g = y)" + (\x\s. \y\s. \g. path g \ path_image g \ s \ pathstart g = x \ pathfinish g = y)" lemma path_connected_component: "path_connected s \ (\x\s. \y\s. path_component s x y)" unfolding path_connected_def path_component_def by auto -lemma path_connected_component_set: "path_connected s \ (\x\s. {y. path_component s x y} = s)" +lemma path_connected_component_set: "path_connected s \ (\x\s. {y. path_component s x y} = s)" unfolding path_connected_component - apply (rule, rule, rule, rule path_component_subset) + apply rule + apply rule + apply rule + apply (rule path_component_subset) unfolding subset_eq mem_Collect_eq Ball_def apply auto done -subsection {* Some useful lemmas about path-connectedness. *} +subsection {* Some useful lemmas about path-connectedness *} lemma convex_imp_path_connected: fixes s :: "'a::real_normed_vector set" - assumes "convex s" shows "path_connected s" + assumes "convex s" + shows "path_connected s" unfolding path_connected_def - apply (rule, rule, rule_tac x = "linepath x y" in exI) + apply rule + apply rule + apply (rule_tac x = "linepath x y" in exI) unfolding path_image_linepath using assms [unfolded convex_contains_segment] apply auto @@ -561,26 +685,33 @@ assumes "path_connected s" shows "connected s" unfolding connected_def not_ex - apply (rule, rule, rule ccontr) + apply rule + apply rule + apply (rule ccontr) unfolding not_not - apply (erule conjE)+ + apply (elim conjE) proof - fix e1 e2 assume as: "open e1" "open e2" "s \ e1 \ e2" "e1 \ e2 \ s = {}" "e1 \ s \ {}" "e2 \ s \ {}" - then obtain x1 x2 where obt:"x1\e1\s" "x2\e2\s" by auto - then obtain g where g:"path g" "path_image g \ s" "pathstart g = x1" "pathfinish g = x2" + then obtain x1 x2 where obt:"x1 \ e1 \ s" "x2 \ e2 \ s" + by auto + then obtain g where g: "path g" "path_image g \ s" "pathstart g = x1" "pathfinish g = x2" using assms[unfolded path_connected_def,rule_format,of x1 x2] by auto have *: "connected {0..1::real}" by (auto intro!: convex_connected convex_real_interval) have "{0..1} \ {x \ {0..1}. g x \ e1} \ {x \ {0..1}. g x \ e2}" using as(3) g(2)[unfolded path_defs] by blast moreover have "{x \ {0..1}. g x \ e1} \ {x \ {0..1}. g x \ e2} = {}" - using as(4) g(2)[unfolded path_defs] unfolding subset_eq by auto + using as(4) g(2)[unfolded path_defs] + unfolding subset_eq + by auto moreover have "{x \ {0..1}. g x \ e1} \ {} \ {x \ {0..1}. g x \ e2} \ {}" - using g(3,4)[unfolded path_defs] using obt + using g(3,4)[unfolded path_defs] + using obt by (simp add: ex_in_conv [symmetric], metis zero_le_one order_refl) ultimately show False - using *[unfolded connected_local not_ex, rule_format, of "{x\{0..1}. g x \ e1}" "{x\{0..1}. g x \ e2}"] + using *[unfolded connected_local not_ex, rule_format, + of "{x\{0..1}. g x \ e1}" "{x\{0..1}. g x \ e2}"] using continuous_open_in_preimage[OF g(1)[unfolded path_def] as(1)] using continuous_open_in_preimage[OF g(1)[unfolded path_def] as(2)] by auto @@ -600,20 +731,23 @@ unfolding mem_Collect_eq apply auto done - then obtain e where e:"e>0" "ball y e \ s" - using assms[unfolded open_contains_ball] by auto + then obtain e where e: "e > 0" "ball y e \ s" + using assms[unfolded open_contains_ball] + by auto show "\e > 0. ball y e \ {y. path_component s x y}" apply (rule_tac x=e in exI) - apply (rule,rule `e>0`, rule) + apply (rule,rule `e>0`) + apply rule unfolding mem_ball mem_Collect_eq proof - fix z assume "dist y z < e" then show "path_component s x z" - apply (rule_tac path_component_trans[of _ _ y]) defer + apply (rule_tac path_component_trans[of _ _ y]) + defer apply (rule path_component_of_subset[OF e(2)]) apply (rule convex_imp_path_connected[OF convex_ball, unfolded path_connected_component, rule_format]) - using `e>0` as + using `e > 0` as apply auto done qed @@ -622,16 +756,21 @@ lemma open_non_path_component: fixes s :: "'a::real_normed_vector set" assumes "open s" - shows "open(s - {y. path_component s x y})" + shows "open (s - {y. path_component s x y})" unfolding open_contains_ball proof fix y - assume as: "y\s - {y. path_component s x y}" - then obtain e where e:"e>0" "ball y e \ s" - using assms [unfolded open_contains_ball] by auto + assume as: "y \ s - {y. path_component s x y}" + then obtain e where e: "e > 0" "ball y e \ s" + using assms [unfolded open_contains_ball] + by auto show "\e>0. ball y e \ s - {y. path_component s x y}" apply (rule_tac x=e in exI) - apply (rule, rule `e>0`, rule, rule) defer + apply rule + apply (rule `e>0`) + apply rule + apply rule + defer proof (rule ccontr) fix z assume "z \ ball y e" "\ z \ {y. path_component s x y}" @@ -643,43 +782,49 @@ apply (rule convex_imp_path_connected[OF convex_ball, unfolded path_connected_component, rule_format]) apply auto done - then show False using as by auto + then show False + using as by auto qed (insert e(2), auto) qed lemma connected_open_path_connected: fixes s :: "'a::real_normed_vector set" - assumes "open s" "connected s" + assumes "open s" + and "connected s" shows "path_connected s" unfolding path_connected_component_set proof (rule, rule, rule path_component_subset, rule) fix x y - assume "x \ s" "y \ s" + assume "x \ s" and "y \ s" show "y \ {y. path_component s x y}" proof (rule ccontr) - assume "y \ {y. path_component s x y}" - moreover - have "{y. path_component s x y} \ s \ {}" - using `x\s` path_component_eq_empty path_component_subset[of s x] by auto + assume "\ ?thesis" + moreover have "{y. path_component s x y} \ s \ {}" + using `x \ s` path_component_eq_empty path_component_subset[of s x] + by auto ultimately show False - using `y\s` open_non_path_component[OF assms(1)] open_path_component[OF assms(1)] - using assms(2)[unfolded connected_def not_ex, rule_format, of"{y. path_component s x y}" "s - {y. path_component s x y}"] + using `y \ s` open_non_path_component[OF assms(1)] open_path_component[OF assms(1)] + using assms(2)[unfolded connected_def not_ex, rule_format, + of"{y. path_component s x y}" "s - {y. path_component s x y}"] by auto qed qed lemma path_connected_continuous_image: - assumes "continuous_on s f" "path_connected s" + assumes "continuous_on s f" + and "path_connected s" shows "path_connected (f ` s)" unfolding path_connected_def proof (rule, rule) fix x' y' assume "x' \ f ` s" "y' \ f ` s" - then obtain x y where xy: "x\s" "y\s" "x' = f x" "y' = f y" by auto - guess g using assms(2)[unfolded path_connected_def, rule_format, OF xy(1,2)] .. + then obtain x y where x: "x \ s" and y: "y \ s" and x': "x' = f x" and y': "y' = f y" + by auto + from x y obtain g where "path g \ path_image g \ s \ pathstart g = x \ pathfinish g = y" + using assms(2)[unfolded path_connected_def] by fast then show "\g. path g \ path_image g \ f ` s \ pathstart g = x' \ pathfinish g = y'" - unfolding xy + unfolding x' y' apply (rule_tac x="f \ g" in exI) unfolding path_defs apply (intro conjI continuous_on_compose continuous_on_subset[OF assms(1)]) @@ -688,11 +833,12 @@ qed lemma homeomorphic_path_connectedness: - "s homeomorphic t \ (path_connected s \ path_connected t)" + "s homeomorphic t \ path_connected s \ path_connected t" unfolding homeomorphic_def homeomorphism_def - apply (erule exE|erule conjE)+ + apply (erule exE|erule conjE)+ apply rule - apply (drule_tac f=f in path_connected_continuous_image) prefer 3 + apply (drule_tac f=f in path_connected_continuous_image) + prefer 3 apply (drule_tac f=g in path_connected_continuous_image) apply auto done @@ -702,21 +848,26 @@ lemma path_connected_singleton: "path_connected {a}" unfolding path_connected_def pathstart_def pathfinish_def path_image_def - apply (clarify, rule_tac x="\x. a" in exI, simp add: image_constant_conv) + apply clarify + apply (rule_tac x="\x. a" in exI) + apply (simp add: image_constant_conv) apply (simp add: path_def continuous_on_const) done lemma path_connected_Un: - assumes "path_connected s" "path_connected t" "s \ t \ {}" + assumes "path_connected s" + and "path_connected t" + and "s \ t \ {}" shows "path_connected (s \ t)" unfolding path_connected_component proof (rule, rule) fix x y assume as: "x \ s \ t" "y \ s \ t" - from assms(3) obtain z where "z \ s \ t" by auto + from assms(3) obtain z where "z \ s \ t" + by auto then show "path_component (s \ t) x y" using as and assms(1-2)[unfolded path_connected_component] - apply - + apply - apply (erule_tac[!] UnE)+ apply (rule_tac[2-3] path_component_trans[of _ _ z]) apply (auto simp add:path_component_of_subset [OF Un_upper1] path_component_of_subset[OF Un_upper2]) @@ -740,11 +891,11 @@ qed -subsection {* sphere is path-connected. *} +subsection {* Sphere is path-connected *} lemma path_connected_punctured_universe: assumes "2 \ DIM('a::euclidean_space)" - shows "path_connected((UNIV::'a::euclidean_space set) - {a})" + shows "path_connected ((UNIV::'a set) - {a})" proof - let ?A = "{x::'a. \i\Basis. x \ i < a \ i}" let ?B = "{x::'a. \i\Basis. a \ i < x \ i}" @@ -754,70 +905,87 @@ proof (rule path_connected_UNION) fix i :: 'a assume "i \ Basis" - then show "(\i\Basis. (a \ i - 1)*\<^sub>R i) \ {x::'a. x \ i < a \ i}" by simp + then show "(\i\Basis. (a \ i - 1)*\<^sub>R i) \ {x::'a. x \ i < a \ i}" + by simp show "path_connected {x. x \ i < a \ i}" using convex_imp_path_connected [OF convex_halfspace_lt, of i "a \ i"] by (simp add: inner_commute) qed - have B: "path_connected ?B" unfolding Collect_bex_eq + have B: "path_connected ?B" + unfolding Collect_bex_eq proof (rule path_connected_UNION) fix i :: 'a assume "i \ Basis" - then show "(\i\Basis. (a \ i + 1) *\<^sub>R i) \ {x::'a. a \ i < x \ i}" by simp + then show "(\i\Basis. (a \ i + 1) *\<^sub>R i) \ {x::'a. a \ i < x \ i}" + by simp show "path_connected {x. a \ i < x \ i}" using convex_imp_path_connected [OF convex_halfspace_gt, of "a \ i" i] by (simp add: inner_commute) qed - obtain S :: "'a set" where "S \ Basis" "card S = Suc (Suc 0)" - using ex_card[OF assms] by auto - then obtain b0 b1 :: 'a where "b0 \ Basis" "b1 \ Basis" "b0 \ b1" + obtain S :: "'a set" where "S \ Basis" and "card S = Suc (Suc 0)" + using ex_card[OF assms] + by auto + then obtain b0 b1 :: 'a where "b0 \ Basis" and "b1 \ Basis" and "b0 \ b1" unfolding card_Suc_eq by auto - then have "a + b0 - b1 \ ?A \ ?B" by (auto simp: inner_simps inner_Basis) - then have "?A \ ?B \ {}" by fast + then have "a + b0 - b1 \ ?A \ ?B" + by (auto simp: inner_simps inner_Basis) + then have "?A \ ?B \ {}" + by fast with A B have "path_connected (?A \ ?B)" by (rule path_connected_Un) also have "?A \ ?B = {x. \i\Basis. x \ i \ a \ i}" unfolding neq_iff bex_disj_distrib Collect_disj_eq .. also have "\ = {x. x \ a}" - unfolding euclidean_eq_iff [where 'a='a] by (simp add: Bex_def) - also have "\ = UNIV - {a}" by auto + unfolding euclidean_eq_iff [where 'a='a] + by (simp add: Bex_def) + also have "\ = UNIV - {a}" + by auto finally show ?thesis . qed lemma path_connected_sphere: assumes "2 \ DIM('a::euclidean_space)" - shows "path_connected {x::'a::euclidean_space. norm(x - a) = r}" + shows "path_connected {x::'a. norm (x - a) = r}" proof (rule linorder_cases [of r 0]) assume "r < 0" - then have "{x::'a. norm(x - a) = r} = {}" by auto - then show ?thesis using path_connected_empty by simp + then have "{x::'a. norm(x - a) = r} = {}" + by auto + then show ?thesis + using path_connected_empty by simp next assume "r = 0" - then show ?thesis using path_connected_singleton by simp + then show ?thesis + using path_connected_singleton by simp next assume r: "0 < r" - then have *: "{x::'a. norm(x - a) = r} = (\x. a + r *\<^sub>R x) ` {x. norm x = 1}" - apply - - apply (rule set_eqI, rule) + have *: "{x::'a. norm(x - a) = r} = (\x. a + r *\<^sub>R x) ` {x. norm x = 1}" + apply (rule set_eqI) + apply rule unfolding image_iff apply (rule_tac x="(1/r) *\<^sub>R (x - a)" in bexI) unfolding mem_Collect_eq norm_scaleR + using r apply (auto simp add: scaleR_right_diff_distrib) done have **: "{x::'a. norm x = 1} = (\x. (1/norm x) *\<^sub>R x) ` (UNIV - {0})" - apply (rule set_eqI,rule) + apply (rule set_eqI) + apply rule unfolding image_iff apply (rule_tac x=x in bexI) unfolding mem_Collect_eq - apply (auto split:split_if_asm) + apply (auto split: split_if_asm) done have "continuous_on (UNIV - {0}) (\x::'a. 1 / norm x)" - unfolding field_divide_inverse by (simp add: continuous_on_intros) - then show ?thesis unfolding * ** using path_connected_punctured_universe[OF assms] + unfolding field_divide_inverse + by (simp add: continuous_on_intros) + then show ?thesis + unfolding * ** + using path_connected_punctured_universe[OF assms] by (auto intro!: path_connected_continuous_image continuous_on_intros) qed -lemma connected_sphere: "2 \ DIM('a::euclidean_space) \ connected {x::'a. norm(x - a) = r}" - using path_connected_sphere path_connected_imp_connected by auto +lemma connected_sphere: "2 \ DIM('a::euclidean_space) \ connected {x::'a. norm (x - a) = r}" + using path_connected_sphere path_connected_imp_connected + by auto end diff -r f8147d885600 -r b19242603e92 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Sat Sep 14 22:34:25 2013 +0200 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Sat Sep 14 23:58:58 2013 +0200 @@ -25,7 +25,7 @@ using dist_triangle[of y z x] by (simp add: dist_commute) (* LEGACY *) -lemma lim_subseq: "subseq r \ s ----> l \ (s o r) ----> l" +lemma lim_subseq: "subseq r \ s ----> l \ (s \ r) ----> l" by (rule LIMSEQ_subseq_LIMSEQ) lemmas real_isGlb_unique = isGlb_unique[where 'a=real] @@ -85,7 +85,7 @@ show "topological_basis B" using assms unfolding topological_basis_def proof safe - fix O'::"'a set" + fix O' :: "'a set" assume "open O'" with H obtain f where "\x\O'. f x \ B \ x \ f x \ f x \ O'" by (force intro: bchoice simp: Bex_def) @@ -138,14 +138,14 @@ qed lemma basis_dense: - fixes B::"'a set set" - and f::"'a set \ 'a" + fixes B :: "'a set set" + and f :: "'a set \ 'a" assumes "topological_basis B" and choosefrom_basis: "\B'. B' \ {} \ f B' \ B'" shows "(\X. open X \ X \ {} \ (\B' \ B. f B' \ X))" proof (intro allI impI) - fix X::"'a set" - assume "open X" "X \ {}" + fix X :: "'a set" + assume "open X" and "X \ {}" from topological_basisE[OF `topological_basis B` `open X` choosefrom_basis[OF `X \ {}`]] guess B' . note B' = this then show "\B'\B. f B' \ X" @@ -180,7 +180,7 @@ subsection {* Countable Basis *} locale countable_basis = - fixes B::"'a::topological_space set set" + fixes B :: "'a::topological_space set set" assumes is_basis: "topological_basis B" and countable_basis: "countable B" begin @@ -283,8 +283,9 @@ proof (rule first_countableI[of "(\(a, b). a \ b) ` (A \ B)"], safe) fix a b assume x: "a \ A" "b \ B" - with A(2, 3)[of a] B(2, 3)[of b] show "x \ a \ b" "open (a \ b)" - unfolding mem_Times_iff by (auto intro: open_Times) + with A(2, 3)[of a] B(2, 3)[of b] show "x \ a \ b" and "open (a \ b)" + unfolding mem_Times_iff + by (auto intro: open_Times) next fix S assume "open S" "x \ S" @@ -418,7 +419,7 @@ text{* Infer the "universe" from union of all sets in the topology. *} -definition "topspace T = \{S. openin T S}" +definition "topspace T = \{S. openin T S}" subsubsection {* Main properties of open sets *} @@ -1007,7 +1008,7 @@ lemma islimpt_approachable_le: fixes x :: "'a::metric_space" - shows "x islimpt S \ (\e>0. \x'\ S. x' \ x \ dist x' x <= e)" + shows "x islimpt S \ (\e>0. \x'\ S. x' \ x \ dist x' x \ e)" unfolding islimpt_approachable using approachable_lt_le [where f="\y. dist y x" and P="\y. y \ S \ y = x", THEN arg_cong [where f=Not]] @@ -1043,7 +1044,7 @@ lemma finite_set_avoid: fixes a :: "'a::metric_space" assumes fS: "finite S" - shows "\d>0. \x\S. x \ a \ d <= dist a x" + shows "\d>0. \x\S. x \ a \ d \ dist a x" proof (induct rule: finite_induct[OF fS]) case 1 then show ?case by (auto intro: zero_less_one) @@ -1423,8 +1424,9 @@ apply (drule_tac x=UNIV in spec, simp) done -lemma not_trivial_limit_within: "~trivial_limit (at x within S) = (x:closure(S-{x}))" - using islimpt_in_closure by (metis trivial_limit_within) +lemma not_trivial_limit_within: "\ trivial_limit (at x within S) = (x \ closure (S - {x}))" + using islimpt_in_closure + by (metis trivial_limit_within) text {* Some property holds "sufficiently close" to the limit point. *} @@ -1463,19 +1465,19 @@ text{* Show that they yield usual definitions in the various cases. *} lemma Lim_within_le: "(f ---> l)(at a within S) \ - (\e>0. \d>0. \x\S. 0 < dist x a \ dist x a <= d \ dist (f x) l < e)" + (\e>0. \d>0. \x\S. 0 < dist x a \ dist x a \ d \ dist (f x) l < e)" by (auto simp add: tendsto_iff eventually_at_le dist_nz) lemma Lim_within: "(f ---> l) (at a within S) \ - (\e >0. \d>0. \x \ S. 0 < dist x a \ dist x a < d \ dist (f x) l < e)" + (\e >0. \d>0. \x \ S. 0 < dist x a \ dist x a < d \ dist (f x) l < e)" by (auto simp add: tendsto_iff eventually_at dist_nz) lemma Lim_at: "(f ---> l) (at a) \ - (\e >0. \d>0. \x. 0 < dist x a \ dist x a < d \ dist (f x) l < e)" + (\e >0. \d>0. \x. 0 < dist x a \ dist x a < d \ dist (f x) l < e)" by (auto simp add: tendsto_iff eventually_at2) lemma Lim_at_infinity: - "(f ---> l) at_infinity \ (\e>0. \b. \x. norm x >= b \ dist (f x) l < e)" + "(f ---> l) at_infinity \ (\e>0. \b. \x. norm x \ b \ dist (f x) l < e)" by (auto simp add: tendsto_iff eventually_at_infinity) lemma Lim_eventually: "eventually (\x. f x = l) net \ (f ---> l) net" @@ -1489,7 +1491,8 @@ lemma Lim_Un: assumes "(f ---> l) (at x within S)" "(f ---> l) (at x within T)" shows "(f ---> l) (at x within (S \ T))" - using assms unfolding tendsto_def eventually_at_filter + using assms + unfolding tendsto_def eventually_at_filter apply clarify apply (drule spec, drule (1) mp, drule (1) mp) apply (drule spec, drule (1) mp, drule (1) mp) @@ -1515,10 +1518,10 @@ from assms obtain T where T: "open T" "x \ T" "T \ S" .. { assume "?lhs" - then obtain A where "open A" "x \ A" "\y\A. y \ x \ y \ S \ P y" + then obtain A where "open A" and "x \ A" and "\y\A. y \ x \ y \ S \ P y" unfolding eventually_at_topological by auto - with T have "open (A \ T)" "x \ A \ T" "\y\(A \ T). y \ x \ P y" + with T have "open (A \ T)" and "x \ A \ T" and "\y \ A \ T. y \ x \ P y" by auto then show "?rhs" unfolding eventually_at_topological by auto @@ -1546,11 +1549,11 @@ assumes mono: "\a b. a \ I \ b \ I \ x < a \ a \ b \ f a \ f b" and bnd: "\a. a \ I \ x < a \ K \ f a" shows "(f ---> Inf (f ` ({x<..} \ I))) (at x within ({x<..} \ I))" -proof cases - assume "{x<..} \ I = {}" +proof (cases "{x<..} \ I = {}") + case True then show ?thesis by (simp add: Lim_within_empty) next - assume e: "{x<..} \ I \ {}" + case False show ?thesis proof (rule order_tendstoI) fix a @@ -1558,7 +1561,7 @@ { fix y assume "y \ {x<..} \ I" - with e bnd have "Inf (f ` ({x<..} \ I)) \ f y" + with False bnd have "Inf (f ` ({x<..} \ I)) \ f y" by (auto intro: cInf_lower) with a have "a < f y" by (blast intro: less_le_trans) @@ -1568,7 +1571,7 @@ next fix a assume "Inf (f ` ({x<..} \ I)) < a" - from cInf_lessD[OF _ this] e obtain y where y: "x < y" "y \ I" "f y < a" + from cInf_lessD[OF _ this] False obtain y where y: "x < y" "y \ I" "f y < a" by auto then have "eventually (\x. x \ I \ f x < a) (at_right x)" unfolding eventually_at_right by (metis less_imp_le le_less_trans mono) @@ -1625,7 +1628,7 @@ and A :: "'a filter" assumes "(f ---> l) A" and "l \ 0" - shows "((inverse o f) ---> inverse l) A" + shows "((inverse \ f) ---> inverse l) A" unfolding o_def using assms by (rule tendsto_inverse) lemma Lim_null: @@ -1646,7 +1649,7 @@ lemma Lim_transform_bound: fixes f :: "'a \ 'b::real_normed_vector" and g :: "'a \ 'c::real_normed_vector" - assumes "eventually (\n. norm(f n) <= norm(g n)) net" + assumes "eventually (\n. norm (f n) \ norm (g n)) net" and "(g ---> 0) net" shows "(f ---> 0) net" using assms(1) tendsto_norm_zero [OF assms(2)] @@ -1657,7 +1660,7 @@ lemma Lim_in_closed_set: assumes "closed S" and "eventually (\x. f(x) \ S) net" - and "\(trivial_limit net)" "(f ---> l) net" + and "\ trivial_limit net" "(f ---> l) net" shows "l \ S" proof (rule ccontr) assume "l \ S" @@ -1676,8 +1679,8 @@ lemma Lim_dist_ubound: assumes "\(trivial_limit net)" and "(f ---> l) net" - and "eventually (\x. dist a (f x) <= e) net" - shows "dist a l <= e" + and "eventually (\x. dist a (f x) \ e) net" + shows "dist a l \ e" proof - have "dist a l \ {..e}" proof (rule Lim_in_closed_set) @@ -1714,7 +1717,9 @@ lemma Lim_norm_lbound: fixes f :: "'a \ 'b::real_normed_vector" - assumes "\ (trivial_limit net)" "(f ---> l) net" "eventually (\x. e <= norm(f x)) net" + assumes "\ trivial_limit net" + and "(f ---> l) net" + and "eventually (\x. e \ norm (f x)) net" shows "e \ norm l" proof - have "norm l \ {e..}" @@ -1946,7 +1951,7 @@ lemma not_trivial_limit_within_ball: - "(\ trivial_limit (at x within S)) = (\e>0. S \ ball x e - {x} \ {})" + "\ trivial_limit (at x within S) \ (\e>0. S \ ball x e - {x} \ {})" (is "?lhs = ?rhs") proof - { @@ -1954,12 +1959,12 @@ { fix e :: real assume "e > 0" - then obtain y where "y:(S-{x}) & dist y x < e" + then obtain y where "y \ S - {x}" and "dist y x < e" using `?lhs` not_trivial_limit_within[of x S] closure_approachable[of x "S - {x}"] by auto - then have "y : (S Int ball x e - {x})" + then have "y \ S \ ball x e - {x}" unfolding ball_def by (simp add: dist_commute) - then have "S Int ball x e - {x} ~= {}" by blast + then have "S \ ball x e - {x} \ {}" by blast } then have "?rhs" by auto } @@ -1969,11 +1974,11 @@ { fix e :: real assume "e > 0" - then obtain y where "y : (S Int ball x e - {x})" + then obtain y where "y \ S \ ball x e - {x}" using `?rhs` by blast - then have "y:(S-{x}) & dist y x < e" - unfolding ball_def by (simp add: dist_commute) - then have "EX y:(S-{x}). dist y x < e" + then have "y \ S - {x}" and "dist y x < e" + unfolding ball_def by (simp_all add: dist_commute) + then have "\y \ S - {x}. dist y x < e" by auto } then have "?lhs" @@ -2004,16 +2009,18 @@ assumes "a \ A" shows "infdist a A = 0" proof - - from infdist_le[OF assms, of "dist a a"] have "infdist a A \ 0" by auto - with infdist_nonneg[of a A] assms show "infdist a A = 0" by auto + from infdist_le[OF assms, of "dist a a"] have "infdist a A \ 0" + by auto + with infdist_nonneg[of a A] assms show "infdist a A = 0" + by auto qed lemma infdist_triangle: "infdist x A \ infdist y A + dist x y" -proof cases - assume "A = {}" +proof (cases "A = {}") + case True then show ?thesis by (simp add: infdist_def) next - assume "A \ {}" + case False then obtain a where "a \ A" by auto have "infdist x A \ Inf {dist x y + dist y a |a. a \ A}" proof (rule cInf_greatest) @@ -2202,7 +2209,7 @@ ultimately show "?rhs" by auto next assume "?rhs" - then have "e>0" by auto + then have "e > 0" by auto { fix d :: real assume "d > 0" @@ -2340,7 +2347,7 @@ lemma interior_cball: fixes x :: "'a::{real_normed_vector, perfect_space}" shows "interior (cball x e) = ball x e" -proof (cases "e\0") +proof (cases "e \ 0") case False note cs = this from cs have "ball x e = {}" using ball_empty[of e x] by auto @@ -2409,7 +2416,9 @@ then have "\S \ cball x e. open S \ S \ ball x e" by auto ultimately show ?thesis - using interior_unique[of "ball x e" "cball x e"] using open_ball[of x e] by auto + using interior_unique[of "ball x e" "cball x e"] + using open_ball[of x e] + by auto qed lemma frontier_ball: @@ -2422,13 +2431,13 @@ lemma frontier_cball: fixes a :: "'a::{real_normed_vector, perfect_space}" - shows "frontier(cball a e) = {x. dist a x = e}" + shows "frontier (cball a e) = {x. dist a x = e}" apply (simp add: frontier_def interior_cball closed_cball order_less_imp_le) apply (simp add: set_eq_iff) apply arith done -lemma cball_eq_empty: "(cball x e = {}) \ e < 0" +lemma cball_eq_empty: "cball x e = {} \ e < 0" apply (simp add: set_eq_iff not_le) apply (metis zero_le_dist dist_self order_less_le_trans) done @@ -2438,7 +2447,7 @@ lemma cball_eq_sing: fixes x :: "'a::{metric_space,perfect_space}" - shows "(cball x e = {x}) \ e = 0" + shows "cball x e = {x} \ e = 0" proof (rule linorder_cases) assume e: "0 < e" obtain a where "a \ x" "dist a x < e" @@ -2466,7 +2475,8 @@ lemma bounded_any_center: "bounded S \ (\e. \y\S. dist a y \ e)" unfolding bounded_def apply safe - apply (rule_tac x="dist a x + e" in exI, clarify) + apply (rule_tac x="dist a x + e" in exI) + apply clarify apply (drule (1) bspec) apply (erule order_trans [OF dist_triangle add_left_mono]) apply auto @@ -2526,7 +2536,7 @@ apply auto done -lemma bounded_ball[simp,intro]: "bounded(ball x e)" +lemma bounded_ball[simp,intro]: "bounded (ball x e)" by (metis ball_subset_cball bounded_cball bounded_subset) lemma bounded_Un[simp]: "bounded (S \ T) \ bounded S \ bounded T" @@ -2534,14 +2544,16 @@ apply (rename_tac x y r s) apply (rule_tac x=x in exI) apply (rule_tac x="max r (dist x y + s)" in exI) - apply (rule ballI, rename_tac z, safe) - apply (drule (1) bspec, simp) + apply (rule ballI) + apply safe + apply (drule (1) bspec) + apply simp apply (drule (1) bspec) apply (rule min_max.le_supI2) apply (erule order_trans [OF dist_triangle add_left_mono]) done -lemma bounded_Union[intro]: "finite F \ (\S\F. bounded S) \ bounded(\F)" +lemma bounded_Union[intro]: "finite F \ \S\F. bounded S \ bounded (\F)" by (induct rule: finite_induct[of F]) auto lemma bounded_UN [intro]: "finite A \ \x\A. bounded (B x) \ bounded (\x\A. B x)" @@ -2549,22 +2561,27 @@ lemma bounded_insert [simp]: "bounded (insert x S) \ bounded S" proof - - have "\y\{x}. dist x y \ 0" by simp - then have "bounded {x}" unfolding bounded_def by fast - then show ?thesis by (metis insert_is_Un bounded_Un) + have "\y\{x}. dist x y \ 0" + by simp + then have "bounded {x}" + unfolding bounded_def by fast + then show ?thesis + by (metis insert_is_Un bounded_Un) qed lemma finite_imp_bounded [intro]: "finite S \ bounded S" by (induct set: finite) simp_all -lemma bounded_pos: "bounded S \ (\b>0. \x\ S. norm x <= b)" +lemma bounded_pos: "bounded S \ (\b>0. \x\ S. norm x \ b)" apply (simp add: bounded_iff) - apply (subgoal_tac "\x (y::real). 0 < 1 + abs y \ (x <= y \ x <= 1 + abs y)") + apply (subgoal_tac "\x (y::real). 0 < 1 + abs y \ (x \ y \ x \ 1 + abs y)") apply metis apply arith done -lemma Bseq_eq_bounded: "Bseq f \ bounded (range f::_::real_normed_vector set)" +lemma Bseq_eq_bounded: + fixes f :: "nat \ 'a::real_normed_vector" + shows "Bseq f \ bounded (range f)" unfolding Bseq_def bounded_pos by auto lemma bounded_Int[intro]: "bounded S \ bounded T \ bounded (S \ T)" @@ -2575,11 +2592,13 @@ lemma not_bounded_UNIV[simp, intro]: "\ bounded (UNIV :: 'a::{real_normed_vector, perfect_space} set)" -proof(auto simp add: bounded_pos not_le) +proof (auto simp add: bounded_pos not_le) obtain x :: 'a where "x \ 0" using perfect_choose_dist [OF zero_less_one] by fast - fix b::real assume b: "b >0" - have b1: "b +1 \ 0" using b by simp + fix b :: real + assume b: "b >0" + have b1: "b +1 \ 0" + using b by simp with `x \ 0` have "b < norm (scaleR (b + 1) (sgn x))" by (simp add: norm_sgn) then show "\x::'a. b < norm x" .. @@ -2590,15 +2609,17 @@ and "bounded_linear f" shows "bounded (f ` S)" proof - - from assms(1) obtain b where b:"b>0" "\x\S. norm x \ b" + from assms(1) obtain b where b: "b > 0" "\x\S. norm x \ b" unfolding bounded_pos by auto - from assms(2) obtain B where B:"B>0" "\x. norm (f x) \ B * norm x" + from assms(2) obtain B where B: "B > 0" "\x. norm (f x) \ B * norm x" using bounded_linear.pos_bounded by (auto simp add: mult_ac) { fix x - assume "x\S" - then have "norm x \ b" using b by auto - then have "norm (f x) \ B * b" using B(2) + assume "x \ S" + then have "norm x \ b" + using b by auto + then have "norm (f x) \ B * b" + using B(2) apply (erule_tac x=x in allE) apply (metis B(1) B(2) order_trans mult_le_cancel_left_pos) done @@ -2624,11 +2645,11 @@ assumes "bounded S" shows "bounded ((\x. a + x) ` S)" proof - - from assms obtain b where b:"b>0" "\x\S. norm x \ b" + from assms obtain b where b: "b > 0" "\x\S. norm x \ b" unfolding bounded_pos by auto { fix x - assume "x\S" + assume "x \ S" then have "norm (a + x) \ b + norm a" using norm_triangle_ineq[of a x] b by auto } @@ -2648,7 +2669,8 @@ lemma bounded_has_Sup: fixes S :: "real set" - assumes "bounded S" "S \ {}" + assumes "bounded S" + and "S \ {}" shows "\x\S. x \ Sup S" and "\b. (\x\S. x \ b) \ Sup S \ b" proof @@ -2679,18 +2701,19 @@ lemma bounded_has_Inf: fixes S :: "real set" - assumes "bounded S" "S \ {}" + assumes "bounded S" + and "S \ {}" shows "\x\S. x \ Inf S" and "\b. (\x\S. x \ b) \ Inf S \ b" proof fix x - assume "x\S" + assume "x \ S" from assms(1) obtain a where a: "\x\S. \x\ \ a" unfolding bounded_real by auto - then show "x \ Inf S" using `x\S` + then show "x \ Inf S" using `x \ S` by (metis cInf_lower_EX abs_le_D2 minus_le_iff) next - show "\b. (\x\S. x >= b) \ Inf S \ b" + show "\b. (\x\S. x \ b) \ Inf S \ b" using assms by (metis cInf_greatest) qed @@ -2715,25 +2738,29 @@ subsubsection {* Bolzano-Weierstrass property *} lemma heine_borel_imp_bolzano_weierstrass: - assumes "compact s" and "infinite t" and "t \ s" + assumes "compact s" + and "infinite t" + and "t \ s" shows "\x \ s. x islimpt t" proof (rule ccontr) assume "\ (\x \ s. x islimpt t)" - then obtain f where f:"\x\s. x \ f x \ open (f x) \ (\y\t. y \ f x \ y = x)" + then obtain f where f: "\x\s. x \ f x \ open (f x) \ (\y\t. y \ f x \ y = x)" unfolding islimpt_def using bchoice[of s "\ x T. x \ T \ open T \ (\y\t. y \ T \ y = x)"] by auto - obtain g where g: "g\{t. \x. x \ s \ t = f x}" "finite g" "s \ \g" + obtain g where g: "g \ {t. \x. x \ s \ t = f x}" "finite g" "s \ \g" using assms(1)[unfolded compact_eq_heine_borel, THEN spec[where x="{t. \x. x\s \ t = f x}"]] using f by auto - from g(1,3) have g':"\x\g. \xa \ s. x = f xa" by auto + from g(1,3) have g':"\x\g. \xa \ s. x = f xa" + by auto { fix x y - assume "x\t" "y\t" "f x = f y" + assume "x \ t" "y \ t" "f x = f y" then have "x \ f x" "y \ f x \ y = x" - using f[THEN bspec[where x=x]] and `t\s` by auto + using f[THEN bspec[where x=x]] and `t \ s` by auto then have "x = y" - using `f x = f y` and f[THEN bspec[where x=y]] and `y\t` and `t\s` by auto + using `f x = f y` and f[THEN bspec[where x=y]] and `y \ t` and `t \ s` + by auto } then have "inj_on f t" unfolding inj_on_def by simp @@ -2742,14 +2769,17 @@ moreover { fix x - assume "x\t" "f x \ g" - from g(3) assms(3) `x\t` obtain h where "h\g" and "x\h" by auto - then obtain y where "y\s" "h = f y" + assume "x \ t" "f x \ g" + from g(3) assms(3) `x \ t` obtain h where "h \ g" and "x \ h" + by auto + then obtain y where "y \ s" "h = f y" using g'[THEN bspec[where x=h]] by auto then have "y = x" - using f[THEN bspec[where x=y]] and `x\t` and `x\h`[unfolded `h = f y`] by auto + using f[THEN bspec[where x=y]] and `x\t` and `x\h`[unfolded `h = f y`] + by auto then have False - using `f x \ g` `h\g` unfolding `h = f y` by auto + using `f x \ g` `h \ g` unfolding `h = f y` + by auto } then have "f ` t \ g" by auto ultimately show False @@ -2786,7 +2816,8 @@ proof (rule topological_tendstoI) fix S assume "open S" "l \ S" - with A(3) have "eventually (\i. A i \ S) sequentially" by auto + with A(3) have "eventually (\i. A i \ S) sequentially" + by auto moreover { fix i @@ -2810,12 +2841,18 @@ shows "infinite (range f)" proof assume "finite (range f)" - then have "closed (range f)" by (rule finite_imp_closed) - then have "open (- range f)" by (rule open_Compl) - from assms(1) have "l \ - range f" by auto + then have "closed (range f)" + by (rule finite_imp_closed) + then have "open (- range f)" + by (rule open_Compl) + from assms(1) have "l \ - range f" + by auto from assms(2) have "eventually (\n. f n \ - range f) sequentially" - using `open (- range f)` `l \ - range f` by (rule topological_tendstoD) - then show False unfolding eventually_sequentially by auto + using `open (- range f)` `l \ - range f` + by (rule topological_tendstoD) + then show False + unfolding eventually_sequentially + by auto qed lemma closure_insert: @@ -2928,7 +2965,7 @@ qed lemma bolzano_weierstrass_imp_closed: - fixes s :: "'a::{first_countable_topology, t2_space} set" + fixes s :: "'a::{first_countable_topology,t2_space} set" assumes "\t. infinite t \ t \ s --> (\x \ s. x islimpt t)" shows "closed s" proof - @@ -3276,7 +3313,7 @@ definition seq_compact :: "'a::topological_space set \ bool" where "seq_compact S \ - (\f. (\n. f n \ S) \ (\l\S. \r. subseq r \ ((f o r) ---> l) sequentially))" + (\f. (\n. f n \ S) \ (\l\S. \r. subseq r \ ((f \ r) ---> l) sequentially))" lemma seq_compact_imp_countably_compact: fixes U :: "'a :: first_countable_topology set" @@ -3391,7 +3428,7 @@ qed lemma seq_compactI: - assumes "\f. \n. f n \ S \ \l\S. \r. subseq r \ ((f o r) ---> l) sequentially" + assumes "\f. \n. f n \ S \ \l\S. \r. subseq r \ ((f \ r) ---> l) sequentially" shows "seq_compact S" unfolding seq_compact_def using assms by fast @@ -3611,7 +3648,7 @@ lemma compact_def: "compact (S :: 'a::metric_space set) \ - (\f. (\n. f n \ S) \ (\l\S. \r. subseq r \ (f o r) ----> l))" + (\f. (\n. f n \ S) \ (\l\S. \r. subseq r \ (f \ r) ----> l))" unfolding compact_eq_seq_compact_metric seq_compact_def by auto subsubsection {* Complete the chain of compactness variants *} @@ -4514,7 +4551,7 @@ fixes f :: "'a::metric_space \ 'b::topological_space" shows "continuous (at a within s) f \ (\x. (\n::nat. x n \ s) \ (x ---> a) sequentially - \ ((f o x) ---> f a) sequentially)" + \ ((f \ x) ---> f a) sequentially)" (is "?lhs = ?rhs") proof assume ?lhs @@ -4546,14 +4583,14 @@ lemma continuous_at_sequentially: fixes f :: "'a::metric_space \ 'b::topological_space" shows "continuous (at a) f \ - (\x. (x ---> a) sequentially --> ((f o x) ---> f a) sequentially)" + (\x. (x ---> a) sequentially --> ((f \ x) ---> f a) sequentially)" using continuous_within_sequentially[of a UNIV f] by simp lemma continuous_on_sequentially: fixes f :: "'a::metric_space \ 'b::topological_space" shows "continuous_on s f \ (\x. \a \ s. (\n. x(n) \ s) \ (x ---> a) sequentially - --> ((f o x) ---> f(a)) sequentially)" + --> ((f \ x) ---> f a) sequentially)" (is "?lhs = ?rhs") proof assume ?rhs @@ -4804,8 +4841,8 @@ lemma uniformly_continuous_on_compose[continuous_on_intros]: assumes "uniformly_continuous_on s f" "uniformly_continuous_on (f ` s) g" - shows "uniformly_continuous_on s (g o f)" -proof- + shows "uniformly_continuous_on s (g \ f)" +proof - { fix e :: real assume "e > 0" @@ -6818,7 +6855,7 @@ lemma Lim_component_eq: fixes f :: "'a \ 'b::euclidean_space" - assumes net: "(f ---> l) net" "~(trivial_limit net)" + assumes net: "(f ---> l) net" "\ trivial_limit net" and ev:"eventually (\x. f(x)\i = b) net" shows "l\i = b" using ev[unfolded order_eq_iff eventually_conj_iff] @@ -6887,8 +6924,7 @@ (\x\s. (g(f x) = x)) \ (f ` s = t) \ continuous_on s f \ (\y\t. (f(g y) = y)) \ (g ` t = s) \ continuous_on t g" -definition - homeomorphic :: "'a::topological_space set \ 'b::topological_space set \ bool" +definition homeomorphic :: "'a::topological_space set \ 'b::topological_space set \ bool" (infixr "homeomorphic" 60) where "s homeomorphic t \ (\f g. homeomorphism s t f g)" @@ -7099,12 +7135,12 @@ lemma cauchy_isometric: fixes x :: "nat \ 'a::euclidean_space" - assumes e: "0 < e" + assumes e: "e > 0" and s: "subspace s" and f: "bounded_linear f" - and normf: "\x\s. norm(f x) \ e * norm(x)" - and xs: "\n::nat. x n \ s" - and cf: "Cauchy(f o x)" + and normf: "\x\s. norm (f x) \ e * norm x" + and xs: "\n. x n \ s" + and cf: "Cauchy (f \ x)" shows "Cauchy x" proof - interpret f: bounded_linear f by fact @@ -7145,24 +7181,31 @@ fix g assume as:"\n::nat. g n \ f ` s" and cfg:"Cauchy g" then obtain x where "\n. x n \ s \ g n = f (x n)" - using choice[of "\ n xa. xa \ s \ g n = f xa"] by auto - then have x:"\n. x n \ s" "\n. g n = f (x n)" by auto - then have "f \ x = g" unfolding fun_eq_iff by auto + using choice[of "\ n xa. xa \ s \ g n = f xa"] + by auto + then have x:"\n. x n \ s" "\n. g n = f (x n)" + by auto + then have "f \ x = g" + unfolding fun_eq_iff + by auto then obtain l where "l\s" and l:"(x ---> l) sequentially" using cs[unfolded complete_def, THEN spec[where x="x"]] - using cauchy_isometric[OF `0l\f ` s. (g ---> l) sequentially" using linear_continuous_at[OF f, unfolded continuous_at_sequentially, THEN spec[where x=x], of l] - unfolding `f \ x = g` by auto + unfolding `f \ x = g` + by auto } - then show ?thesis unfolding complete_def by auto + then show ?thesis + unfolding complete_def by auto qed lemma injective_imp_isometric: fixes f :: "'a::euclidean_space \ 'b::euclidean_space" assumes s: "closed s" "subspace s" - and f: "bounded_linear f" "\x\s. (f x = 0) \ (x = 0)" - shows "\e>0. \x\s. norm (f x) \ e * norm(x)" + and f: "bounded_linear f" "\x\s. f x = 0 \ x = 0" + shows "\e>0. \x\s. norm (f x) \ e * norm x" proof (cases "s \ {0::'a}") case True { @@ -7175,8 +7218,10 @@ next interpret f: bounded_linear f by fact case False - then obtain a where a:"a\0" "a\s" by auto - from False have "s \ {}" by auto + then obtain a where a: "a \ 0" "a \ s" + by auto + from False have "s \ {}" + by auto let ?S = "{f x| x. (x \ s \ norm x = norm a)}" let ?S' = "{x::'a. x\s \ norm x = norm a}" let ?S'' = "{x::'a. norm x = norm a}" diff -r f8147d885600 -r b19242603e92 src/Tools/jEdit/etc/options --- a/src/Tools/jEdit/etc/options Sat Sep 14 22:34:25 2013 +0200 +++ b/src/Tools/jEdit/etc/options Sat Sep 14 23:58:58 2013 +0200 @@ -21,7 +21,7 @@ public option jedit_tooltip_margin : int = 60 -- "margin for tooltip pretty-printing" -public option jedit_text_overview_limit : int = 100000 +public option jedit_text_overview_limit : int = 65536 -- "maximum amount of text to visualize in overview column" public option jedit_symbols_search_limit : int = 50