# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1523716609 -3600
# Node ID a8177d098b74a3bc709945ad9dd48d1f4429dac6
# Parent  53323937ee2599ae30995caa6b95b86bc4c8b94f
a few new theorems and some fixes

diff -r 53323937ee25 -r a8177d098b74 src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Sat Apr 14 09:23:00 2018 +0100
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Sat Apr 14 15:36:49 2018 +0100
@@ -971,8 +971,7 @@
   fixes f :: "'a :: euclidean_space \<Rightarrow> real"
   assumes f: "f integrable_on A" and "\<And>x. x \<in> A \<Longrightarrow> 0 \<le> f x"
   shows "f absolutely_integrable_on A"
-  apply (rule absolutely_integrable_onI [OF f])
-  using assms by (simp add: integrable_eq)
+  by (rule absolutely_integrable_onI [OF f]) (use assms in \<open>simp add: integrable_eq\<close>)
 
 lemma absolutely_integrable_on_iff_nonneg:
   fixes f :: "'a :: euclidean_space \<Rightarrow> real"
@@ -1002,6 +1001,46 @@
   by (simp add: norm_mult)
 qed auto
 
+lemma absolutely_integrable_spike:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  assumes "f absolutely_integrable_on T" and S: "negligible S" "\<And>x. x \<in> T - S \<Longrightarrow> g x = f x"
+  shows "g absolutely_integrable_on T"
+  using assms integrable_spike
+  unfolding absolutely_integrable_on_def by metis
+
+lemma absolutely_integrable_negligible:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  assumes "negligible S"
+  shows "f absolutely_integrable_on S"
+  using assms by (simp add: absolutely_integrable_on_def integrable_negligible)
+
+lemma absolutely_integrable_spike_eq:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  assumes "negligible S" "\<And>x. x \<in> T - S \<Longrightarrow> g x = f x"
+  shows "(f absolutely_integrable_on T \<longleftrightarrow> g absolutely_integrable_on T)"
+  using assms by (blast intro: absolutely_integrable_spike sym)
+
+lemma absolutely_integrable_spike_set_eq:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  assumes "negligible {x \<in> S - T. f x \<noteq> 0}" "negligible {x \<in> T - S. f x \<noteq> 0}"
+  shows "(f absolutely_integrable_on S \<longleftrightarrow> f absolutely_integrable_on T)"
+proof -
+  have "(\<lambda>x. if x \<in> S then f x else 0) absolutely_integrable_on UNIV \<longleftrightarrow>
+        (\<lambda>x. if x \<in> T then f x else 0) absolutely_integrable_on UNIV"
+  proof (rule absolutely_integrable_spike_eq)
+    show "negligible ({x \<in> S - T. f x \<noteq> 0} \<union> {x \<in> T - S. f x \<noteq> 0})"
+      by (rule negligible_Un [OF assms])
+  qed auto
+  with absolutely_integrable_restrict_UNIV show ?thesis
+    by blast
+qed
+
+lemma absolutely_integrable_spike_set:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  assumes f: "f absolutely_integrable_on S" and neg: "negligible {x \<in> S - T. f x \<noteq> 0}" "negligible {x \<in> T - S. f x \<noteq> 0}"
+  shows "f absolutely_integrable_on T"
+  using absolutely_integrable_spike_set_eq f neg by blast
+
 lemma lmeasurable_iff_integrable_on: "S \<in> lmeasurable \<longleftrightarrow> (\<lambda>x. 1::real) integrable_on S"
   by (subst absolutely_integrable_on_iff_nonneg[symmetric])
      (simp_all add: lmeasurable_iff_integrable set_integrable_def)
@@ -1010,7 +1049,7 @@
   by (simp add: lmeasurable_iff_has_integral integral_unique)
 
 lemma lmeasure_integral: "S \<in> lmeasurable \<Longrightarrow> measure lebesgue S = integral S (\<lambda>x. 1::real)"
-  by (auto simp add: lmeasure_integral_UNIV indicator_def[abs_def] lmeasurable_iff_integrable_on)
+  by (fastforce simp add: lmeasure_integral_UNIV indicator_def[abs_def] lmeasurable_iff_integrable_on)
 
 lemma
   assumes \<D>: "\<D> division_of S"
diff -r 53323937ee25 -r a8177d098b74 src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Sat Apr 14 09:23:00 2018 +0100
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Sat Apr 14 15:36:49 2018 +0100
@@ -2201,11 +2201,11 @@
         unfolding sum_distrib_left by (metis divide_inverse inverse_eq_divide power_one_over)
       also have "\<dots> < e/2 * 2"
       proof (rule mult_strict_left_mono)
-        have "sum ((^) (1/2)) {..N + 1} = sum ((^) (1/2::real)) {..<N + 2}"
+        have "sum (power (1/2)) {..N + 1} = sum (power (1/2::real)) {..<N + 2}"
           using lessThan_Suc_atMost by auto
         also have "... < 2"
           by (auto simp: geometric_sum)
-        finally show "sum ((^) (1/2::real)) {..N + 1} < 2" .
+        finally show "sum (power (1/2::real)) {..N + 1} < 2" .
       qed (use \<open>0 < e\<close> in auto)
       finally  show ?thesis by auto
     qed
@@ -2236,6 +2236,12 @@
     by (rule_tac f="?f" in has_integral_eq) auto
 qed
 
+lemma
+  assumes "negligible S"
+  shows integrable_negligible: "f integrable_on S" and integral_negligible: "integral S f = 0"
+  using has_integral_negligible [OF assms]
+  by (auto simp: has_integral_iff)
+
 lemma has_integral_spike:
   fixes f :: "'b::euclidean_space \<Rightarrow> 'a::real_normed_vector"
   assumes "negligible S"
@@ -2271,10 +2277,8 @@
     by metis
 
 lemma integrable_spike:
-  assumes "negligible S"
-    and "\<And>x. x \<in> T - S \<Longrightarrow> g x = f x"
-    and "f integrable_on T"
-  shows "g integrable_on T"
+  assumes "f integrable_on T" "negligible S" "\<And>x. x \<in> T - S \<Longrightarrow> g x = f x"
+    shows "g integrable_on T"
   using assms unfolding integrable_on_def by (blast intro: has_integral_spike)
 
 lemma integral_spike:
@@ -2335,6 +2339,10 @@
 lemma negligible_empty[iff]: "negligible {}"
   using negligible_insert by blast
 
+text\<open>Useful in this form for backchaining\<close>
+lemma empty_imp_negligible: "S = {} \<Longrightarrow> negligible S"
+  by simp
+
 lemma negligible_finite[intro]:
   assumes "finite s"
   shows "negligible s"
@@ -2495,7 +2503,7 @@
         show "?g integrable_on cbox a b"
         proof -
           have "?g integrable_on cbox a b \<inter> {x. x \<bullet> k \<le> c}" "?g integrable_on cbox a b \<inter> {x. x \<bullet> k \<ge> c}"
-            by(rule integrable_spike[OF negligible_standard_hyperplane[of k c]], use k g1 g2 in auto)+
+            by(rule integrable_spike[OF _ negligible_standard_hyperplane[of k c]], use k g1 g2 in auto)+
           with has_integral_split[OF _ _ k] show ?thesis
             unfolding integrable_on_def by blast
         qed
@@ -4664,13 +4672,10 @@
   unfolding integrable_on_def
   by (auto intro:has_integral_on_superset)
 
-lemma integral_restrict_UNIV [intro]:
+lemma integral_restrict_UNIV:
   fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
-  shows "f integrable_on S \<Longrightarrow> integral UNIV (\<lambda>x. if x \<in> S then f x else 0) = integral S f"
-  apply (rule integral_unique)
-  unfolding has_integral_restrict_UNIV
-  apply auto
-  done
+  shows "integral UNIV (\<lambda>x. if x \<in> S then f x else 0) = integral S f"
+  by (simp add: integral_restrict_Int)
 
 lemma integrable_restrict_UNIV:
   fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
@@ -4776,24 +4781,31 @@
 
 lemma has_integral_spike_set_eq:
   fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
-  assumes "negligible ((S - T) \<union> (T - S))"
+  assumes "negligible {x \<in> S - T. f x \<noteq> 0}" "negligible {x \<in> T - S. f x \<noteq> 0}"
   shows "(f has_integral y) S \<longleftrightarrow> (f has_integral y) T"
-  unfolding has_integral_restrict_UNIV[symmetric,of f]
-  apply (rule has_integral_spike_eq[OF assms])
-  by (auto split: if_split_asm)
-
-lemma has_integral_spike_set:
+proof -
+  have "((\<lambda>x. if x \<in> S then f x else 0) has_integral y) UNIV =
+        ((\<lambda>x. if x \<in> T then f x else 0) has_integral y) UNIV"
+  proof (rule has_integral_spike_eq)
+    show "negligible ({x \<in> S - T. f x \<noteq> 0} \<union> {x \<in> T - S. f x \<noteq> 0})"
+      by (rule negligible_Un [OF assms])
+  qed auto
+  then show ?thesis
+    by (simp add: has_integral_restrict_UNIV)
+qed
+
+corollary integral_spike_set:
   fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
-  assumes "(f has_integral y) S" "negligible ((S - T) \<union> (T - S))"
-  shows "(f has_integral y) T"
-  using assms has_integral_spike_set_eq
-  by auto
+  assumes "negligible {x \<in> S - T. f x \<noteq> 0}" "negligible {x \<in> T - S. f x \<noteq> 0}"
+  shows "integral S f = integral T f"
+  using has_integral_spike_set_eq [OF assms]
+  by (metis eq_integralD integral_unique)
 
 lemma integrable_spike_set:
   fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
-  assumes "f integrable_on S" and "negligible ((S - T) \<union> (T - S))"
-    shows "f integrable_on T"
-  using assms by (simp add: integrable_on_def has_integral_spike_set_eq)
+  assumes f: "f integrable_on S" and neg: "negligible {x \<in> S - T. f x \<noteq> 0}" "negligible {x \<in> T - S. f x \<noteq> 0}"
+  shows "f integrable_on T"
+  using has_integral_spike_set_eq [OF neg] f by blast
 
 lemma integrable_spike_set_eq:
   fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
@@ -4808,15 +4820,13 @@
 lemma has_integral_interior:
   fixes f :: "'a :: euclidean_space \<Rightarrow> 'b :: banach"
   shows "negligible(frontier S) \<Longrightarrow> (f has_integral y) (interior S) \<longleftrightarrow> (f has_integral y) S"
-  apply (rule has_integral_spike_set_eq)
-  apply (auto simp: frontier_def Un_Diff closure_def)
-  apply (metis Diff_eq_empty_iff interior_subset negligible_empty)
-  done
+  by (rule has_integral_spike_set_eq [OF empty_imp_negligible negligible_subset])
+     (use interior_subset in \<open>auto simp: frontier_def closure_def\<close>)
 
 lemma has_integral_closure:
   fixes f :: "'a :: euclidean_space \<Rightarrow> 'b :: banach"
   shows "negligible(frontier S) \<Longrightarrow> (f has_integral y) (closure S) \<longleftrightarrow> (f has_integral y) S"
-  by (rule has_integral_spike_set_eq) (simp add: Un_Diff closure_Un_frontier negligible_diff)
+  by (rule has_integral_spike_set_eq [OF negligible_subset empty_imp_negligible]) (auto simp: closure_Un_frontier )
 
 lemma has_integral_open_interval:
   fixes f :: "'a :: euclidean_space \<Rightarrow> 'b :: banach"
diff -r 53323937ee25 -r a8177d098b74 src/HOL/Analysis/Improper_Integral.thy
--- a/src/HOL/Analysis/Improper_Integral.thy	Sat Apr 14 09:23:00 2018 +0100
+++ b/src/HOL/Analysis/Improper_Integral.thy	Sat Apr 14 15:36:49 2018 +0100
@@ -1293,7 +1293,7 @@
       have "negligible S"
         unfolding S_def by force
       then have int_f': "(\<lambda>x. if x \<in> S then 0 else f x) integrable_on cbox a b"
-        by (rule integrable_spike) (auto intro: assms)
+        by (force intro: integrable_spike assms)
       have get_n: "\<exists>n. \<forall>m\<ge>n. x \<in> cbox (u m) (v m) \<longleftrightarrow> x \<in> cbox c d" if x: "x \<notin> S" for x
       proof -
         define \<epsilon> where "\<epsilon> \<equiv> Min ((\<lambda>i. min \<bar>x \<bullet> i - c \<bullet> i\<bar> \<bar>x \<bullet> i - d \<bullet> i\<bar>) ` Basis)"