--- 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"
--- 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"
--- 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)"