src/HOL/Analysis/Set_Integral.thy
changeset 63886 685fb01256af
parent 63627 6ddb43c6b711
child 63941 f353674c2528
--- a/src/HOL/Analysis/Set_Integral.thy	Thu Sep 15 22:41:05 2016 +0200
+++ b/src/HOL/Analysis/Set_Integral.thy	Fri Sep 16 13:56:51 2016 +0200
@@ -7,7 +7,7 @@
 *)
 
 theory Set_Integral
-  imports Bochner_Integration Lebesgue_Measure
+  imports Equivalence_Lebesgue_Henstock_Integration
 begin
 
 (*
@@ -85,7 +85,7 @@
 lemma set_lebesgue_integral_cong:
   assumes "A \<in> sets M" and "\<forall>x. x \<in> A \<longrightarrow> f x = g x"
   shows "(LINT x:A|M. f x) = (LINT x:A|M. g x)"
-  using assms by (auto intro!: integral_cong split: split_indicator simp add: sets.sets_into_space)
+  using assms by (auto intro!: Bochner_Integration.integral_cong split: split_indicator simp add: sets.sets_into_space)
 
 lemma set_lebesgue_integral_cong_AE:
   assumes [measurable]: "A \<in> sets M" "f \<in> borel_measurable M" "g \<in> borel_measurable M"
@@ -118,22 +118,22 @@
 (* TODO: borel_integrable_atLeastAtMost should be named something like set_integrable_Icc_isCont *)
 
 lemma set_integral_scaleR_right [simp]: "LINT t:A|M. a *\<^sub>R f t = a *\<^sub>R (LINT t:A|M. f t)"
-  by (subst integral_scaleR_right[symmetric]) (auto intro!: integral_cong)
+  by (subst integral_scaleR_right[symmetric]) (auto intro!: Bochner_Integration.integral_cong)
 
 lemma set_integral_mult_right [simp]:
   fixes a :: "'a::{real_normed_field, second_countable_topology}"
   shows "LINT t:A|M. a * f t = a * (LINT t:A|M. f t)"
-  by (subst integral_mult_right_zero[symmetric]) (auto intro!: integral_cong)
+  by (subst integral_mult_right_zero[symmetric]) auto
 
 lemma set_integral_mult_left [simp]:
   fixes a :: "'a::{real_normed_field, second_countable_topology}"
   shows "LINT t:A|M. f t * a = (LINT t:A|M. f t) * a"
-  by (subst integral_mult_left_zero[symmetric]) (auto intro!: integral_cong)
+  by (subst integral_mult_left_zero[symmetric]) auto
 
 lemma set_integral_divide_zero [simp]:
   fixes a :: "'a::{real_normed_field, field, second_countable_topology}"
   shows "LINT t:A|M. f t / a = (LINT t:A|M. f t) / a"
-  by (subst integral_divide_zero[symmetric], intro integral_cong)
+  by (subst integral_divide_zero[symmetric], intro Bochner_Integration.integral_cong)
      (auto split: split_indicator)
 
 lemma set_integrable_scaleR_right [simp, intro]:
@@ -184,7 +184,7 @@
   fixes S and f :: "real \<Rightarrow> 'a :: {banach, second_countable_topology}"
   shows "(LBINT x : S. f x) = (LBINT x : {x. - x \<in> S}. f (- x))"
   by (subst lborel_integral_real_affine[where c="-1" and t=0])
-     (auto intro!: integral_cong split: split_indicator)
+     (auto intro!: Bochner_Integration.integral_cong split: split_indicator)
 
 (* question: why do we have this for negation, but multiplication by a constant
    requires an integrability assumption? *)
@@ -194,7 +194,7 @@
 lemma set_integral_complex_of_real:
   "LINT x:A|M. complex_of_real (f x) = of_real (LINT x:A|M. f x)"
   by (subst integral_complex_of_real[symmetric])
-     (auto intro!: integral_cong split: split_indicator)
+     (auto intro!: Bochner_Integration.integral_cong split: split_indicator)
 
 lemma set_integral_mono:
   fixes f g :: "_ \<Rightarrow> real"
@@ -254,7 +254,7 @@
 proof -
   have "set_integrable M (A - B) f"
     using f_A by (rule set_integrable_subset) auto
-  from integrable_add[OF this f_B] show ?thesis
+  from Bochner_Integration.integrable_add[OF this f_B] show ?thesis
     by (rule integrable_cong[THEN iffD1, rotated 2]) (auto split: split_indicator)
 qed
 
@@ -410,7 +410,7 @@
       by simp
   qed
   show "set_lebesgue_integral M (UNION UNIV A) f = LINT x|M. (\<Sum>i. indicator (A i) x *\<^sub>R f x)"
-    apply (rule integral_cong[OF refl])
+    apply (rule Bochner_Integration.integral_cong[OF refl])
     apply (subst suminf_scaleR_left[OF sums_summable[OF indicator_sums, OF disj], symmetric])
     using sums_unique[OF indicator_sums[OF disj]]
     apply auto