src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
changeset 63928 d81fb5b46a5c
parent 63918 6bf55e6e0b75
child 63938 f6ce08859d4c
     1.1 --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Wed Sep 21 14:20:07 2016 +0100
     1.2 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Wed Sep 21 16:59:51 2016 +0100
     1.3 @@ -5894,7 +5894,7 @@
     1.4    assumes "0 < r"
     1.5      and "\<forall>x. h(g x) = x"
     1.6      and "\<forall>x. g(h x) = x"
     1.7 -    and "\<forall>x. continuous (at x) g"
     1.8 +    and contg: "\<And>x. continuous (at x) g"
     1.9      and "\<forall>u v. \<exists>w z. g ` cbox u v = cbox w z"
    1.10      and "\<forall>u v. \<exists>w z. h ` cbox u v = cbox w z"
    1.11      and "\<forall>u v. content(g ` cbox u v) = r * content (cbox u v)"
    1.12 @@ -5947,7 +5947,7 @@
    1.13        show "gauge d'"
    1.14          using d(1)
    1.15          unfolding gauge_def d'
    1.16 -        using continuous_open_preimage_univ[OF assms(4)]
    1.17 +        using continuous_open_preimage_univ[OF _ contg]
    1.18          by auto
    1.19        fix p
    1.20        assume as: "p tagged_division_of h ` cbox a b" "d' fine p"
    1.21 @@ -5985,7 +5985,7 @@
    1.22          proof -
    1.23            assume as: "interior k \<inter> interior k' = {}"
    1.24            have "z \<in> g ` (interior k \<inter> interior k')"
    1.25 -            using interior_image_subset[OF assms(4) inj(1)] z
    1.26 +            using interior_image_subset[OF \<open>inj g\<close> contg] z
    1.27              unfolding image_Int[OF inj(1)] by blast
    1.28            then show False
    1.29              using as by blast
    1.30 @@ -6178,20 +6178,13 @@
    1.31    assumes "(f has_integral i) (cbox a b)"
    1.32      and "\<forall>k\<in>Basis. m k \<noteq> 0"
    1.33    shows "((\<lambda>x. f (\<Sum>k\<in>Basis. (m k * (x\<bullet>k))*\<^sub>R k)) has_integral
    1.34 -    ((1/ \<bar>setprod m Basis\<bar>) *\<^sub>R i)) ((\<lambda>x. (\<Sum>k\<in>Basis. (1 / m k * (x\<bullet>k))*\<^sub>R k)) ` cbox a b)"
    1.35 -  apply (rule has_integral_twiddle[where f=f])
    1.36 -  unfolding zero_less_abs_iff content_image_stretch_interval
    1.37 -  unfolding image_stretch_interval empty_as_interval euclidean_eq_iff[where 'a='a]
    1.38 -  using assms
    1.39 -proof -
    1.40 -  show "\<forall>y::'a. continuous (at y) (\<lambda>x. (\<Sum>k\<in>Basis. (m k * (x\<bullet>k))*\<^sub>R k))"
    1.41 -    apply rule
    1.42 -    apply (rule linear_continuous_at)
    1.43 -    unfolding linear_linear
    1.44 -    unfolding linear_iff inner_simps euclidean_eq_iff[where 'a='a]
    1.45 -    apply (auto simp add: field_simps)
    1.46 -    done
    1.47 -qed auto
    1.48 +         ((1/ \<bar>setprod m Basis\<bar>) *\<^sub>R i)) ((\<lambda>x. (\<Sum>k\<in>Basis. (1 / m k * (x\<bullet>k))*\<^sub>R k)) ` cbox a b)"
    1.49 +apply (rule has_integral_twiddle[where f=f])
    1.50 +unfolding zero_less_abs_iff content_image_stretch_interval
    1.51 +unfolding image_stretch_interval empty_as_interval euclidean_eq_iff[where 'a='a]
    1.52 +using assms
    1.53 +by auto
    1.54 + 
    1.55  
    1.56  lemma integrable_stretch:
    1.57    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
    1.58 @@ -6199,14 +6192,9 @@
    1.59      and "\<forall>k\<in>Basis. m k \<noteq> 0"
    1.60    shows "(\<lambda>x::'a. f (\<Sum>k\<in>Basis. (m k * (x\<bullet>k))*\<^sub>R k)) integrable_on
    1.61      ((\<lambda>x. \<Sum>k\<in>Basis. (1 / m k * (x\<bullet>k))*\<^sub>R k) ` cbox a b)"
    1.62 -  using assms
    1.63 -  unfolding integrable_on_def
    1.64 -  apply -
    1.65 -  apply (erule exE)
    1.66 -  apply (drule has_integral_stretch)
    1.67 -  apply assumption
    1.68 -  apply auto
    1.69 -  done
    1.70 +  using assms unfolding integrable_on_def
    1.71 +  by (force dest: has_integral_stretch)
    1.72 +
    1.73  
    1.74  subsection \<open>even more special cases.\<close>
    1.75