src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
changeset 64272 f76b6dda2e56
parent 64267 b9a1486e79be
child 64287 d85d88722745
     1.1 --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Mon Oct 17 14:37:32 2016 +0200
     1.2 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Mon Oct 17 17:33:07 2016 +0200
     1.3 @@ -56,7 +56,7 @@
     1.4    where "content s \<equiv> measure lborel s"
     1.5  
     1.6  lemma content_cbox_cases:
     1.7 -  "content (cbox a b) = (if \<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i then setprod (\<lambda>i. b\<bullet>i - a\<bullet>i) Basis else 0)"
     1.8 +  "content (cbox a b) = (if \<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i then prod (\<lambda>i. b\<bullet>i - a\<bullet>i) Basis else 0)"
     1.9    by (simp add: measure_lborel_cbox_eq inner_diff)
    1.10  
    1.11  lemma content_cbox: "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i \<Longrightarrow> content (cbox a b) = (\<Prod>i\<in>Basis. b\<bullet>i - a\<bullet>i)"
    1.12 @@ -84,7 +84,7 @@
    1.13    using not_le by blast
    1.14  
    1.15  lemma content_pos_lt: "\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i \<Longrightarrow> 0 < content (cbox a b)"
    1.16 -  by (auto simp: less_imp_le inner_diff box_eq_empty intro!: setprod_pos)
    1.17 +  by (auto simp: less_imp_le inner_diff box_eq_empty intro!: prod_pos)
    1.18  
    1.19  lemma content_eq_0: "content (cbox a b) = 0 \<longleftrightarrow> (\<exists>i\<in>Basis. b\<bullet>i \<le> a\<bullet>i)"
    1.20    by (auto simp: content_cbox_cases not_le intro: less_imp_le antisym eq_refl)
    1.21 @@ -93,7 +93,7 @@
    1.22    unfolding content_eq_0 interior_cbox box_eq_empty by auto
    1.23  
    1.24  lemma content_pos_lt_eq: "0 < content (cbox a (b::'a::euclidean_space)) \<longleftrightarrow> (\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i)"
    1.25 -  by (auto simp add: content_cbox_cases less_le setprod_nonneg)
    1.26 +  by (auto simp add: content_cbox_cases less_le prod_nonneg)
    1.27  
    1.28  lemma content_empty [simp]: "content {} = 0"
    1.29    by simp
    1.30 @@ -110,9 +110,9 @@
    1.31  
    1.32  lemma content_Pair: "content (cbox (a,c) (b,d)) = content (cbox a b) * content (cbox c d)"
    1.33    unfolding measure_lborel_cbox_eq Basis_prod_def
    1.34 -  apply (subst setprod.union_disjoint)
    1.35 +  apply (subst prod.union_disjoint)
    1.36    apply (auto simp: bex_Un ball_Un)
    1.37 -  apply (subst (1 2) setprod.reindex_nontrivial)
    1.38 +  apply (subst (1 2) prod.reindex_nontrivial)
    1.39    apply auto
    1.40    done
    1.41  
    1.42 @@ -138,7 +138,7 @@
    1.43      apply (subst *(1))
    1.44      defer
    1.45      apply (subst *(1))
    1.46 -    unfolding setprod.insert[OF *(2-)]
    1.47 +    unfolding prod.insert[OF *(2-)]
    1.48      apply auto
    1.49      done
    1.50    assume as: "\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i"
    1.51 @@ -151,7 +151,7 @@
    1.52        (\<Prod>i\<in>Basis. (if i = k then min (b \<bullet> k) c else b \<bullet> i) - a \<bullet> i)"
    1.53      "(\<Prod>i\<in>Basis. b \<bullet> i - ((\<Sum>i\<in>Basis. (if i = k then max (a \<bullet> k) c else a \<bullet> i) *\<^sub>R i) \<bullet> i)) =
    1.54        (\<Prod>i\<in>Basis. b \<bullet> i - (if i = k then max (a \<bullet> k) c else a \<bullet> i))"
    1.55 -    by (auto intro!: setprod.cong)
    1.56 +    by (auto intro!: prod.cong)
    1.57    have "\<not> a \<bullet> k \<le> c \<Longrightarrow> \<not> c \<le> b \<bullet> k \<Longrightarrow> False"
    1.58      unfolding not_le
    1.59      using as[unfolded ,rule_format,of k] assms
    1.60 @@ -1876,7 +1876,7 @@
    1.61      by (auto simp: b'_def a'_def intro!: tendsto_min tendsto_max tendsto_eq_intros)
    1.62    also have "(\<Prod>j\<in>Basis. (b' 0 - a' 0) \<bullet> j) = 0"
    1.63      using k *
    1.64 -    by (intro setprod_zero bexI[OF _ k])
    1.65 +    by (intro prod_zero bexI[OF _ k])
    1.66         (auto simp: b'_def a'_def inner_diff inner_sum_left inner_not_same_Basis intro!: sum.cong)
    1.67    also have "((\<lambda>d. \<Prod>j\<in>Basis. (b' d - a' d) \<bullet> j) \<longlongrightarrow> 0) (at_right 0) =
    1.68      ((\<lambda>d. content (cbox a b \<inter> {x. \<bar>x\<bullet>k - c\<bar> \<le> d})) \<longlongrightarrow> 0) (at_right 0)"
    1.69 @@ -3472,7 +3472,7 @@
    1.70    also have "\<dots> = (\<Prod>j\<in>Basis. emeasure lborel (if j = k then {c} else UNIV))"
    1.71      by (intro measure_times) auto
    1.72    also have "\<dots> = 0"
    1.73 -    by (intro setprod_zero bexI[OF _ k]) auto
    1.74 +    by (intro prod_zero bexI[OF _ k]) auto
    1.75    finally show ?thesis
    1.76      by (subst AE_iff_measurable[OF _ refl]) auto
    1.77  qed
    1.78 @@ -3494,13 +3494,13 @@
    1.79    show ?thesis
    1.80      using m unfolding eq measure_def
    1.81      by (subst lborel_affine_euclidean[where c=m and t=0])
    1.82 -       (simp_all add: emeasure_density measurable_sets_borel[OF s] abs_setprod nn_integral_cmult
    1.83 -                      s_def[symmetric] emeasure_distr vimage_comp s_comp_s enn2real_mult setprod_nonneg)
    1.84 +       (simp_all add: emeasure_density measurable_sets_borel[OF s] abs_prod nn_integral_cmult
    1.85 +                      s_def[symmetric] emeasure_distr vimage_comp s_comp_s enn2real_mult prod_nonneg)
    1.86  next
    1.87    assume "\<not> (\<forall>k\<in>Basis. m k \<noteq> 0)"
    1.88    then obtain k where k: "k \<in> Basis" "m k = 0" by auto
    1.89    then have [simp]: "(\<Prod>k\<in>Basis. m k) = 0"
    1.90 -    by (intro setprod_zero) auto
    1.91 +    by (intro prod_zero) auto
    1.92    have "emeasure lborel {x\<in>space lborel. x \<in> s m ` cbox a b} = 0"
    1.93    proof (rule emeasure_eq_0_AE)
    1.94      show "AE x in lborel. x \<notin> s m ` cbox a b"
    1.95 @@ -3539,7 +3539,7 @@
    1.96        by (simp add: inner_simps field_simps)
    1.97      ultimately show ?thesis
    1.98        by (simp add: image_affinity_cbox True content_cbox'
    1.99 -        setprod.distrib setprod_constant inner_diff_left)
   1.100 +        prod.distrib prod_constant inner_diff_left)
   1.101    next
   1.102      case False
   1.103      with \<open>cbox a b \<noteq> {}\<close> have "cbox (m *\<^sub>R b + c) (m *\<^sub>R a + c) \<noteq> {}"
   1.104 @@ -3552,7 +3552,7 @@
   1.105        by (simp add: inner_simps field_simps)
   1.106      ultimately show ?thesis using False
   1.107        by (simp add: image_affinity_cbox content_cbox'
   1.108 -        setprod.distrib[symmetric] setprod_constant[symmetric] inner_diff_left)
   1.109 +        prod.distrib[symmetric] prod_constant[symmetric] inner_diff_left)
   1.110    qed
   1.111  qed
   1.112  
   1.113 @@ -3589,7 +3589,7 @@
   1.114    assumes "(f has_integral i) (cbox a b)"
   1.115      and "\<forall>k\<in>Basis. m k \<noteq> 0"
   1.116    shows "((\<lambda>x. f (\<Sum>k\<in>Basis. (m k * (x\<bullet>k))*\<^sub>R k)) has_integral
   1.117 -         ((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.118 +         ((1/ \<bar>prod 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.119  apply (rule has_integral_twiddle[where f=f])
   1.120  unfolding zero_less_abs_iff content_image_stretch_interval
   1.121  unfolding image_stretch_interval empty_as_interval euclidean_eq_iff[where 'a='a]
   1.122 @@ -7371,7 +7371,8 @@
   1.123  subsection \<open>Integration by parts\<close>
   1.124  
   1.125  lemma integration_by_parts_interior_strong:
   1.126 -  assumes bilinear: "bounded_bilinear (prod :: _ \<Rightarrow> _ \<Rightarrow> 'b :: banach)"
   1.127 +  fixes prod :: "_ \<Rightarrow> _ \<Rightarrow> 'b :: banach"
   1.128 +  assumes bilinear: "bounded_bilinear (prod)"
   1.129    assumes s: "finite s" and le: "a \<le> b"
   1.130    assumes cont [continuous_intros]: "continuous_on {a..b} f" "continuous_on {a..b} g"
   1.131    assumes deriv: "\<And>x. x\<in>{a<..<b} - s \<Longrightarrow> (f has_vector_derivative f' x) (at x)"
   1.132 @@ -7389,7 +7390,8 @@
   1.133  qed
   1.134  
   1.135  lemma integration_by_parts_interior:
   1.136 -  assumes "bounded_bilinear (prod :: _ \<Rightarrow> _ \<Rightarrow> 'b :: banach)" "a \<le> b"
   1.137 +  fixes prod :: "_ \<Rightarrow> _ \<Rightarrow> 'b :: banach"
   1.138 +  assumes "bounded_bilinear (prod)" "a \<le> b"
   1.139            "continuous_on {a..b} f" "continuous_on {a..b} g"
   1.140    assumes "\<And>x. x\<in>{a<..<b} \<Longrightarrow> (f has_vector_derivative f' x) (at x)"
   1.141            "\<And>x. x\<in>{a<..<b} \<Longrightarrow> (g has_vector_derivative g' x) (at x)"
   1.142 @@ -7398,7 +7400,8 @@
   1.143    by (rule integration_by_parts_interior_strong[of _ "{}" _ _ f g f' g']) (insert assms, simp_all)
   1.144  
   1.145  lemma integration_by_parts:
   1.146 -  assumes "bounded_bilinear (prod :: _ \<Rightarrow> _ \<Rightarrow> 'b :: banach)" "a \<le> b"
   1.147 +  fixes prod :: "_ \<Rightarrow> _ \<Rightarrow> 'b :: banach"
   1.148 +  assumes "bounded_bilinear (prod)" "a \<le> b"
   1.149            "continuous_on {a..b} f" "continuous_on {a..b} g"
   1.150    assumes "\<And>x. x\<in>{a..b} \<Longrightarrow> (f has_vector_derivative f' x) (at x)"
   1.151            "\<And>x. x\<in>{a..b} \<Longrightarrow> (g has_vector_derivative g' x) (at x)"
   1.152 @@ -7407,7 +7410,8 @@
   1.153    by (rule integration_by_parts_interior[of _ _ _ f g f' g']) (insert assms, simp_all)
   1.154  
   1.155  lemma integrable_by_parts_interior_strong:
   1.156 -  assumes bilinear: "bounded_bilinear (prod :: _ \<Rightarrow> _ \<Rightarrow> 'b :: banach)"
   1.157 +  fixes prod :: "_ \<Rightarrow> _ \<Rightarrow> 'b :: banach"
   1.158 +  assumes bilinear: "bounded_bilinear (prod)"
   1.159    assumes s: "finite s" and le: "a \<le> b"
   1.160    assumes cont [continuous_intros]: "continuous_on {a..b} f" "continuous_on {a..b} g"
   1.161    assumes deriv: "\<And>x. x\<in>{a<..<b} - s \<Longrightarrow> (f has_vector_derivative f' x) (at x)"
   1.162 @@ -7424,7 +7428,8 @@
   1.163  qed
   1.164  
   1.165  lemma integrable_by_parts_interior:
   1.166 -  assumes "bounded_bilinear (prod :: _ \<Rightarrow> _ \<Rightarrow> 'b :: banach)" "a \<le> b"
   1.167 +  fixes prod :: "_ \<Rightarrow> _ \<Rightarrow> 'b :: banach"
   1.168 +  assumes "bounded_bilinear (prod)" "a \<le> b"
   1.169            "continuous_on {a..b} f" "continuous_on {a..b} g"
   1.170    assumes "\<And>x. x\<in>{a<..<b} \<Longrightarrow> (f has_vector_derivative f' x) (at x)"
   1.171            "\<And>x. x\<in>{a<..<b} \<Longrightarrow> (g has_vector_derivative g' x) (at x)"
   1.172 @@ -7433,7 +7438,8 @@
   1.173    by (rule integrable_by_parts_interior_strong[of _ "{}" _ _ f g f' g']) (insert assms, simp_all)
   1.174  
   1.175  lemma integrable_by_parts:
   1.176 -  assumes "bounded_bilinear (prod :: _ \<Rightarrow> _ \<Rightarrow> 'b :: banach)" "a \<le> b"
   1.177 +  fixes prod :: "_ \<Rightarrow> _ \<Rightarrow> 'b :: banach"
   1.178 +  assumes "bounded_bilinear (prod)" "a \<le> b"
   1.179            "continuous_on {a..b} f" "continuous_on {a..b} g"
   1.180    assumes "\<And>x. x\<in>{a..b} \<Longrightarrow> (f has_vector_derivative f' x) (at x)"
   1.181            "\<And>x. x\<in>{a..b} \<Longrightarrow> (g has_vector_derivative g' x) (at x)"