--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Mon Apr 09 17:21:10 2018 +0100
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Wed Apr 11 16:34:44 2018 +0100
@@ -839,13 +839,15 @@
lemma set_integral_reflect:
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))"
+ unfolding set_lebesgue_integral_def
by (subst lborel_integral_real_affine[where c="-1" and t=0])
(auto intro!: Bochner_Integration.integral_cong split: split_indicator)
lemma borel_integrable_atLeastAtMost':
fixes f :: "real \<Rightarrow> 'a::{banach, second_countable_topology}"
assumes f: "continuous_on {a..b} f"
- shows "set_integrable lborel {a..b} f" (is "integrable _ ?f")
+ shows "set_integrable lborel {a..b} f"
+ unfolding set_integrable_def
by (intro borel_integrable_compact compact_Icc f)
lemma integral_FTC_atLeastAtMost:
@@ -857,7 +859,8 @@
proof -
let ?f = "\<lambda>x. indicator {a .. b} x *\<^sub>R f x"
have "(?f has_integral (\<integral>x. ?f x \<partial>lborel)) UNIV"
- using borel_integrable_atLeastAtMost'[OF f] by (rule has_integral_integral_lborel)
+ using borel_integrable_atLeastAtMost'[OF f]
+ unfolding set_integrable_def by (rule has_integral_integral_lborel)
moreover
have "(f has_integral F b - F a) {a .. b}"
by (intro fundamental_theorem_of_calculus ballI assms) auto
@@ -876,7 +879,8 @@
proof -
let ?f = "\<lambda>x. indicator S x *\<^sub>R f x"
have "(?f has_integral LINT x : S | lborel. f x) UNIV"
- by (rule has_integral_integral_lborel) fact
+ using assms has_integral_integral_lborel
+ unfolding set_integrable_def set_lebesgue_integral_def by blast
hence 1: "(f has_integral (set_lebesgue_integral lborel S f)) S"
apply (subst has_integral_restrict_UNIV [symmetric])
apply (rule has_integral_eq)
@@ -893,8 +897,8 @@
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes f: "set_integrable lebesgue S f"
shows "(f has_integral (LINT x:S|lebesgue. f x)) S"
- using has_integral_integral_lebesgue[OF f]
- by (simp_all add: indicator_def if_distrib[of "\<lambda>x. x *\<^sub>R f _"] has_integral_restrict_UNIV cong: if_cong)
+ using has_integral_integral_lebesgue f
+ by (fastforce simp add: set_integrable_def set_lebesgue_integral_def indicator_def if_distrib[of "\<lambda>x. x *\<^sub>R f _"] cong: if_cong)
lemma set_lebesgue_integral_eq_integral:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
@@ -915,26 +919,26 @@
lemma absolutely_integrable_on_def:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
- shows "f absolutely_integrable_on s \<longleftrightarrow> f integrable_on s \<and> (\<lambda>x. norm (f x)) integrable_on s"
+ shows "f absolutely_integrable_on S \<longleftrightarrow> f integrable_on S \<and> (\<lambda>x. norm (f x)) integrable_on S"
proof safe
- assume f: "f absolutely_integrable_on s"
- then have nf: "integrable lebesgue (\<lambda>x. norm (indicator s x *\<^sub>R f x))"
- by (intro integrable_norm)
- note integrable_on_lebesgue[OF f] integrable_on_lebesgue[OF nf]
- moreover have
- "(\<lambda>x. indicator s x *\<^sub>R f x) = (\<lambda>x. if x \<in> s then f x else 0)"
- "(\<lambda>x. norm (indicator s x *\<^sub>R f x)) = (\<lambda>x. if x \<in> s then norm (f x) else 0)"
+ assume f: "f absolutely_integrable_on S"
+ then have nf: "integrable lebesgue (\<lambda>x. norm (indicator S x *\<^sub>R f x))"
+ using integrable_norm set_integrable_def by blast
+ show "f integrable_on S"
+ by (rule set_lebesgue_integral_eq_integral[OF f])
+ have "(\<lambda>x. norm (indicator S x *\<^sub>R f x)) = (\<lambda>x. if x \<in> S then norm (f x) else 0)"
by auto
- ultimately show "f integrable_on s" "(\<lambda>x. norm (f x)) integrable_on s"
- by (simp_all add: integrable_restrict_UNIV)
+ with integrable_on_lebesgue[OF nf] show "(\<lambda>x. norm (f x)) integrable_on S"
+ by (simp add: integrable_restrict_UNIV)
next
- assume f: "f integrable_on s" and nf: "(\<lambda>x. norm (f x)) integrable_on s"
- show "f absolutely_integrable_on s"
+ assume f: "f integrable_on S" and nf: "(\<lambda>x. norm (f x)) integrable_on S"
+ show "f absolutely_integrable_on S"
+ unfolding set_integrable_def
proof (rule integrableI_bounded)
- show "(\<lambda>x. indicator s x *\<^sub>R f x) \<in> borel_measurable lebesgue"
- using f has_integral_implies_lebesgue_measurable[of f _ s] by (auto simp: integrable_on_def)
- show "(\<integral>\<^sup>+ x. ennreal (norm (indicator s x *\<^sub>R f x)) \<partial>lebesgue) < \<infinity>"
- using nf nn_integral_has_integral_lebesgue[of "\<lambda>x. norm (f x)" _ s]
+ show "(\<lambda>x. indicator S x *\<^sub>R f x) \<in> borel_measurable lebesgue"
+ using f has_integral_implies_lebesgue_measurable[of f _ S] by (auto simp: integrable_on_def)
+ show "(\<integral>\<^sup>+ x. ennreal (norm (indicator S x *\<^sub>R f x)) \<partial>lebesgue) < \<infinity>"
+ using nf nn_integral_has_integral_lebesgue[of "\<lambda>x. norm (f x)" _ S]
by (auto simp: integrable_on_def nn_integral_completion)
qed
qed
@@ -951,12 +955,13 @@
by (auto simp: integrable_on_open_interval absolutely_integrable_on_def)
lemma absolutely_integrable_restrict_UNIV:
- "(\<lambda>x. if x \<in> s then f x else 0) absolutely_integrable_on UNIV \<longleftrightarrow> f absolutely_integrable_on s"
+ "(\<lambda>x. if x \<in> S then f x else 0) absolutely_integrable_on UNIV \<longleftrightarrow> f absolutely_integrable_on S"
+ unfolding set_integrable_def
by (intro arg_cong2[where f=integrable]) auto
lemma absolutely_integrable_onI:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
- shows "f integrable_on s \<Longrightarrow> (\<lambda>x. norm (f x)) integrable_on s \<Longrightarrow> f absolutely_integrable_on s"
+ shows "f integrable_on S \<Longrightarrow> (\<lambda>x. norm (f x)) integrable_on S \<Longrightarrow> f absolutely_integrable_on S"
unfolding absolutely_integrable_on_def by auto
lemma nonnegative_absolutely_integrable_1:
@@ -984,7 +989,7 @@
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)
+ (simp_all add: lmeasurable_iff_integrable set_integrable_def)
lemma lmeasure_integral_UNIV: "S \<in> lmeasurable \<Longrightarrow> measure lebesgue S = integral UNIV (indicator S)"
by (simp add: lmeasurable_iff_has_integral integral_unique)
@@ -1532,7 +1537,8 @@
lemma set_integral_norm_bound:
fixes f :: "_ \<Rightarrow> 'a :: {banach, second_countable_topology}"
shows "set_integrable M k f \<Longrightarrow> norm (LINT x:k|M. f x) \<le> LINT x:k|M. norm (f x)"
- using integral_norm_bound[of M "\<lambda>x. indicator k x *\<^sub>R f x"] by simp
+ using integral_norm_bound[of M "\<lambda>x. indicator k x *\<^sub>R f x"] by (simp add: set_lebesgue_integral_def)
+
lemma set_integral_finite_UN_AE:
fixes f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
@@ -1557,13 +1563,13 @@
with insert.hyps insert.IH[symmetric]
show ?case
by (auto intro!: set_integral_Un_AE sets.finite_UN f set_integrable_UN)
-qed simp
+qed (simp add: set_lebesgue_integral_def)
lemma set_integrable_norm:
fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
assumes f: "set_integrable M k f" shows "set_integrable M k (\<lambda>x. norm (f x))"
- using integrable_norm[OF f] by simp
-
+ using integrable_norm f by (force simp add: set_integrable_def)
+
lemma absolutely_integrable_bounded_variation:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes f: "f absolutely_integrable_on UNIV"
@@ -2120,30 +2126,36 @@
and h :: "'n::euclidean_space \<Rightarrow> 'p::euclidean_space"
shows "f absolutely_integrable_on s \<Longrightarrow> bounded_linear h \<Longrightarrow> (h \<circ> f) absolutely_integrable_on s"
using integrable_bounded_linear[of h lebesgue "\<lambda>x. indicator s x *\<^sub>R f x"]
- by (simp add: linear_simps[of h])
+ by (simp add: linear_simps[of h] set_integrable_def)
+
+lemma absolutely_integrable_zero [simp]: "(\<lambda>x. 0) absolutely_integrable_on S"
+ by (simp add: set_integrable_def)
lemma absolutely_integrable_sum:
fixes f :: "'a \<Rightarrow> 'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
- assumes "finite t" and "\<And>a. a \<in> t \<Longrightarrow> (f a) absolutely_integrable_on s"
- shows "(\<lambda>x. sum (\<lambda>a. f a x) t) absolutely_integrable_on s"
- using assms(1,2) by induct auto
+ assumes "finite T" and "\<And>a. a \<in> T \<Longrightarrow> (f a) absolutely_integrable_on S"
+ shows "(\<lambda>x. sum (\<lambda>a. f a x) T) absolutely_integrable_on S"
+ using assms by induction auto
lemma absolutely_integrable_integrable_bound:
fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
- assumes le: "\<forall>x\<in>s. norm (f x) \<le> g x" and f: "f integrable_on s" and g: "g integrable_on s"
- shows "f absolutely_integrable_on s"
+ assumes le: "\<And>x. x\<in>S \<Longrightarrow> norm (f x) \<le> g x" and f: "f integrable_on S" and g: "g integrable_on S"
+ shows "f absolutely_integrable_on S"
+ unfolding set_integrable_def
proof (rule Bochner_Integration.integrable_bound)
- show "g absolutely_integrable_on s"
+ have "g absolutely_integrable_on S"
unfolding absolutely_integrable_on_def
proof
- show "(\<lambda>x. norm (g x)) integrable_on s"
+ show "(\<lambda>x. norm (g x)) integrable_on S"
using le norm_ge_zero[of "f _"]
by (intro integrable_spike_finite[OF _ _ g, of "{}"])
(auto intro!: abs_of_nonneg intro: order_trans simp del: norm_ge_zero)
qed fact
- show "set_borel_measurable lebesgue s f"
+ then show "integrable lebesgue (\<lambda>x. indicat_real S x *\<^sub>R g x)"
+ by (simp add: set_integrable_def)
+ show "(\<lambda>x. indicat_real S x *\<^sub>R f x) \<in> borel_measurable lebesgue"
using f by (auto intro: has_integral_implies_lebesgue_measurable simp: integrable_on_def)
-qed (use le in \<open>auto intro!: always_eventually split: split_indicator\<close>)
+qed (use le in \<open>force intro!: always_eventually split: split_indicator\<close>)
subsection \<open>Componentwise\<close>
@@ -2175,7 +2187,7 @@
lemma absolutely_integrable_componentwise:
shows "(\<And>b. b \<in> Basis \<Longrightarrow> (\<lambda>x. f x \<bullet> b) absolutely_integrable_on A) \<Longrightarrow> f absolutely_integrable_on A"
- by (simp add: absolutely_integrable_componentwise_iff)
+ using absolutely_integrable_componentwise_iff by blast
lemma absolutely_integrable_component:
"f absolutely_integrable_on A \<Longrightarrow> (\<lambda>x. f x \<bullet> (b :: 'b :: euclidean_space)) absolutely_integrable_on A"
@@ -2190,7 +2202,8 @@
have "(\<lambda>x. c *\<^sub>R x) o f absolutely_integrable_on S"
apply (rule absolutely_integrable_linear [OF assms])
by (simp add: bounded_linear_scaleR_right)
- then show ?thesis by simp
+ then show ?thesis
+ using assms by blast
qed
lemma absolutely_integrable_scaleR_right:
@@ -2202,7 +2215,7 @@
fixes f :: "'a :: euclidean_space \<Rightarrow> 'b :: euclidean_space"
assumes "f absolutely_integrable_on S"
shows "(norm o f) absolutely_integrable_on S"
- using assms unfolding absolutely_integrable_on_def by auto
+ using assms by (simp add: absolutely_integrable_on_def o_def)
lemma absolutely_integrable_abs:
fixes f :: "'a :: euclidean_space \<Rightarrow> 'b :: euclidean_space"
@@ -2405,56 +2418,60 @@
lemma dominated_convergence:
fixes f :: "nat \<Rightarrow> 'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
- assumes f: "\<And>k. (f k) integrable_on s" and h: "h integrable_on s"
- and le: "\<And>k. \<forall>x \<in> s. norm (f k x) \<le> h x"
- and conv: "\<forall>x \<in> s. (\<lambda>k. f k x) \<longlonglongrightarrow> g x"
- shows "g integrable_on s" "(\<lambda>k. integral s (f k)) \<longlonglongrightarrow> integral s g"
+ assumes f: "\<And>k. (f k) integrable_on S" and h: "h integrable_on S"
+ and le: "\<And>k x. x \<in> S \<Longrightarrow> norm (f k x) \<le> h x"
+ and conv: "\<forall>x \<in> S. (\<lambda>k. f k x) \<longlonglongrightarrow> g x"
+ shows "g integrable_on S" "(\<lambda>k. integral S (f k)) \<longlonglongrightarrow> integral S g"
proof -
- have 3: "h absolutely_integrable_on s"
+ have 3: "h absolutely_integrable_on S"
unfolding absolutely_integrable_on_def
proof
- show "(\<lambda>x. norm (h x)) integrable_on s"
+ show "(\<lambda>x. norm (h x)) integrable_on S"
proof (intro integrable_spike_finite[OF _ _ h, of "{}"] ballI)
- fix x assume "x \<in> s - {}" then show "norm (h x) = h x"
+ fix x assume "x \<in> S - {}" then show "norm (h x) = h x"
by (metis Diff_empty abs_of_nonneg bot_set_def le norm_ge_zero order_trans real_norm_def)
qed auto
qed fact
- have 2: "set_borel_measurable lebesgue s (f k)" for k
+ have 2: "set_borel_measurable lebesgue S (f k)" for k
+ unfolding set_borel_measurable_def
using f by (auto intro: has_integral_implies_lebesgue_measurable simp: integrable_on_def)
- then have 1: "set_borel_measurable lebesgue s g"
+ then have 1: "set_borel_measurable lebesgue S g"
+ unfolding set_borel_measurable_def
by (rule borel_measurable_LIMSEQ_metric) (use conv in \<open>auto split: split_indicator\<close>)
- have 4: "AE x in lebesgue. (\<lambda>i. indicator s x *\<^sub>R f i x) \<longlonglongrightarrow> indicator s x *\<^sub>R g x"
- "AE x in lebesgue. norm (indicator s x *\<^sub>R f k x) \<le> indicator s x *\<^sub>R h x" for k
+ have 4: "AE x in lebesgue. (\<lambda>i. indicator S x *\<^sub>R f i x) \<longlonglongrightarrow> indicator S x *\<^sub>R g x"
+ "AE x in lebesgue. norm (indicator S x *\<^sub>R f k x) \<le> indicator S x *\<^sub>R h x" for k
using conv le by (auto intro!: always_eventually split: split_indicator)
-
- have g: "g absolutely_integrable_on s"
- using 1 2 3 4 by (rule integrable_dominated_convergence)
- then show "g integrable_on s"
+ have g: "g absolutely_integrable_on S"
+ using 1 2 3 4 unfolding set_borel_measurable_def set_integrable_def
+ by (rule integrable_dominated_convergence)
+ then show "g integrable_on S"
by (auto simp: absolutely_integrable_on_def)
- have "(\<lambda>k. (LINT x:s|lebesgue. f k x)) \<longlonglongrightarrow> (LINT x:s|lebesgue. g x)"
- using 1 2 3 4 by (rule integral_dominated_convergence)
- then show "(\<lambda>k. integral s (f k)) \<longlonglongrightarrow> integral s g"
+ have "(\<lambda>k. (LINT x:S|lebesgue. f k x)) \<longlonglongrightarrow> (LINT x:S|lebesgue. g x)"
+ unfolding set_borel_measurable_def set_lebesgue_integral_def
+ using 1 2 3 4 unfolding set_borel_measurable_def set_lebesgue_integral_def set_integrable_def
+ by (rule integral_dominated_convergence)
+ then show "(\<lambda>k. integral S (f k)) \<longlonglongrightarrow> integral S g"
using g absolutely_integrable_integrable_bound[OF le f h]
by (subst (asm) (1 2) set_lebesgue_integral_eq_integral) auto
qed
lemma has_integral_dominated_convergence:
fixes f :: "nat \<Rightarrow> 'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
- assumes "\<And>k. (f k has_integral y k) s" "h integrable_on s"
- "\<And>k. \<forall>x\<in>s. norm (f k x) \<le> h x" "\<forall>x\<in>s. (\<lambda>k. f k x) \<longlonglongrightarrow> g x"
+ assumes "\<And>k. (f k has_integral y k) S" "h integrable_on S"
+ "\<And>k. \<forall>x\<in>S. norm (f k x) \<le> h x" "\<forall>x\<in>S. (\<lambda>k. f k x) \<longlonglongrightarrow> g x"
and x: "y \<longlonglongrightarrow> x"
- shows "(g has_integral x) s"
+ shows "(g has_integral x) S"
proof -
- have int_f: "\<And>k. (f k) integrable_on s"
+ have int_f: "\<And>k. (f k) integrable_on S"
using assms by (auto simp: integrable_on_def)
- have "(g has_integral (integral s g)) s"
- by (intro integrable_integral dominated_convergence[OF int_f assms(2)]) fact+
- moreover have "integral s g = x"
+ have "(g has_integral (integral S g)) S"
+ by (metis assms(2-4) dominated_convergence(1) has_integral_integral int_f)
+ moreover have "integral S g = x"
proof (rule LIMSEQ_unique)
- show "(\<lambda>i. integral s (f i)) \<longlonglongrightarrow> x"
+ show "(\<lambda>i. integral S (f i)) \<longlonglongrightarrow> x"
using integral_unique[OF assms(1)] x by simp
- show "(\<lambda>i. integral s (f i)) \<longlonglongrightarrow> integral s g"
- by (intro dominated_convergence[OF int_f assms(2)]) fact+
+ show "(\<lambda>i. integral S (f i)) \<longlonglongrightarrow> integral S g"
+ by (metis assms(2) assms(3) assms(4) dominated_convergence(2) int_f)
qed
ultimately show ?thesis
by simp
@@ -2720,7 +2737,11 @@
then have "integral (closure S) f = set_lebesgue_integral lebesgue (closure S) f"
by (intro set_lebesgue_integral_eq_integral(2)[symmetric])
also have "\<dots> = 0 \<longleftrightarrow> (AE x in lebesgue. indicator (closure S) x *\<^sub>R f x = 0)"
- by (rule integral_nonneg_eq_0_iff_AE[OF af]) (use nonneg in \<open>auto simp: indicator_def\<close>)
+ unfolding set_lebesgue_integral_def
+ proof (rule integral_nonneg_eq_0_iff_AE)
+ show "integrable lebesgue (\<lambda>x. indicat_real (closure S) x *\<^sub>R f x)"
+ by (metis af set_integrable_def)
+ qed (use nonneg in \<open>auto simp: indicator_def\<close>)
also have "\<dots> \<longleftrightarrow> (AE x in lebesgue. x \<in> {x. x \<in> closure S \<longrightarrow> f x = 0})"
by (auto simp: indicator_def)
finally have "(AE x in lebesgue. x \<in> {x. x \<in> closure S \<longrightarrow> f x = 0})" by simp
--- a/src/HOL/Analysis/Infinite_Set_Sum.thy Mon Apr 09 17:21:10 2018 +0100
+++ b/src/HOL/Analysis/Infinite_Set_Sum.thy Wed Apr 11 16:34:44 2018 +0100
@@ -142,8 +142,6 @@
\<close>
-
-
lemma restrict_count_space_subset:
"A \<subseteq> B \<Longrightarrow> restrict_space (count_space B) A = count_space A"
by (subst restrict_count_space) (simp_all add: Int_absorb2)
@@ -156,17 +154,19 @@
have "count_space A = restrict_space (count_space B) A"
by (rule restrict_count_space_subset [symmetric]) fact+
also have "integrable \<dots> f \<longleftrightarrow> set_integrable (count_space B) A f"
- by (subst integrable_restrict_space) auto
+ by (simp add: integrable_restrict_space set_integrable_def)
finally show ?thesis
- unfolding abs_summable_on_def .
+ unfolding abs_summable_on_def set_integrable_def .
qed
lemma abs_summable_on_altdef: "f abs_summable_on A \<longleftrightarrow> set_integrable (count_space UNIV) A f"
- by (subst abs_summable_on_restrict[of _ UNIV]) (auto simp: abs_summable_on_def)
+ unfolding abs_summable_on_def set_integrable_def
+ by (metis (no_types) inf_top.right_neutral integrable_restrict_space restrict_count_space sets_UNIV)
lemma abs_summable_on_altdef':
"A \<subseteq> B \<Longrightarrow> f abs_summable_on A \<longleftrightarrow> set_integrable (count_space B) A f"
- by (subst abs_summable_on_restrict[of _ B]) (auto simp: abs_summable_on_def)
+ unfolding abs_summable_on_def set_integrable_def
+ by (metis (no_types) Pow_iff abs_summable_on_def inf.orderE integrable_restrict_space restrict_count_space_subset set_integrable_def sets_count_space space_count_space)
lemma abs_summable_on_norm_iff [simp]:
"(\<lambda>x. norm (f x)) abs_summable_on A \<longleftrightarrow> f abs_summable_on A"
@@ -205,7 +205,7 @@
assumes "\<And>x. x \<in> B - A \<Longrightarrow> g x = 0"
assumes "\<And>x. x \<in> A \<inter> B \<Longrightarrow> f x = g x"
shows "f abs_summable_on A \<longleftrightarrow> g abs_summable_on B"
- unfolding abs_summable_on_altdef using assms
+ unfolding abs_summable_on_altdef set_integrable_def using assms
by (intro Bochner_Integration.integrable_cong refl)
(auto simp: indicator_def split: if_splits)
@@ -418,11 +418,13 @@
lemma infsetsum_altdef:
"infsetsum f A = set_lebesgue_integral (count_space UNIV) A f"
+ unfolding set_lebesgue_integral_def
by (subst integral_restrict_space [symmetric])
(auto simp: restrict_count_space_subset infsetsum_def)
lemma infsetsum_altdef':
"A \<subseteq> B \<Longrightarrow> infsetsum f A = set_lebesgue_integral (count_space B) A f"
+ unfolding set_lebesgue_integral_def
by (subst integral_restrict_space [symmetric])
(auto simp: restrict_count_space_subset infsetsum_def)
@@ -477,7 +479,8 @@
shows "infsetsum f A = (\<Sum>n. if n \<in> A then f n else 0)"
proof -
from assms have "infsetsum f A = (\<Sum>n. indicator A n *\<^sub>R f n)"
- unfolding infsetsum_altdef abs_summable_on_altdef by (subst integral_count_space_nat) auto
+ unfolding infsetsum_altdef abs_summable_on_altdef set_lebesgue_integral_def set_integrable_def
+ by (subst integral_count_space_nat) auto
also have "(\<lambda>n. indicator A n *\<^sub>R f n) = (\<lambda>n. if n \<in> A then f n else 0)"
by auto
finally show ?thesis .
@@ -560,7 +563,7 @@
assumes "\<And>x. x \<in> B - A \<Longrightarrow> g x = 0"
assumes "\<And>x. x \<in> A \<inter> B \<Longrightarrow> f x = g x"
shows "infsetsum f A = infsetsum g B"
- unfolding infsetsum_altdef using assms
+ unfolding infsetsum_altdef set_lebesgue_integral_def using assms
by (intro Bochner_Integration.integral_cong refl)
(auto simp: indicator_def split: if_splits)
@@ -571,7 +574,7 @@
assumes "\<And>x. x \<in> A - B \<Longrightarrow> f x \<le> 0"
assumes "\<And>x. x \<in> B - A \<Longrightarrow> g x \<ge> 0"
shows "infsetsum f A \<le> infsetsum g B"
- using assms unfolding infsetsum_altdef abs_summable_on_altdef
+ using assms unfolding infsetsum_altdef set_lebesgue_integral_def abs_summable_on_altdef set_integrable_def
by (intro Bochner_Integration.integral_mono) (auto simp: indicator_def)
lemma infsetsum_mono_neutral_left:
@@ -617,7 +620,8 @@
by (intro pair_sigma_finite.intro sigma_finite_measure_count_space_countable) fact+
have "integrable (count_space (A \<times> B')) (\<lambda>z. indicator (Sigma A B) z *\<^sub>R f z)"
- using summable by (subst abs_summable_on_altdef' [symmetric]) (auto simp: B'_def)
+ using summable
+ by (metis (mono_tags, lifting) abs_summable_on_altdef abs_summable_on_def integrable_cong integrable_mult_indicator set_integrable_def sets_UNIV)
also have "?this \<longleftrightarrow> integrable (count_space A \<Otimes>\<^sub>M count_space B') (\<lambda>(x, y). indicator (B x) y *\<^sub>R f (x, y))"
by (intro Bochner_Integration.integrable_cong)
(auto simp: pair_measure_countable indicator_def split: if_splits)
@@ -627,14 +631,20 @@
(\<integral>x. infsetsum (\<lambda>y. f (x, y)) (B x) \<partial>count_space A)"
unfolding infsetsum_def by simp
also have "\<dots> = (\<integral>x. \<integral>y. indicator (B x) y *\<^sub>R f (x, y) \<partial>count_space B' \<partial>count_space A)"
- by (intro Bochner_Integration.integral_cong infsetsum_altdef'[of _ B'] refl)
- (auto simp: B'_def)
+ proof (rule Bochner_Integration.integral_cong [OF refl])
+ show "\<And>x. x \<in> space (count_space A) \<Longrightarrow>
+ (\<Sum>\<^sub>ay\<in>B x. f (x, y)) = LINT y|count_space B'. indicat_real (B x) y *\<^sub>R f (x, y)"
+ using infsetsum_altdef'[of _ B']
+ unfolding set_lebesgue_integral_def B'_def
+ by auto
+ qed
also have "\<dots> = (\<integral>(x,y). indicator (B x) y *\<^sub>R f (x, y) \<partial>(count_space A \<Otimes>\<^sub>M count_space B'))"
by (subst integral_fst [OF integrable]) auto
also have "\<dots> = (\<integral>z. indicator (Sigma A B) z *\<^sub>R f z \<partial>count_space (A \<times> B'))"
by (intro Bochner_Integration.integral_cong)
(auto simp: pair_measure_countable indicator_def split: if_splits)
also have "\<dots> = infsetsum f (Sigma A B)"
+ unfolding set_lebesgue_integral_def [symmetric]
by (rule infsetsum_altdef' [symmetric]) (auto simp: B'_def)
finally show ?thesis ..
qed
@@ -693,7 +703,6 @@
unfolding B'_def using assms by auto
interpret pair_sigma_finite "count_space A" "count_space B'"
by (intro pair_sigma_finite.intro sigma_finite_measure_count_space_countable) fact+
-
{
assume *: "f abs_summable_on Sigma A B"
thus "(\<lambda>y. f (x, y)) abs_summable_on B x" if "x \<in> A" for x
@@ -707,18 +716,18 @@
finally have "integrable (count_space A)
(\<lambda>x. lebesgue_integral (count_space B')
(\<lambda>y. indicator (Sigma A B) (x, y) *\<^sub>R norm (f (x, y))))"
- by (rule integrable_fst')
+ unfolding set_integrable_def by (rule integrable_fst')
also have "?this \<longleftrightarrow> integrable (count_space A)
(\<lambda>x. lebesgue_integral (count_space B')
(\<lambda>y. indicator (B x) y *\<^sub>R norm (f (x, y))))"
by (intro integrable_cong refl) (simp_all add: indicator_def)
also have "\<dots> \<longleftrightarrow> integrable (count_space A) (\<lambda>x. infsetsum (\<lambda>y. norm (f (x, y))) (B x))"
+ unfolding set_lebesgue_integral_def [symmetric]
by (intro integrable_cong refl infsetsum_altdef' [symmetric]) (auto simp: B'_def)
also have "\<dots> \<longleftrightarrow> (\<lambda>x. infsetsum (\<lambda>y. norm (f (x, y))) (B x)) abs_summable_on A"
by (simp add: abs_summable_on_def)
finally show \<dots> .
}
-
{
assume *: "\<forall>x\<in>A. (\<lambda>y. f (x, y)) abs_summable_on B x"
assume "(\<lambda>x. \<Sum>\<^sub>ay\<in>B x. norm (f (x, y))) abs_summable_on A"
@@ -726,6 +735,7 @@
by (intro abs_summable_on_cong refl infsetsum_altdef') (auto simp: B'_def)
also have "\<dots> \<longleftrightarrow> (\<lambda>x. \<integral>y. indicator (Sigma A B) (x, y) *\<^sub>R norm (f (x, y)) \<partial>count_space B')
abs_summable_on A" (is "_ \<longleftrightarrow> ?h abs_summable_on _")
+ unfolding set_lebesgue_integral_def
by (intro abs_summable_on_cong) (auto simp: indicator_def)
also have "\<dots> \<longleftrightarrow> integrable (count_space A) ?h"
by (simp add: abs_summable_on_def)
@@ -740,7 +750,8 @@
by blast
also have "?this \<longleftrightarrow> integrable (count_space B')
(\<lambda>y. indicator (B x) y *\<^sub>R f (x, y))"
- using x by (intro abs_summable_on_altdef') (auto simp: B'_def)
+ unfolding set_integrable_def [symmetric]
+ using x by (intro abs_summable_on_altdef') (auto simp: B'_def)
also have "(\<lambda>y. indicator (B x) y *\<^sub>R f (x, y)) =
(\<lambda>y. indicator (Sigma A B) (x, y) *\<^sub>R f (x, y))"
using x by (auto simp: indicator_def)
@@ -749,12 +760,13 @@
}
thus ?case by (auto simp: AE_count_space)
qed (insert **, auto simp: pair_measure_countable)
- also have "count_space A \<Otimes>\<^sub>M count_space B' = count_space (A \<times> B')"
+ moreover have "count_space A \<Otimes>\<^sub>M count_space B' = count_space (A \<times> B')"
by (simp add: pair_measure_countable)
- also have "set_integrable (count_space (A \<times> B')) (Sigma A B) f \<longleftrightarrow>
+ moreover have "set_integrable (count_space (A \<times> B')) (Sigma A B) f \<longleftrightarrow>
f abs_summable_on Sigma A B"
by (rule abs_summable_on_altdef' [symmetric]) (auto simp: B'_def)
- finally show \<dots> .
+ ultimately show "f abs_summable_on Sigma A B"
+ by (simp add: set_integrable_def)
}
qed
--- a/src/HOL/Analysis/Interval_Integral.thy Mon Apr 09 17:21:10 2018 +0100
+++ b/src/HOL/Analysis/Interval_Integral.thy Wed Apr 11 16:34:44 2018 +0100
@@ -51,9 +51,7 @@
lemma borel_einterval[measurable]: "einterval a b \<in> sets borel"
unfolding einterval_def by measurable
-(*
- Approximating a (possibly infinite) interval
-*)
+subsection\<open>Approximating a (possibly infinite) interval\<close>
lemma filterlim_sup1: "(LIM x F. f x :> G1) \<Longrightarrow> (LIM x F. f x :> (sup G1 G2))"
unfolding filterlim_def by (auto intro: le_supI1)
@@ -175,9 +173,7 @@
translations
"LBINT x=a..b. f" == "CONST interval_lebesgue_integral CONST lborel a b (\<lambda>x. f)"
-(*
- Basic properties of integration over an interval.
-*)
+subsection\<open>Basic properties of integration over an interval\<close>
lemma interval_lebesgue_integral_cong:
"a \<le> b \<Longrightarrow> (\<And>x. x \<in> einterval a b \<Longrightarrow> f x = g x) \<Longrightarrow> einterval a b \<in> sets M \<Longrightarrow>
@@ -200,7 +196,7 @@
show ?thesis
unfolding interval_lebesgue_integrable_def
using lborel_integrable_real_affine_iff[symmetric, of "-1" "\<lambda>x. indicator (einterval _ _) x *\<^sub>R f x" 0]
- by (simp add: *)
+ by (simp add: * set_integrable_def)
qed
lemma interval_lebesgue_integral_add [intro, simp]:
@@ -260,7 +256,7 @@
lemma interval_lebesgue_integral_uminus:
"interval_lebesgue_integral M a b (\<lambda>x. - f x) = - interval_lebesgue_integral M a b f"
- by (auto simp add: interval_lebesgue_integral_def interval_lebesgue_integrable_def)
+ by (auto simp add: interval_lebesgue_integral_def interval_lebesgue_integrable_def set_lebesgue_integral_def)
lemma interval_lebesgue_integral_of_real:
"interval_lebesgue_integral M a b (\<lambda>x. complex_of_real (f x)) =
@@ -287,10 +283,10 @@
using assms by (auto simp add: interval_lebesgue_integral_def less_imp_le einterval_def)
lemma interval_integral_endpoints_same [simp]: "(LBINT x=a..a. f x) = 0"
- by (simp add: interval_lebesgue_integral_def einterval_same)
+ by (simp add: interval_lebesgue_integral_def set_lebesgue_integral_def einterval_same)
lemma interval_integral_endpoints_reverse: "(LBINT x=a..b. f x) = -(LBINT x=b..a. f x)"
- by (cases a b rule: linorder_cases) (auto simp: interval_lebesgue_integral_def einterval_same)
+ by (cases a b rule: linorder_cases) (auto simp: interval_lebesgue_integral_def set_lebesgue_integral_def einterval_same)
lemma interval_integrable_endpoints_reverse:
"interval_lebesgue_integrable lborel a b f \<longleftrightarrow>
@@ -304,15 +300,16 @@
by (auto simp add: interval_lebesgue_integral_def interval_integrable_endpoints_reverse
split: if_split_asm)
next
- case (le a b) then show ?case
- unfolding interval_lebesgue_integral_def
- by (subst set_integral_reflect)
- (auto simp: interval_lebesgue_integrable_def einterval_iff
- ereal_uminus_le_reorder ereal_uminus_less_reorder not_less
- uminus_ereal.simps[symmetric]
+ case (le a b)
+ have "LBINT x:{x. - x \<in> einterval a b}. f (- x) = LBINT x:einterval (- b) (- a). f (- x)"
+ unfolding interval_lebesgue_integrable_def set_lebesgue_integral_def
+ apply (rule Bochner_Integration.integral_cong [OF refl])
+ by (auto simp: einterval_iff ereal_uminus_le_reorder ereal_uminus_less_reorder not_less uminus_ereal.simps[symmetric]
simp del: uminus_ereal.simps
- intro!: Bochner_Integration.integral_cong
split: split_indicator)
+ then show ?case
+ unfolding interval_lebesgue_integral_def
+ by (subst set_integral_reflect) (simp add: le)
qed
lemma interval_lebesgue_integral_0_infty:
@@ -328,21 +325,19 @@
(set_integrable M {a<..} f)"
unfolding interval_lebesgue_integrable_def by auto
-(*
- Basic properties of integration over an interval wrt lebesgue measure.
-*)
+subsection\<open>Basic properties of integration over an interval wrt lebesgue measure\<close>
lemma interval_integral_zero [simp]:
fixes a b :: ereal
shows"LBINT x=a..b. 0 = 0"
-unfolding interval_lebesgue_integral_def einterval_eq
+unfolding interval_lebesgue_integral_def set_lebesgue_integral_def einterval_eq
by simp
lemma interval_integral_const [intro, simp]:
fixes a b c :: real
shows "interval_lebesgue_integrable lborel a b (\<lambda>x. c)" and "LBINT x=a..b. c = c * (b - a)"
-unfolding interval_lebesgue_integral_def interval_lebesgue_integrable_def einterval_eq
-by (auto simp add: less_imp_le field_simps measure_def)
+ unfolding interval_lebesgue_integral_def interval_lebesgue_integrable_def einterval_eq
+ by (auto simp add: less_imp_le field_simps measure_def set_integrable_def set_lebesgue_integral_def)
lemma interval_integral_cong_AE:
assumes [measurable]: "f \<in> borel_measurable borel" "g \<in> borel_measurable borel"
@@ -429,7 +424,7 @@
and anti_eq: "\<And>x. b \<le> a \<Longrightarrow> b < x \<Longrightarrow> x < a \<Longrightarrow> x \<notin> X \<Longrightarrow> f x = g x"
assumes "\<And>x. x \<in> X \<Longrightarrow> emeasure M {x} = 0" "\<And>x. x \<in> X \<Longrightarrow> {x} \<in> sets M"
shows "interval_lebesgue_integral M a b f = interval_lebesgue_integral M a b g"
- unfolding interval_lebesgue_integral_def
+ unfolding interval_lebesgue_integral_def set_lebesgue_integral_def
apply (intro if_cong refl arg_cong[where f="\<lambda>x. - x"] integral_discrete_difference[of X] assms)
apply (auto simp: eq anti_eq einterval_iff split: split_indicator)
done
@@ -444,13 +439,17 @@
then have ord: "a \<le> b" "b \<le> c" "a \<le> c" and f': "set_integrable lborel (einterval a c) f"
by (auto simp: interval_lebesgue_integrable_def)
then have f: "set_borel_measurable borel (einterval a c) f"
+ unfolding set_integrable_def set_borel_measurable_def
by (drule_tac borel_measurable_integrable) simp
have "(LBINT x:einterval a c. f x) = (LBINT x:einterval a b \<union> einterval b c. f x)"
proof (rule set_integral_cong_set)
show "AE x in lborel. (x \<in> einterval a b \<union> einterval b c) = (x \<in> einterval a c)"
using AE_lborel_singleton[of "real_of_ereal b"] ord
by (cases a b c rule: ereal3_cases) (auto simp: einterval_iff)
- qed (insert ord, auto intro!: set_borel_measurable_subset[OF f] simp: einterval_iff)
+ show "set_borel_measurable lborel (einterval a c) f" "set_borel_measurable lborel (einterval a b \<union> einterval b c) f"
+ unfolding set_borel_measurable_def
+ using ord by (auto simp: einterval_iff intro!: set_borel_measurable_subset[OF f, unfolded set_borel_measurable_def])
+ qed
also have "\<dots> = (LBINT x:einterval a b. f x) + (LBINT x:einterval b c. f x)"
using ord
by (intro set_integral_Un_AE) (auto intro!: set_integrable_subset[OF f'] simp: einterval_iff not_less)
@@ -475,9 +474,10 @@
interval_lebesgue_integrable lborel a b f"
proof (induct a b rule: linorder_wlog)
case (le a b) then show ?case
+ unfolding interval_lebesgue_integrable_def set_integrable_def
by (auto simp: interval_lebesgue_integrable_def
- intro!: set_integrable_subset[OF borel_integrable_compact[of "{a .. b}"]]
- continuous_at_imp_continuous_on)
+ intro!: set_integrable_subset[unfolded set_integrable_def, OF borel_integrable_compact[of "{a .. b}"]]
+ continuous_at_imp_continuous_on)
qed (auto intro: interval_integrable_endpoints_reverse[THEN iffD1])
lemma interval_integrable_continuous_on:
@@ -497,9 +497,8 @@
shows "a \<le> b \<Longrightarrow> set_integrable lborel (einterval a b) f \<Longrightarrow> LBINT x=a..b. f x = integral (einterval a b) f"
by (subst interval_lebesgue_integral_le_eq, simp) (rule set_borel_integral_eq_integral)
-(*
- General limit approximation arguments
-*)
+
+subsection\<open>General limit approximation arguments\<close>
lemma interval_integral_Icc_approx_nonneg:
fixes a b :: ereal
@@ -517,7 +516,7 @@
"set_integrable lborel (einterval a b) f"
"(LBINT x=a..b. f x) = C"
proof -
- have 1: "\<And>i. set_integrable lborel {l i..u i} f" by (rule f_integrable)
+ have 1 [unfolded set_integrable_def]: "\<And>i. set_integrable lborel {l i..u i} f" by (rule f_integrable)
have 2: "AE x in lborel. mono (\<lambda>n. indicator {l n..u n} x *\<^sub>R f x)"
proof -
from f_nonneg have "AE x in lborel. \<forall>i. l i \<le> x \<longrightarrow> x \<le> u i \<longrightarrow> 0 \<le> f x"
@@ -544,14 +543,16 @@
unfolding approx(1) by (auto intro!: AE_I2 Lim_eventually split: split_indicator)
qed
have 4: "(\<lambda>i. \<integral> x. indicator {l i..u i} x *\<^sub>R f x \<partial>lborel) \<longlonglongrightarrow> C"
- using lbint_lim by (simp add: interval_integral_Icc approx less_imp_le)
- have 5: "set_borel_measurable lborel (einterval a b) f" by (rule assms)
+ using lbint_lim by (simp add: interval_integral_Icc [unfolded set_lebesgue_integral_def] approx less_imp_le)
+ have 5: "(\<lambda>x. indicat_real (einterval a b) x *\<^sub>R f x) \<in> borel_measurable lborel"
+ using f_measurable set_borel_measurable_def by blast
have "(LBINT x=a..b. f x) = lebesgue_integral lborel (\<lambda>x. indicator (einterval a b) x *\<^sub>R f x)"
- using assms by (simp add: interval_lebesgue_integral_def less_imp_le)
- also have "... = C" by (rule integral_monotone_convergence [OF 1 2 3 4 5])
+ using assms by (simp add: interval_lebesgue_integral_def set_lebesgue_integral_def less_imp_le)
+ also have "... = C"
+ by (rule integral_monotone_convergence [OF 1 2 3 4 5])
finally show "(LBINT x=a..b. f x) = C" .
-
show "set_integrable lborel (einterval a b) f"
+ unfolding set_integrable_def
by (rule integrable_monotone_convergence[OF 1 2 3 4 5])
qed
@@ -566,13 +567,14 @@
shows "(\<lambda>i. LBINT x=l i.. u i. f x) \<longlonglongrightarrow> (LBINT x=a..b. f x)"
proof -
have "(\<lambda>i. LBINT x:{l i.. u i}. f x) \<longlonglongrightarrow> (LBINT x:einterval a b. f x)"
+ unfolding set_lebesgue_integral_def
proof (rule integral_dominated_convergence)
show "integrable lborel (\<lambda>x. norm (indicator (einterval a b) x *\<^sub>R f x))"
- by (rule integrable_norm) fact
- show "set_borel_measurable lborel (einterval a b) f"
- using f_integrable by (rule borel_measurable_integrable)
- then show "\<And>i. set_borel_measurable lborel {l i..u i} f"
- by (rule set_borel_measurable_subset) (auto simp: approx)
+ using f_integrable integrable_norm set_integrable_def by blast
+ show "(\<lambda>x. indicat_real (einterval a b) x *\<^sub>R f x) \<in> borel_measurable lborel"
+ using f_integrable by (simp add: set_integrable_def)
+ then show "\<And>i. (\<lambda>x. indicat_real {l i..u i} x *\<^sub>R f x) \<in> borel_measurable lborel"
+ by (rule set_borel_measurable_subset [unfolded set_borel_measurable_def]) (auto simp: approx)
show "\<And>i. AE x in lborel. norm (indicator {l i..u i} x *\<^sub>R f x) \<le> norm (indicator (einterval a b) x *\<^sub>R f x)"
by (intro AE_I2) (auto simp: approx split: split_indicator)
show "AE x in lborel. (\<lambda>i. indicator {l i..u i} x *\<^sub>R f x) \<longlonglongrightarrow> indicator (einterval a b) x *\<^sub>R f x"
@@ -591,10 +593,12 @@
by (simp add: interval_lebesgue_integral_le_eq[symmetric] interval_integral_Icc less_imp_le)
qed
+subsection\<open>A slightly stronger Fundamental Theorem of Calculus\<close>
+
+text\<open>Three versions: first, for finite intervals, and then two versions for
+ arbitrary intervals.\<close>
+
(*
- A slightly stronger version of integral_FTC_atLeastAtMost and related facts,
- with continuous_on instead of isCont
-
TODO: make the older versions corollaries of these (using continuous_at_imp_continuous_on, etc.)
*)
@@ -606,28 +610,43 @@
where x and y are real. These should be better automated.
*)
-(*
- The first Fundamental Theorem of Calculus
-
- First, for finite intervals, and then two versions for arbitrary intervals.
-*)
-
lemma interval_integral_FTC_finite:
fixes f F :: "real \<Rightarrow> 'a::euclidean_space" and a b :: real
assumes f: "continuous_on {min a b..max a b} f"
assumes F: "\<And>x. min a b \<le> x \<Longrightarrow> x \<le> max a b \<Longrightarrow> (F has_vector_derivative (f x)) (at x within
{min a b..max a b})"
shows "(LBINT x=a..b. f x) = F b - F a"
- apply (case_tac "a \<le> b")
- apply (subst interval_integral_Icc, simp)
- apply (rule integral_FTC_atLeastAtMost, assumption)
- apply (metis F max_def min_def)
- using f apply (simp add: min_absorb1 max_absorb2)
- apply (subst interval_integral_endpoints_reverse)
- apply (subst interval_integral_Icc, simp)
- apply (subst integral_FTC_atLeastAtMost, auto)
- apply (metis F max_def min_def)
-using f by (simp add: min_absorb2 max_absorb1)
+proof (cases "a \<le> b")
+ case True
+ have "(LBINT x=a..b. f x) = (LBINT x. indicat_real {a..b} x *\<^sub>R f x)"
+ by (simp add: True interval_integral_Icc set_lebesgue_integral_def)
+ also have "... = F b - F a"
+ proof (rule integral_FTC_atLeastAtMost [OF True])
+ show "continuous_on {a..b} f"
+ using True f by linarith
+ show "\<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> (F has_vector_derivative f x) (at x within {a..b})"
+ by (metis F True max.commute max_absorb1 min_def)
+ qed
+ finally show ?thesis .
+next
+ case False
+ then have "b \<le> a"
+ by simp
+ have "- interval_lebesgue_integral lborel (ereal b) (ereal a) f = - (LBINT x. indicat_real {b..a} x *\<^sub>R f x)"
+ by (simp add: \<open>b \<le> a\<close> interval_integral_Icc set_lebesgue_integral_def)
+ also have "... = F b - F a"
+ proof (subst integral_FTC_atLeastAtMost [OF \<open>b \<le> a\<close>])
+ show "continuous_on {b..a} f"
+ using False f by linarith
+ show "\<And>x. \<lbrakk>b \<le> x; x \<le> a\<rbrakk>
+ \<Longrightarrow> (F has_vector_derivative f x) (at x within {b..a})"
+ by (metis F False max_def min_def)
+ qed auto
+ finally show ?thesis
+ by (metis interval_integral_endpoints_reverse)
+qed
+
+
lemma interval_integral_FTC_nonneg:
fixes f F :: "real \<Rightarrow> real" and a b :: ereal
@@ -655,11 +674,12 @@
have 1: "\<And>i. set_integrable lborel {l i..u i} f"
proof -
fix i show "set_integrable lborel {l i .. u i} f"
- using \<open>a < l i\<close> \<open>u i < b\<close>
+ using \<open>a < l i\<close> \<open>u i < b\<close> unfolding set_integrable_def
by (intro borel_integrable_compact f continuous_at_imp_continuous_on compact_Icc ballI)
(auto simp del: ereal_less_eq simp add: ereal_less_eq(3)[symmetric])
qed
have 2: "set_borel_measurable lborel (einterval a b) f"
+ unfolding set_borel_measurable_def
by (auto simp del: real_scaleR_def intro!: borel_measurable_continuous_on_indicator
simp: continuous_on_eq_continuous_at einterval_iff f)
have 3: "(\<lambda>i. LBINT x=l i..u i. f x) \<longlonglongrightarrow> B - A"
@@ -779,12 +799,10 @@
qed
qed
-(*
- The substitution theorem
+subsection\<open>The substitution theorem\<close>
- Once again, three versions: first, for finite intervals, and then two versions for
- arbitrary intervals.
-*)
+text\<open>Once again, three versions: first, for finite intervals, and then two versions for
+ arbitrary intervals.\<close>
lemma interval_integral_substitution_finite:
fixes a b :: real and f :: "real \<Rightarrow> 'a::euclidean_space"
@@ -824,6 +842,7 @@
by (blast intro: continuous_on_compose2 contf contg)
have "LBINT x=a..b. g' x *\<^sub>R f (g x) = F (g b) - F (g a)"
apply (subst interval_integral_Icc, simp add: assms)
+ unfolding set_lebesgue_integral_def
apply (rule integral_FTC_atLeastAtMost[of a b "\<lambda>x. F (g x)", OF \<open>a \<le> b\<close>])
apply (rule vector_diff_chain_within[OF v_derivg derivF, unfolded comp_def])
apply (auto intro!: continuous_on_scaleR contg' contfg)
@@ -1093,7 +1112,7 @@
shows "interval_lebesgue_integrable lborel a b f \<Longrightarrow> a \<le> b \<Longrightarrow>
norm (LBINT t=a..b. f t) \<le> LBINT t=a..b. norm (f t)"
using integral_norm_bound[of lborel "\<lambda>x. indicator (einterval a b) x *\<^sub>R f x"]
- by (auto simp add: interval_lebesgue_integral_def interval_lebesgue_integrable_def)
+ by (auto simp add: interval_lebesgue_integral_def interval_lebesgue_integrable_def set_lebesgue_integral_def)
lemma interval_integral_norm2:
"interval_lebesgue_integrable lborel a b f \<Longrightarrow>
@@ -1105,7 +1124,7 @@
case (le a b)
then have "\<bar>LBINT t=a..b. norm (f t)\<bar> = LBINT t=a..b. norm (f t)"
using integrable_norm[of lborel "\<lambda>x. indicator (einterval a b) x *\<^sub>R f x"]
- by (auto simp add: interval_lebesgue_integral_def interval_lebesgue_integrable_def
+ by (auto simp add: interval_lebesgue_integral_def interval_lebesgue_integrable_def set_lebesgue_integral_def
intro!: integral_nonneg_AE abs_of_nonneg)
then show ?case
using le by (simp add: interval_integral_norm)
--- a/src/HOL/Analysis/Set_Integral.thy Mon Apr 09 17:21:10 2018 +0100
+++ b/src/HOL/Analysis/Set_Integral.thy Wed Apr 11 16:34:44 2018 +0100
@@ -15,18 +15,18 @@
Notation
*)
-abbreviation "set_borel_measurable M A f \<equiv> (\<lambda>x. indicator A x *\<^sub>R f x) \<in> borel_measurable M"
+definition "set_borel_measurable M A f \<equiv> (\<lambda>x. indicator A x *\<^sub>R f x) \<in> borel_measurable M"
-abbreviation "set_integrable M A f \<equiv> integrable M (\<lambda>x. indicator A x *\<^sub>R f x)"
+definition "set_integrable M A f \<equiv> integrable M (\<lambda>x. indicator A x *\<^sub>R f x)"
-abbreviation "set_lebesgue_integral M A f \<equiv> lebesgue_integral M (\<lambda>x. indicator A x *\<^sub>R f x)"
+definition "set_lebesgue_integral M A f \<equiv> lebesgue_integral M (\<lambda>x. indicator A x *\<^sub>R f x)"
syntax
-"_ascii_set_lebesgue_integral" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real"
-("(4LINT (_):(_)/|(_)./ _)" [0,60,110,61] 60)
+ "_ascii_set_lebesgue_integral" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real"
+ ("(4LINT (_):(_)/|(_)./ _)" [0,60,110,61] 60)
translations
-"LINT x:A|M. f" == "CONST set_lebesgue_integral M A (\<lambda>x. f)"
+ "LINT x:A|M. f" == "CONST set_lebesgue_integral M A (\<lambda>x. f)"
(*
Notation for integration wrt lebesgue measure on the reals:
@@ -38,12 +38,12 @@
*)
syntax
-"_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> real"
-("(2LBINT _./ _)" [0,60] 60)
+ "_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> real"
+ ("(2LBINT _./ _)" [0,60] 60)
syntax
-"_set_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real set \<Rightarrow> real \<Rightarrow> real"
-("(3LBINT _:_./ _)" [0,60,61] 60)
+ "_set_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real set \<Rightarrow> real \<Rightarrow> real"
+ ("(3LBINT _:_./ _)" [0,60,61] 60)
(*
Basic properties
@@ -60,7 +60,7 @@
shows "f -` B \<inter> X \<in> sets M"
proof -
have "f \<in> borel_measurable (restrict_space M X)"
- using assms by (subst borel_measurable_restrict_space_iff) auto
+ using assms unfolding set_borel_measurable_def by (subst borel_measurable_restrict_space_iff) auto
then have "f -` B \<inter> space (restrict_space M X) \<in> sets (restrict_space M X)"
by (rule measurable_sets) fact
with \<open>X \<in> sets M\<close> show ?thesis
@@ -70,7 +70,9 @@
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!: Bochner_Integration.integral_cong split: split_indicator simp add: sets.sets_into_space)
+ unfolding set_lebesgue_integral_def
+ using assms
+ by (metis indicator_simps(2) real_vector.scale_zero_left)
lemma set_lebesgue_integral_cong_AE:
assumes [measurable]: "A \<in> sets M" "f \<in> borel_measurable M" "g \<in> borel_measurable M"
@@ -79,13 +81,15 @@
proof-
have "AE x in M. indicator A x *\<^sub>R f x = indicator A x *\<^sub>R g x"
using assms by auto
- thus ?thesis by (intro integral_cong_AE) auto
+ thus ?thesis
+ unfolding set_lebesgue_integral_def by (intro integral_cong_AE) auto
qed
lemma set_integrable_cong_AE:
"f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow>
AE x \<in> A in M. f x = g x \<Longrightarrow> A \<in> sets M \<Longrightarrow>
set_integrable M A f = set_integrable M A g"
+ unfolding set_integrable_def
by (rule integrable_cong_AE) auto
lemma set_integrable_subset:
@@ -94,8 +98,9 @@
shows "set_integrable M B f"
proof -
have "set_integrable M B (\<lambda>x. indicator A x *\<^sub>R f x)"
- by (rule integrable_mult_indicator) fact+
+ using assms integrable_mult_indicator set_integrable_def by blast
with \<open>B \<subseteq> A\<close> show ?thesis
+ unfolding set_integrable_def
by (simp add: indicator_inter_arith[symmetric] Int_absorb2)
qed
@@ -104,11 +109,12 @@
assumes f: "set_integrable M S f" and T: "T \<in> sets (restrict_space M S)"
shows "set_integrable M T f"
proof -
- obtain T' where T_eq: "T = S \<inter> T'" and "T' \<in> sets M" using T by (auto simp: sets_restrict_space)
-
+ obtain T' where T_eq: "T = S \<inter> T'" and "T' \<in> sets M"
+ using T by (auto simp: sets_restrict_space)
have \<open>integrable M (\<lambda>x. indicator T' x *\<^sub>R (indicator S x *\<^sub>R f x))\<close>
- by (rule integrable_mult_indicator; fact)
+ using \<open>T' \<in> sets M\<close> f integrable_mult_indicator set_integrable_def by blast
then show ?thesis
+ unfolding set_integrable_def
unfolding T_eq indicator_inter_arith by (simp add: ac_simps)
qed
@@ -116,41 +122,49 @@
(* 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)"
+ unfolding set_lebesgue_integral_def
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)"
+ unfolding set_lebesgue_integral_def
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"
+ unfolding set_lebesgue_integral_def
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"
+ unfolding set_lebesgue_integral_def
by (subst integral_divide_zero[symmetric], intro Bochner_Integration.integral_cong)
(auto split: split_indicator)
lemma set_integrable_scaleR_right [simp, intro]:
shows "(a \<noteq> 0 \<Longrightarrow> set_integrable M A f) \<Longrightarrow> set_integrable M A (\<lambda>t. a *\<^sub>R f t)"
+ unfolding set_integrable_def
unfolding scaleR_left_commute by (rule integrable_scaleR_right)
lemma set_integrable_scaleR_left [simp, intro]:
fixes a :: "_ :: {banach, second_countable_topology}"
shows "(a \<noteq> 0 \<Longrightarrow> set_integrable M A f) \<Longrightarrow> set_integrable M A (\<lambda>t. f t *\<^sub>R a)"
+ unfolding set_integrable_def
using integrable_scaleR_left[of a M "\<lambda>x. indicator A x *\<^sub>R f x"] by simp
lemma set_integrable_mult_right [simp, intro]:
fixes a :: "'a::{real_normed_field, second_countable_topology}"
shows "(a \<noteq> 0 \<Longrightarrow> set_integrable M A f) \<Longrightarrow> set_integrable M A (\<lambda>t. a * f t)"
+ unfolding set_integrable_def
using integrable_mult_right[of a M "\<lambda>x. indicator A x *\<^sub>R f x"] by simp
lemma set_integrable_mult_left [simp, intro]:
fixes a :: "'a::{real_normed_field, second_countable_topology}"
shows "(a \<noteq> 0 \<Longrightarrow> set_integrable M A f) \<Longrightarrow> set_integrable M A (\<lambda>t. f t * a)"
+ unfolding set_integrable_def
using integrable_mult_left[of a M "\<lambda>x. indicator A x *\<^sub>R f x"] by simp
lemma set_integrable_divide [simp, intro]:
@@ -159,10 +173,11 @@
shows "set_integrable M A (\<lambda>t. f t / a)"
proof -
have "integrable M (\<lambda>x. indicator A x *\<^sub>R f x / a)"
- using assms by (rule integrable_divide_zero)
+ using assms unfolding set_integrable_def by (rule integrable_divide_zero)
also have "(\<lambda>x. indicator A x *\<^sub>R f x / a) = (\<lambda>x. indicator A x *\<^sub>R (f x / a))"
by (auto split: split_indicator)
- finally show ?thesis .
+ finally show ?thesis
+ unfolding set_integrable_def .
qed
lemma set_integral_add [simp, intro]:
@@ -170,21 +185,23 @@
assumes "set_integrable M A f" "set_integrable M A g"
shows "set_integrable M A (\<lambda>x. f x + g x)"
and "LINT x:A|M. f x + g x = (LINT x:A|M. f x) + (LINT x:A|M. g x)"
- using assms by (simp_all add: scaleR_add_right)
+ using assms unfolding set_integrable_def set_lebesgue_integral_def by (simp_all add: scaleR_add_right)
lemma set_integral_diff [simp, intro]:
assumes "set_integrable M A f" "set_integrable M A g"
shows "set_integrable M A (\<lambda>x. f x - g x)" and "LINT x:A|M. f x - g x =
(LINT x:A|M. f x) - (LINT x:A|M. g x)"
- using assms by (simp_all add: scaleR_diff_right)
+ using assms unfolding set_integrable_def set_lebesgue_integral_def by (simp_all add: scaleR_diff_right)
(* question: why do we have this for negation, but multiplication by a constant
requires an integrability assumption? *)
lemma set_integral_uminus: "set_integrable M A f \<Longrightarrow> LINT x:A|M. - f x = - (LINT x:A|M. f x)"
+ unfolding set_integrable_def set_lebesgue_integral_def
by (subst integral_minus[symmetric]) simp_all
lemma set_integral_complex_of_real:
"LINT x:A|M. complex_of_real (f x) = of_real (LINT x:A|M. f x)"
+ unfolding set_lebesgue_integral_def
by (subst integral_complex_of_real[symmetric])
(auto intro!: Bochner_Integration.integral_cong split: split_indicator)
@@ -193,28 +210,31 @@
assumes "set_integrable M A f" "set_integrable M A g"
"\<And>x. x \<in> A \<Longrightarrow> f x \<le> g x"
shows "(LINT x:A|M. f x) \<le> (LINT x:A|M. g x)"
-using assms by (auto intro: integral_mono split: split_indicator)
+ using assms unfolding set_integrable_def set_lebesgue_integral_def
+ by (auto intro: integral_mono split: split_indicator)
lemma set_integral_mono_AE:
fixes f g :: "_ \<Rightarrow> real"
assumes "set_integrable M A f" "set_integrable M A g"
"AE x \<in> A in M. f x \<le> g x"
shows "(LINT x:A|M. f x) \<le> (LINT x:A|M. g x)"
-using assms by (auto intro: integral_mono_AE split: split_indicator)
+ using assms unfolding set_integrable_def set_lebesgue_integral_def
+ by (auto intro: integral_mono_AE split: split_indicator)
lemma set_integrable_abs: "set_integrable M A f \<Longrightarrow> set_integrable M A (\<lambda>x. \<bar>f x\<bar> :: real)"
- using integrable_abs[of M "\<lambda>x. f x * indicator A x"] by (simp add: abs_mult ac_simps)
+ using integrable_abs[of M "\<lambda>x. f x * indicator A x"]unfolding set_integrable_def by (simp add: abs_mult ac_simps)
lemma set_integrable_abs_iff:
fixes f :: "_ \<Rightarrow> real"
shows "set_borel_measurable M A f \<Longrightarrow> set_integrable M A (\<lambda>x. \<bar>f x\<bar>) = set_integrable M A f"
+ unfolding set_integrable_def set_borel_measurable_def
by (subst (2) integrable_abs_iff[symmetric]) (simp_all add: abs_mult ac_simps)
lemma set_integrable_abs_iff':
fixes f :: "_ \<Rightarrow> real"
shows "f \<in> borel_measurable M \<Longrightarrow> A \<in> sets M \<Longrightarrow>
set_integrable M A (\<lambda>x. \<bar>f x\<bar>) = set_integrable M A f"
-by (intro set_integrable_abs_iff) auto
+ by (simp add: set_borel_measurable_def set_integrable_abs_iff)
lemma set_integrable_discrete_difference:
fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
@@ -222,6 +242,7 @@
assumes diff: "(A - B) \<union> (B - A) \<subseteq> X"
assumes "\<And>x. x \<in> X \<Longrightarrow> emeasure M {x} = 0" "\<And>x. x \<in> X \<Longrightarrow> {x} \<in> sets M"
shows "set_integrable M A f \<longleftrightarrow> set_integrable M B f"
+ unfolding set_integrable_def
proof (rule integrable_discrete_difference[where X=X])
show "\<And>x. x \<in> space M \<Longrightarrow> x \<notin> X \<Longrightarrow> indicator A x *\<^sub>R f x = indicator B x *\<^sub>R f x"
using diff by (auto split: split_indicator)
@@ -233,6 +254,7 @@
assumes diff: "(A - B) \<union> (B - A) \<subseteq> X"
assumes "\<And>x. x \<in> X \<Longrightarrow> emeasure M {x} = 0" "\<And>x. x \<in> X \<Longrightarrow> {x} \<in> sets M"
shows "set_lebesgue_integral M A f = set_lebesgue_integral M B f"
+ unfolding set_lebesgue_integral_def
proof (rule integral_discrete_difference[where X=X])
show "\<And>x. x \<in> space M \<Longrightarrow> x \<notin> X \<Longrightarrow> indicator A x *\<^sub>R f x = indicator B x *\<^sub>R f x"
using diff by (auto split: split_indicator)
@@ -246,35 +268,44 @@
proof -
have "set_integrable M (A - B) f"
using f_A by (rule set_integrable_subset) auto
- from Bochner_Integration.integrable_add[OF this f_B] show ?thesis
+ with f_B have "integrable M (\<lambda>x. indicator (A - B) x *\<^sub>R f x + indicator B x *\<^sub>R f x)"
+ unfolding set_integrable_def using integrable_add by blast
+ then show ?thesis
+ unfolding set_integrable_def
by (rule integrable_cong[THEN iffD1, rotated 2]) (auto split: split_indicator)
qed
+lemma set_integrable_empty [simp]: "set_integrable M {} f"
+ by (auto simp: set_integrable_def)
+
lemma set_integrable_UN:
fixes f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
assumes "finite I" "\<And>i. i\<in>I \<Longrightarrow> set_integrable M (A i) f"
"\<And>i. i\<in>I \<Longrightarrow> A i \<in> sets M"
shows "set_integrable M (\<Union>i\<in>I. A i) f"
-using assms by (induct I) (auto intro!: set_integrable_Un)
+ using assms
+ by (induct I) (auto simp: set_integrable_Un sets.finite_UN)
lemma set_integral_Un:
fixes f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
assumes "A \<inter> B = {}"
and "set_integrable M A f"
and "set_integrable M B f"
- shows "LINT x:A\<union>B|M. f x = (LINT x:A|M. f x) + (LINT x:B|M. f x)"
-by (auto simp add: indicator_union_arith indicator_inter_arith[symmetric]
- scaleR_add_left assms)
+shows "LINT x:A\<union>B|M. f x = (LINT x:A|M. f x) + (LINT x:B|M. f x)"
+ using assms
+ unfolding set_integrable_def set_lebesgue_integral_def
+ by (auto simp add: indicator_union_arith indicator_inter_arith[symmetric] scaleR_add_left)
lemma set_integral_cong_set:
fixes f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
- assumes [measurable]: "set_borel_measurable M A f" "set_borel_measurable M B f"
+ assumes "set_borel_measurable M A f" "set_borel_measurable M B f"
and ae: "AE x in M. x \<in> A \<longleftrightarrow> x \<in> B"
shows "LINT x:B|M. f x = LINT x:A|M. f x"
+ unfolding set_lebesgue_integral_def
proof (rule integral_cong_AE)
show "AE x in M. indicator B x *\<^sub>R f x = indicator A x *\<^sub>R f x"
using ae by (auto simp: subset_eq split: split_indicator)
-qed fact+
+qed (use assms in \<open>auto simp: set_borel_measurable_def\<close>)
lemma set_borel_measurable_subset:
fixes f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
@@ -282,10 +313,12 @@
shows "set_borel_measurable M B f"
proof -
have "set_borel_measurable M B (\<lambda>x. indicator A x *\<^sub>R f x)"
- by measurable
- also have "(\<lambda>x. indicator B x *\<^sub>R indicator A x *\<^sub>R f x) = (\<lambda>x. indicator B x *\<^sub>R f x)"
+ using assms unfolding set_borel_measurable_def
+ using borel_measurable_indicator borel_measurable_scaleR by blast
+ moreover have "(\<lambda>x. indicator B x *\<^sub>R indicator A x *\<^sub>R f x) = (\<lambda>x. indicator B x *\<^sub>R f x)"
using \<open>B \<subseteq> A\<close> by (auto simp: fun_eq_iff split: split_indicator)
- finally show ?thesis .
+ ultimately show ?thesis
+ unfolding set_borel_measurable_def by simp
qed
lemma set_integral_Un_AE:
@@ -298,7 +331,7 @@
have f: "set_integrable M (A \<union> B) f"
by (intro set_integrable_Un assms)
then have f': "set_borel_measurable M (A \<union> B) f"
- by (rule borel_measurable_integrable)
+ using integrable_iff_bounded set_borel_measurable_def set_integrable_def by blast
have "LINT x:A\<union>B|M. f x = LINT x:(A - A \<inter> B) \<union> (B - A \<inter> B)|M. f x"
proof (rule set_integral_cong_set)
show "AE x in M. (x \<in> A - A \<inter> B \<union> (B - A \<inter> B)) = (x \<in> A \<union> B)"
@@ -321,9 +354,13 @@
and "\<And>i. i \<in> I \<Longrightarrow> set_integrable M (A i) f" "\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets M"
shows "(LINT x:(\<Union>i\<in>I. A i)|M. f x) = (\<Sum>i\<in>I. LINT x:A i|M. f x)"
using assms
- apply induct
- apply (auto intro!: set_integral_Un set_integrable_Un set_integrable_UN simp: disjoint_family_on_def)
-by (subst set_integral_Un, auto intro: set_integrable_UN)
+proof induction
+ case (insert x F)
+ then have "A x \<inter> UNION F A = {}"
+ by (meson disjoint_family_on_insert)
+ with insert show ?case
+ by (simp add: set_integral_Un set_integrable_Un set_integrable_UN disjoint_family_on_insert)
+qed (simp add: set_lebesgue_integral_def)
(* TODO: find a better name? *)
lemma pos_integrable_to_top:
@@ -332,10 +369,11 @@
assumes nneg: "\<And>x i. x \<in> A i \<Longrightarrow> 0 \<le> f x"
and intgbl: "\<And>i::nat. set_integrable M (A i) f"
and lim: "(\<lambda>i::nat. LINT x:A i|M. f x) \<longlonglongrightarrow> l"
- shows "set_integrable M (\<Union>i. A i) f"
+shows "set_integrable M (\<Union>i. A i) f"
+ unfolding set_integrable_def
apply (rule integrable_monotone_convergence[where f = "\<lambda>i::nat. \<lambda>x. indicator (A i) x *\<^sub>R f x" and x = l])
- apply (rule intgbl)
- prefer 3 apply (rule lim)
+ apply (rule intgbl [unfolded set_integrable_def])
+ prefer 3 apply (rule lim [unfolded set_lebesgue_integral_def])
apply (rule AE_I2)
using \<open>mono A\<close> apply (auto simp: mono_def nneg split: split_indicator) []
proof (rule AE_I2)
@@ -356,8 +394,7 @@
then show "(\<lambda>x. indicator (\<Union>i. A i) x *\<^sub>R f x) \<in> borel_measurable M"
apply (rule borel_measurable_LIMSEQ_real)
apply assumption
- apply (intro borel_measurable_integrable intgbl)
- done
+ using intgbl set_integrable_def by blast
qed
(* Proof from Royden Real Analysis, p. 91. *)
@@ -367,16 +404,18 @@
and disj: "\<And>i j. i \<noteq> j \<Longrightarrow> A i \<inter> A j = {}"
and intgbl: "set_integrable M (\<Union>i. A i) f"
shows "LINT x:(\<Union>i. A i)|M. f x = (\<Sum>i. (LINT x:(A i)|M. f x))"
+ unfolding set_lebesgue_integral_def
proof (subst integral_suminf[symmetric])
- show int_A: "\<And>i. set_integrable M (A i) f"
- using intgbl by (rule set_integrable_subset) auto
+ show int_A: "integrable M (\<lambda>x. indicat_real (A i) x *\<^sub>R f x)" for i
+ using intgbl unfolding set_integrable_def [symmetric]
+ by (rule set_integrable_subset) auto
{ fix x assume "x \<in> space M"
have "(\<lambda>i. indicator (A i) x *\<^sub>R f x) sums (indicator (\<Union>i. A i) x *\<^sub>R f x)"
by (intro sums_scaleR_left indicator_sums) fact }
note sums = this
have norm_f: "\<And>i. set_integrable M (A i) (\<lambda>x. norm (f x))"
- using int_A[THEN integrable_norm] by auto
+ using int_A[THEN integrable_norm] unfolding set_integrable_def by auto
show "AE x in M. summable (\<lambda>i. norm (indicator (A i) x *\<^sub>R f x))"
using disj by (intro AE_I2) (auto intro!: summable_mult2 sums_summable[OF indicator_sums])
@@ -387,21 +426,22 @@
show "0 \<le> LINT x|M. norm (indicator (A n) x *\<^sub>R f x)"
using norm_f by (auto intro!: integral_nonneg_AE)
- have "(\<Sum>i<n. LINT x|M. norm (indicator (A i) x *\<^sub>R f x)) =
- (\<Sum>i<n. set_lebesgue_integral M (A i) (\<lambda>x. norm (f x)))"
- by (simp add: abs_mult)
+ have "(\<Sum>i<n. LINT x|M. norm (indicator (A i) x *\<^sub>R f x)) = (\<Sum>i<n. LINT x:A i|M. norm (f x))"
+ by (simp add: abs_mult set_lebesgue_integral_def)
also have "\<dots> = set_lebesgue_integral M (\<Union>i<n. A i) (\<lambda>x. norm (f x))"
using norm_f
by (subst set_integral_finite_Union) (auto simp: disjoint_family_on_def disj)
also have "\<dots> \<le> set_lebesgue_integral M (\<Union>i. A i) (\<lambda>x. norm (f x))"
- using intgbl[THEN integrable_norm]
- by (intro integral_mono set_integrable_UN[of "{..<n}"] norm_f)
- (auto split: split_indicator)
+ using intgbl[unfolded set_integrable_def, THEN integrable_norm] norm_f
+ unfolding set_lebesgue_integral_def set_integrable_def
+ apply (intro integral_mono set_integrable_UN[of "{..<n}", unfolded set_integrable_def])
+ apply (auto split: split_indicator)
+ done
finally show "(\<Sum>i<n. LINT x|M. norm (indicator (A i) x *\<^sub>R f x)) \<le>
set_lebesgue_integral M (\<Union>i. A i) (\<lambda>x. norm (f x))"
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)"
+ show "LINT x|M. indicator (UNION UNIV A) x *\<^sub>R f x = LINT x|M. (\<Sum>i. indicator (A i) x *\<^sub>R f x)"
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]]
@@ -413,14 +453,18 @@
fixes f :: "_ \<Rightarrow> 'a :: {banach, second_countable_topology}"
assumes [measurable]: "\<And>i. A i \<in> sets M" and A: "incseq A"
and intgbl: "set_integrable M (\<Union>i. A i) f"
- shows "(\<lambda>i. LINT x:(A i)|M. f x) \<longlonglongrightarrow> LINT x:(\<Union>i. A i)|M. f x"
+shows "(\<lambda>i. LINT x:(A i)|M. f x) \<longlonglongrightarrow> LINT x:(\<Union>i. A i)|M. f x"
+ unfolding set_lebesgue_integral_def
proof (intro integral_dominated_convergence[where w="\<lambda>x. indicator (\<Union>i. A i) x *\<^sub>R norm (f x)"])
have int_A: "\<And>i. set_integrable M (A i) f"
using intgbl by (rule set_integrable_subset) auto
- then show "\<And>i. set_borel_measurable M (A i) f" "set_borel_measurable M (\<Union>i. A i) f"
- "set_integrable M (\<Union>i. A i) (\<lambda>x. norm (f x))"
- using intgbl integrable_norm[OF intgbl] by auto
-
+ show "\<And>i. (\<lambda>x. indicator (A i) x *\<^sub>R f x) \<in> borel_measurable M"
+ using int_A integrable_iff_bounded set_integrable_def by blast
+ show "(\<lambda>x. indicator (UNION UNIV A) x *\<^sub>R f x) \<in> borel_measurable M"
+ using integrable_iff_bounded intgbl set_integrable_def by blast
+ show "integrable M (\<lambda>x. indicator (\<Union>i. A i) x *\<^sub>R norm (f x))"
+ using int_A intgbl integrable_norm unfolding set_integrable_def
+ by fastforce
{ fix x i assume "x \<in> A i"
with A have "(\<lambda>xa. indicator (A xa) x::real) \<longlonglongrightarrow> 1 \<longleftrightarrow> (\<lambda>xa. 1::real) \<longlonglongrightarrow> 1"
by (intro filterlim_cong refl)
@@ -435,15 +479,19 @@
assumes [measurable]: "\<And>i. A i \<in> sets M" and A: "decseq A"
and int0: "set_integrable M (A 0) f"
shows "(\<lambda>i::nat. LINT x:(A i)|M. f x) \<longlonglongrightarrow> LINT x:(\<Inter>i. A i)|M. f x"
+ unfolding set_lebesgue_integral_def
proof (rule integral_dominated_convergence)
have int_A: "\<And>i. set_integrable M (A i) f"
using int0 by (rule set_integrable_subset) (insert A, auto simp: decseq_def)
- show "set_integrable M (A 0) (\<lambda>x. norm (f x))"
- using int0[THEN integrable_norm] by simp
+ have "integrable M (\<lambda>c. norm (indicat_real (A 0) c *\<^sub>R f c))"
+ by (metis (no_types) int0 integrable_norm set_integrable_def)
+ then show "integrable M (\<lambda>x. indicator (A 0) x *\<^sub>R norm (f x))"
+ by force
have "set_integrable M (\<Inter>i. A i) f"
using int0 by (rule set_integrable_subset) (insert A, auto simp: decseq_def)
- with int_A show "set_borel_measurable M (\<Inter>i. A i) f" "\<And>i. set_borel_measurable M (A i) f"
- by auto
+ with int_A show "(\<lambda>x. indicat_real (INTER UNIV A) x *\<^sub>R f x) \<in> borel_measurable M"
+ "\<And>i. (\<lambda>x. indicat_real (A i) x *\<^sub>R f x) \<in> borel_measurable M"
+ by (auto simp: set_integrable_def)
show "\<And>i. AE x in M. norm (indicator (A i) x *\<^sub>R f x) \<le> indicator (A 0) x *\<^sub>R norm (f x)"
using A by (auto split: split_indicator simp: decseq_def)
{ fix x i assume "x \<in> space M" "x \<notin> A i"
@@ -462,7 +510,8 @@
proof-
have "set_lebesgue_integral M {a} f = set_lebesgue_integral M {a} (%x. f a)"
by (intro set_lebesgue_integral_cong) simp_all
- then show ?thesis using assms by simp
+ then show ?thesis using assms
+ unfolding set_lebesgue_integral_def by simp
qed
@@ -523,6 +572,7 @@
lemma set_measurable_continuous_on_ivl:
assumes "continuous_on {a..b} (f :: real \<Rightarrow> real)"
shows "set_borel_measurable borel {a..b} f"
+ unfolding set_borel_measurable_def
by (rule borel_measurable_continuous_on_indicator[OF _ assms]) simp
@@ -670,19 +720,19 @@
lemma set_integral_null_delta:
fixes f::"_ \<Rightarrow> _ :: {banach, second_countable_topology}"
assumes [measurable]: "integrable M f" "A \<in> sets M" "B \<in> sets M"
- and "(A - B) \<union> (B - A) \<in> null_sets M"
+ and null: "(A - B) \<union> (B - A) \<in> null_sets M"
shows "(\<integral>x \<in> A. f x \<partial>M) = (\<integral>x \<in> B. f x \<partial>M)"
-proof (rule set_integral_cong_set, auto)
+proof (rule set_integral_cong_set)
have *: "AE a in M. a \<notin> (A - B) \<union> (B - A)"
- using assms(4) AE_not_in by blast
+ using null AE_not_in by blast
then show "AE x in M. (x \<in> B) = (x \<in> A)"
by auto
-qed
+qed (simp_all add: set_borel_measurable_def)
lemma set_integral_space:
assumes "integrable M f"
shows "(\<integral>x \<in> space M. f x \<partial>M) = (\<integral>x. f x \<partial>M)"
-by (metis (mono_tags, lifting) indicator_simps(1) Bochner_Integration.integral_cong real_vector.scale_one)
+ by (metis (no_types, lifting) indicator_simps(1) integral_cong scaleR_one set_lebesgue_integral_def)
lemma null_if_pos_func_has_zero_nn_int:
fixes f::"'a \<Rightarrow> ennreal"
@@ -703,7 +753,8 @@
proof -
have "AE x in M. indicator A x * f x = 0"
apply (subst integral_nonneg_eq_0_iff_AE[symmetric])
- using assms integrable_mult_indicator[OF \<open>A \<in> sets M\<close> assms(1)] by auto
+ using assms integrable_mult_indicator[OF \<open>A \<in> sets M\<close> assms(1)]
+ by (auto simp: set_lebesgue_integral_def)
then have "AE x\<in>A in M. f x = 0" by auto
then have "AE x\<in>A in M. False" using assms(3) by auto
then show "A \<in> null_sets M" using assms(2) by (simp add: AE_iff_null_sets)
@@ -728,31 +779,29 @@
lemma density_unique_real:
fixes f f'::"_ \<Rightarrow> real"
- assumes [measurable]: "integrable M f" "integrable M f'"
+ assumes M[measurable]: "integrable M f" "integrable M f'"
assumes density_eq: "\<And>A. A \<in> sets M \<Longrightarrow> (\<integral>x \<in> A. f x \<partial>M) = (\<integral>x \<in> A. f' x \<partial>M)"
shows "AE x in M. f x = f' x"
proof -
define A where "A = {x \<in> space M. f x < f' x}"
then have [measurable]: "A \<in> sets M" by simp
have "(\<integral>x \<in> A. (f' x - f x) \<partial>M) = (\<integral>x \<in> A. f' x \<partial>M) - (\<integral>x \<in> A. f x \<partial>M)"
- using \<open>A \<in> sets M\<close> assms(1) assms(2) integrable_mult_indicator by blast
+ using \<open>A \<in> sets M\<close> M integrable_mult_indicator set_integrable_def by blast
then have "(\<integral>x \<in> A. (f' x - f x) \<partial>M) = 0" using assms(3) by simp
then have "A \<in> null_sets M"
using A_def null_if_pos_func_has_zero_int[where ?f = "\<lambda>x. f' x - f x" and ?A = A] assms by auto
then have "AE x in M. x \<notin> A" by (simp add: AE_not_in)
then have *: "AE x in M. f' x \<le> f x" unfolding A_def by auto
-
define B where "B = {x \<in> space M. f' x < f x}"
then have [measurable]: "B \<in> sets M" by simp
have "(\<integral>x \<in> B. (f x - f' x) \<partial>M) = (\<integral>x \<in> B. f x \<partial>M) - (\<integral>x \<in> B. f' x \<partial>M)"
- using \<open>B \<in> sets M\<close> assms(1) assms(2) integrable_mult_indicator by blast
+ using \<open>B \<in> sets M\<close> M integrable_mult_indicator set_integrable_def by blast
then have "(\<integral>x \<in> B. (f x - f' x) \<partial>M) = 0" using assms(3) by simp
then have "B \<in> null_sets M"
using B_def null_if_pos_func_has_zero_int[where ?f = "\<lambda>x. f x - f' x" and ?A = B] assms by auto
then have "AE x in M. x \<notin> B" by (simp add: AE_not_in)
then have "AE x in M. f' x \<ge> f x" unfolding B_def by auto
-
then show ?thesis using * by auto
qed