src/HOL/Multivariate_Analysis/Integration.thy
changeset 44170 510ac30f44c0
parent 44167 e81d676d598e
child 44176 eda112e9cdee
     1.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Fri Aug 12 07:18:28 2011 -0700
     1.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Fri Aug 12 09:17:24 2011 -0700
     1.3 @@ -1584,11 +1584,11 @@
     1.4      have lem1: "\<And>f P Q. (\<forall>x k. (x,k) \<in> {(x,f k) | x k. P x k} \<longrightarrow> Q x k) \<longleftrightarrow> (\<forall>x k. P x k \<longrightarrow> Q x (f k))" by auto
     1.5      have lem2: "\<And>f s P f. finite s \<Longrightarrow> finite {(x,f k) | x k. (x,k) \<in> s \<and> P x k}"
     1.6      proof- case goal1 thus ?case apply-apply(rule finite_subset[of _ "(\<lambda>(x,k). (x,f k)) ` s"]) by auto qed
     1.7 -    have lem3: "\<And>g::('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool. finite p \<Longrightarrow>
     1.8 +    have lem3: "\<And>g::'a set \<Rightarrow> 'a set. finite p \<Longrightarrow>
     1.9        setsum (\<lambda>(x,k). content k *\<^sub>R f x) {(x,g k) |x k. (x,k) \<in> p \<and> ~(g k = {})}
    1.10                 = setsum (\<lambda>(x,k). content k *\<^sub>R f x) ((\<lambda>(x,k). (x,g k)) ` p)"
    1.11        apply(rule setsum_mono_zero_left) prefer 3
    1.12 -    proof fix g::"('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" and i::"('a) \<times> (('a) set)"
    1.13 +    proof fix g::"'a set \<Rightarrow> 'a set" and i::"('a) \<times> (('a) set)"
    1.14        assume "i \<in> (\<lambda>(x, k). (x, g k)) ` p - {(x, g k) |x k. (x, k) \<in> p \<and> g k \<noteq> {}}"
    1.15        then obtain x k where xk:"i=(x,g k)" "(x,k)\<in>p" "(x,g k) \<notin> {(x, g k) |x k. (x, k) \<in> p \<and> g k \<noteq> {}}" by auto
    1.16        have "content (g k) = 0" using xk using content_empty by auto
    1.17 @@ -3004,9 +3004,9 @@
    1.18  
    1.19  lemma gauge_modify:
    1.20    assumes "(\<forall>s. open s \<longrightarrow> open {x. f(x) \<in> s})" "gauge d"
    1.21 -  shows "gauge (\<lambda>x y. d (f x) (f y))"
    1.22 +  shows "gauge (\<lambda>x. {y. f y \<in> d (f x)})"
    1.23    using assms unfolding gauge_def apply safe defer apply(erule_tac x="f x" in allE)
    1.24 -  apply(erule_tac x="d (f x)" in allE) unfolding mem_def Collect_def by auto
    1.25 +  apply(erule_tac x="d (f x)" in allE) by auto
    1.26  
    1.27  subsection {* Only need trivial subintervals if the interval itself is trivial. *}
    1.28  
    1.29 @@ -3194,7 +3194,7 @@
    1.30    show ?thesis unfolding has_integral_def has_integral_compact_interval_def apply(subst if_P) apply(rule,rule,rule wz)
    1.31    proof safe fix e::real assume e:"e>0" hence "e * r > 0" using assms(1) by(rule mult_pos_pos)
    1.32      from assms(8)[unfolded has_integral,rule_format,OF this] guess d apply-by(erule exE conjE)+ note d=this[rule_format]
    1.33 -    def d' \<equiv> "\<lambda>x y. d (g x) (g y)" have d':"\<And>x. d' x = {y. g y \<in> (d (g x))}" unfolding d'_def by(auto simp add:mem_def)
    1.34 +    def d' \<equiv> "\<lambda>x. {y. g y \<in> d (g x)}" have d':"\<And>x. d' x = {y. g y \<in> (d (g x))}" unfolding d'_def ..
    1.35      show "\<exists>d. gauge d \<and> (\<forall>p. p tagged_division_of h ` {a..b} \<and> d fine p \<longrightarrow> norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f (g x)) - (1 / r) *\<^sub>R i) < e)"
    1.36      proof(rule_tac x=d' in exI,safe) show "gauge d'" using d(1) unfolding gauge_def d' using continuous_open_preimage_univ[OF assms(4)] by auto
    1.37        fix p assume as:"p tagged_division_of h ` {a..b}" "d' fine p" note p = tagged_division_ofD[OF as(1)]