--- a/src/HOL/Probability/Complete_Measure.thy Fri Feb 04 14:16:48 2011 +0100
+++ b/src/HOL/Probability/Complete_Measure.thy Fri Feb 04 14:16:55 2011 +0100
@@ -266,7 +266,7 @@
proof (intro bexI)
from AE[unfolded all_AE_countable]
show "AE x. g x = (SUP i. f' i x)" (is "AE x. g x = ?f x")
- proof (rule AE_mp, safe intro!: AE_cong)
+ proof (elim AE_mp, safe intro!: AE_I2)
fix x assume eq: "\<forall>i. f i x = f' i x"
moreover have "g = SUPR UNIV f" using `f \<up> g` unfolding isoton_def by simp
ultimately show "g x = ?f x" by (simp add: SUPR_apply)
--- a/src/HOL/Probability/Lebesgue_Integration.thy Fri Feb 04 14:16:48 2011 +0100
+++ b/src/HOL/Probability/Lebesgue_Integration.thy Fri Feb 04 14:16:55 2011 +0100
@@ -694,10 +694,7 @@
assumes "simple_function M f" and "simple_function M g"
and mono: "\<And> x. x \<in> space M \<Longrightarrow> f x \<le> g x"
shows "integral\<^isup>S M f \<le> integral\<^isup>S M g"
-proof (rule simple_integral_mono_AE[OF assms(1, 2)])
- show "AE x. f x \<le> g x"
- using mono by (rule AE_cong) auto
-qed
+ using assms by (intro simple_integral_mono_AE) auto
lemma (in measure_space) simple_integral_cong_AE:
assumes "simple_function M f" "simple_function M g" and "AE x. f x = g x"
@@ -782,20 +779,14 @@
have "AE x. indicator N x = (0 :: pextreal)"
using `N \<in> null_sets` by (auto simp: indicator_def intro!: AE_I[of _ N])
then have "(\<integral>\<^isup>Sx. u x * indicator N x \<partial>M) = (\<integral>\<^isup>Sx. 0 \<partial>M)"
- using assms by (intro simple_integral_cong_AE) (auto intro!: AE_disjI2)
+ using assms by (intro simple_integral_cong_AE) auto
then show ?thesis by simp
qed
lemma (in measure_space) simple_integral_cong_AE_mult_indicator:
assumes sf: "simple_function M f" and eq: "AE x. x \<in> S" and "S \<in> sets M"
shows "integral\<^isup>S M f = (\<integral>\<^isup>Sx. f x * indicator S x \<partial>M)"
-proof (rule simple_integral_cong_AE)
- show "simple_function M f" by fact
- show "simple_function M (\<lambda>x. f x * indicator S x)"
- using sf `S \<in> sets M` by auto
- from eq show "AE x. f x = f x * indicator S x"
- by (rule AE_mp) simp
-qed
+ using assms by (intro simple_integral_cong_AE) auto
lemma (in measure_space) simple_integral_restricted:
assumes "A \<in> sets M"
@@ -1004,7 +995,7 @@
have *: "{x \<in> space M. \<not> a x \<le> a x * indicator (space M - N) x} =
N \<inter> {x \<in> space M. a x \<noteq> 0}" (is "?N = _")
using `N \<in> sets M`[THEN sets_into_space] by (auto simp: indicator_def)
- then show "?N \<in> sets M"
+ then show "?N \<in> sets M"
using `N \<in> sets M` `simple_function M a`[THEN borel_measurable_simple_function]
by (auto intro!: measure_mono Int)
then have "\<mu> ?N \<le> \<mu> N"
@@ -1032,9 +1023,8 @@
by (auto simp: eq_iff intro!: positive_integral_mono_AE)
lemma (in measure_space) positive_integral_mono:
- assumes mono: "\<And>x. x \<in> space M \<Longrightarrow> u x \<le> v x"
- shows "integral\<^isup>P M u \<le> integral\<^isup>P M v"
- using mono by (auto intro!: AE_cong positive_integral_mono_AE)
+ "(\<And>x. x \<in> space M \<Longrightarrow> u x \<le> v x) \<Longrightarrow> integral\<^isup>P M u \<le> integral\<^isup>P M v"
+ by (auto intro: positive_integral_mono_AE)
lemma image_set_cong:
assumes A: "\<And>x. x \<in> A \<Longrightarrow> \<exists>y\<in>B. f x = g y"
@@ -1487,6 +1477,16 @@
qed
qed
+lemma (in measure_space) positive_integral_0_iff_AE:
+ assumes u: "u \<in> borel_measurable M"
+ shows "integral\<^isup>P M u = 0 \<longleftrightarrow> (AE x. u x = 0)"
+proof -
+ have sets: "{x\<in>space M. u x \<noteq> 0} \<in> sets M"
+ using u by auto
+ then show ?thesis
+ using positive_integral_0_iff[OF u] AE_iff_null_set[OF sets] by auto
+qed
+
lemma (in measure_space) positive_integral_restricted:
assumes "A \<in> sets M"
shows "integral\<^isup>P (restricted_space A) f = (\<integral>\<^isup>+ x. f x * indicator A x \<partial>M)"
@@ -1585,10 +1585,8 @@
assumes cong: "AE x. f x = g x"
shows "integral\<^isup>L M f = integral\<^isup>L M g"
proof -
- have "AE x. Real (f x) = Real (g x)"
- using cong by (rule AE_mp) simp
- moreover have "AE x. Real (- f x) = Real (- g x)"
- using cong by (rule AE_mp) simp
+ have "AE x. Real (f x) = Real (g x)" using cong by auto
+ moreover have "AE x. Real (- f x) = Real (- g x)" using cong by auto
ultimately show ?thesis
by (simp cong: positive_integral_cong_AE add: lebesgue_integral_def)
qed
@@ -1756,20 +1754,18 @@
shows "integral\<^isup>L M f \<le> integral\<^isup>L M g"
proof -
have "AE x. Real (f x) \<le> Real (g x)"
- using mono by (rule AE_mp) (auto intro!: AE_cong)
+ using mono by auto
moreover have "AE x. Real (- g x) \<le> Real (- f x)"
- using mono by (rule AE_mp) (auto intro!: AE_cong)
+ using mono by auto
ultimately show ?thesis using fg
by (auto simp: lebesgue_integral_def integrable_def diff_minus
intro!: add_mono real_of_pextreal_mono positive_integral_mono_AE)
qed
lemma (in measure_space) integral_mono:
- assumes fg: "integrable M f" "integrable M g"
- and mono: "\<And>t. t \<in> space M \<Longrightarrow> f t \<le> g t"
+ assumes "integrable M f" "integrable M g" "\<And>t. t \<in> space M \<Longrightarrow> f t \<le> g t"
shows "integral\<^isup>L M f \<le> integral\<^isup>L M g"
- apply (rule integral_mono_AE[OF fg])
- using mono by (rule AE_cong) auto
+ using assms by (auto intro: integral_mono_AE)
lemma (in measure_space) integral_diff[simp, intro]:
assumes f: "integrable M f" and g: "integrable M g"
@@ -2056,14 +2052,12 @@
lemma (in measure_space) integral_real:
fixes f :: "'a \<Rightarrow> pextreal"
- assumes "AE x. f x \<noteq> \<omega>"
+ assumes [simp]: "AE x. f x \<noteq> \<omega>"
shows "(\<integral>x. real (f x) \<partial>M) = real (integral\<^isup>P M f)" (is ?plus)
and "(\<integral>x. - real (f x) \<partial>M) = - real (integral\<^isup>P M f)" (is ?minus)
proof -
have "(\<integral>\<^isup>+ x. Real (real (f x)) \<partial>M) = integral\<^isup>P M f"
- apply (rule positive_integral_cong_AE)
- apply (rule AE_mp[OF assms(1)])
- by (auto intro!: AE_cong simp: Real_real)
+ by (auto intro!: positive_integral_cong_AE simp: Real_real)
moreover
have "(\<integral>\<^isup>+ x. Real (- real (f x)) \<partial>M) = (\<integral>\<^isup>+ x. 0 \<partial>M)"
by (intro positive_integral_cong) auto
@@ -2073,7 +2067,7 @@
lemma (in measure_space) integral_dominated_convergence:
assumes u: "\<And>i. integrable M (u i)" and bound: "\<And>x j. x\<in>space M \<Longrightarrow> \<bar>u j x\<bar> \<le> w x"
- and w: "integrable M w" "\<And>x. x \<in> space M \<Longrightarrow> 0 \<le> w x"
+ and w: "integrable M w"
and u': "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. u i x) ----> u' x"
shows "integrable M u'"
and "(\<lambda>i. (\<integral>x. \<bar>u i x - u' x\<bar> \<partial>M)) ----> 0" (is "?lim_diff")
@@ -2089,13 +2083,18 @@
have u'_borel: "u' \<in> borel_measurable M"
using u' by (blast intro: borel_measurable_LIMSEQ[of u])
+ { fix x assume x: "x \<in> space M"
+ then have "0 \<le> \<bar>u 0 x\<bar>" by auto
+ also have "\<dots> \<le> w x" using bound[OF x] by auto
+ finally have "0 \<le> w x" . }
+ note w_pos = this
+
show "integrable M u'"
proof (rule integrable_bound)
show "integrable M w" by fact
show "u' \<in> borel_measurable M" by fact
next
- fix x assume x: "x \<in> space M"
- thus "0 \<le> w x" by fact
+ fix x assume x: "x \<in> space M" then show "0 \<le> w x" by fact
show "\<bar>u' x\<bar> \<le> w x" using u'_bound[OF x] .
qed
@@ -2113,7 +2112,7 @@
have PI_diff: "\<And>m n. (\<integral>\<^isup>+ x. Real (?diff (m + n) x) \<partial>M) =
(\<integral>\<^isup>+ x. Real (2 * w x) \<partial>M) - (\<integral>\<^isup>+ x. Real \<bar>u (m + n) x - u' x\<bar> \<partial>M)"
- using diff w diff_less_2w
+ using diff w diff_less_2w w_pos
by (subst positive_integral_diff[symmetric])
(auto simp: integrable_def intro!: positive_integral_cong)
@@ -2155,7 +2154,7 @@
unfolding PI_diff pextreal_INF_minus[OF I2w_fin] pextreal_SUP_minus ..
finally show ?thesis using neq_0 I2w_fin by (rule pextreal_le_minus_imp_0)
qed
-
+
have [simp]: "\<And>n m x. Real (- \<bar>u (m + n) x - u' x\<bar>) = 0" by auto
have [simp]: "\<And>n m. (\<integral>\<^isup>+ x. Real \<bar>u (m + n) x - u' x\<bar> \<partial>M) =
@@ -2230,13 +2229,11 @@
show "(\<lambda>i. integral\<^isup>L M (?w' i)) ----> x" unfolding * sums_def .
qed
- have 4: "\<And>x. x \<in> space M \<Longrightarrow> 0 \<le> ?w x" using 2[of _ 0] by simp
-
from summable[THEN summable_rabs_cancel]
- have 5: "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>n. \<Sum>i = 0..<n. f i x) ----> (\<Sum>i. f i x)"
+ have 4: "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>n. \<Sum>i = 0..<n. f i x) ----> (\<Sum>i. f i x)"
by (auto intro: summable_sumr_LIMSEQ_suminf)
- note int = integral_dominated_convergence(1,3)[OF 1 2 3 4 5]
+ note int = integral_dominated_convergence(1,3)[OF 1 2 3 4]
from int show "integrable M ?S" by simp
--- a/src/HOL/Probability/Measure.thy Fri Feb 04 14:16:48 2011 +0100
+++ b/src/HOL/Probability/Measure.thy Fri Feb 04 14:16:55 2011 +0100
@@ -739,12 +739,25 @@
obtains N where "{x \<in> space M. \<not> P x} \<subseteq> N" "\<mu> N = 0" "N \<in> sets M"
using assms unfolding almost_everywhere_def by auto
+lemma (in measure_space) AE_E2:
+ assumes "AE x. P x" "{x\<in>space M. P x} \<in> sets M"
+ shows "\<mu> {x\<in>space M. \<not> P x} = 0" (is "\<mu> ?P = 0")
+proof -
+ obtain A where A: "?P \<subseteq> A" "A \<in> sets M" "\<mu> A = 0"
+ using assms by (auto elim!: AE_E)
+ have "?P = space M - {x\<in>space M. P x}" by auto
+ then have "?P \<in> sets M" using assms by auto
+ with assms `?P \<subseteq> A` `A \<in> sets M` have "\<mu> ?P \<le> \<mu> A"
+ by (auto intro!: measure_mono)
+ then show "\<mu> ?P = 0" using A by simp
+qed
+
lemma (in measure_space) AE_I:
assumes "{x \<in> space M. \<not> P x} \<subseteq> N" "\<mu> N = 0" "N \<in> sets M"
shows "AE x. P x"
using assms unfolding almost_everywhere_def by auto
-lemma (in measure_space) AE_mp:
+lemma (in measure_space) AE_mp[elim!]:
assumes AE_P: "AE x. P x" and AE_imp: "AE x. P x \<longrightarrow> Q x"
shows "AE x. Q x"
proof -
@@ -765,56 +778,28 @@
qed
qed
-lemma (in measure_space) AE_iffI:
- assumes P: "AE x. P x" and Q: "AE x. P x \<longleftrightarrow> Q x" shows "AE x. Q x"
- using AE_mp[OF Q, of "\<lambda>x. P x \<longrightarrow> Q x"] AE_mp[OF P, of Q] by auto
-
-lemma (in measure_space) AE_disjI1:
- assumes P: "AE x. P x" shows "AE x. P x \<or> Q x"
- by (rule AE_mp[OF P]) auto
-
-lemma (in measure_space) AE_disjI2:
- assumes P: "AE x. Q x" shows "AE x. P x \<or> Q x"
- by (rule AE_mp[OF P]) auto
-
-lemma (in measure_space) AE_conjI:
- assumes AE_P: "AE x. P x" and AE_Q: "AE x. Q x"
- shows "AE x. P x \<and> Q x"
- apply (rule AE_mp[OF AE_P])
- apply (rule AE_mp[OF AE_Q])
- by simp
+lemma (in measure_space)
+ shows AE_iffI: "AE x. P x \<Longrightarrow> AE x. P x \<longleftrightarrow> Q x \<Longrightarrow> AE x. Q x"
+ and AE_disjI1: "AE x. P x \<Longrightarrow> AE x. P x \<or> Q x"
+ and AE_disjI2: "AE x. Q x \<Longrightarrow> AE x. P x \<or> Q x"
+ and AE_conjI: "AE x. P x \<Longrightarrow> AE x. Q x \<Longrightarrow> AE x. P x \<and> Q x"
+ and AE_conj_iff[simp]: "(AE x. P x \<and> Q x) \<longleftrightarrow> (AE x. P x) \<and> (AE x. Q x)"
+ by auto
-lemma (in measure_space) AE_conj_iff[simp]:
- shows "(AE x. P x \<and> Q x) \<longleftrightarrow> (AE x. P x) \<and> (AE x. Q x)"
-proof (intro conjI iffI AE_conjI)
- assume *: "AE x. P x \<and> Q x"
- from * show "AE x. P x" by (rule AE_mp) auto
- from * show "AE x. Q x" by (rule AE_mp) auto
-qed auto
-
-lemma (in measure_space) AE_E2:
- assumes "AE x. P x" "{x\<in>space M. P x} \<in> sets M"
- shows "\<mu> {x\<in>space M. \<not> P x} = 0" (is "\<mu> ?P = 0")
-proof -
- obtain A where A: "?P \<subseteq> A" "A \<in> sets M" "\<mu> A = 0"
- using assms by (auto elim!: AE_E)
- have "?P = space M - {x\<in>space M. P x}" by auto
- then have "?P \<in> sets M" using assms by auto
- with assms `?P \<subseteq> A` `A \<in> sets M` have "\<mu> ?P \<le> \<mu> A"
- by (auto intro!: measure_mono)
- then show "\<mu> ?P = 0" using A by simp
-qed
-
-lemma (in measure_space) AE_space[simp, intro]: "AE x. x \<in> space M"
+lemma (in measure_space) AE_space: "AE x. x \<in> space M"
by (rule AE_I[where N="{}"]) auto
-lemma (in measure_space) AE_cong:
- assumes "\<And>x. x \<in> space M \<Longrightarrow> P x" shows "AE x. P x"
-proof -
- have [simp]: "\<And>x. (x \<in> space M \<longrightarrow> P x) \<longleftrightarrow> True" using assms by auto
- show ?thesis
- by (rule AE_mp[OF AE_space]) auto
-qed
+lemma (in measure_space) AE_I2[simp, intro]:
+ "(\<And>x. x \<in> space M \<Longrightarrow> P x) \<Longrightarrow> AE x. P x"
+ using AE_space by auto
+
+lemma (in measure_space) AE_Ball_mp:
+ "\<forall>x\<in>space M. P x \<Longrightarrow> AE x. P x \<longrightarrow> Q x \<Longrightarrow> AE x. Q x"
+ by auto
+
+lemma (in measure_space) AE_cong[cong]:
+ "(\<And>x. x \<in> space M \<Longrightarrow> P x \<longleftrightarrow> Q x) \<Longrightarrow> (AE x. P x) \<longleftrightarrow> (AE x. Q x)"
+ by auto
lemma (in measure_space) all_AE_countable:
"(\<forall>i::'i::countable. AE x. P i x) \<longleftrightarrow> (AE x. \<forall>i. P i x)"
@@ -829,11 +814,7 @@
by (intro null_sets_UN) auto
ultimately show "AE x. \<forall>i. P i x"
unfolding almost_everywhere_def by auto
-next
- assume *: "AE x. \<forall>i. P i x"
- show "\<forall>i. AE x. P i x"
- by (rule allI, rule AE_mp[OF *]) simp
-qed
+qed auto
lemma (in measure_space) restricted_measure_space:
assumes "S \<in> sets M"
--- a/src/HOL/Probability/Product_Measure.thy Fri Feb 04 14:16:48 2011 +0100
+++ b/src/HOL/Probability/Product_Measure.thy Fri Feb 04 14:16:55 2011 +0100
@@ -1061,46 +1061,28 @@
have AE: "M1.almost_everywhere (\<lambda>x. (\<integral>\<^isup>+y. Real (f (x, y)) \<partial>M2) \<noteq> \<omega>)"
"M1.almost_everywhere (\<lambda>x. (\<integral>\<^isup>+y. Real (- f (x, y)) \<partial>M2) \<noteq> \<omega>)"
by (auto intro!: M1.positive_integral_omega_AE)
- then show ?AE
- apply (rule M1.AE_mp[OF _ M1.AE_mp])
- apply (rule M1.AE_cong)
- using assms unfolding integrable_def
- by (auto intro!: measurable_pair_image_snd)
- have "integrable M1 (\<lambda>x. real (\<integral>\<^isup>+y. Real (f (x, y)) \<partial>M2))" (is "integrable M1 ?f")
- proof (intro integrable_def[THEN iffD2] conjI)
- show "?f \<in> borel_measurable M1"
- using borel by (auto intro!: M1.borel_measurable_real positive_integral_fst_measurable)
- have "(\<integral>\<^isup>+x. Real (?f x) \<partial>M1) = (\<integral>\<^isup>+x. (\<integral>\<^isup>+y. Real (f (x, y)) \<partial>M2) \<partial>M1)"
- apply (rule M1.positive_integral_cong_AE)
- apply (rule M1.AE_mp[OF AE(1)])
- apply (rule M1.AE_cong)
- by (auto simp: Real_real)
- then show "(\<integral>\<^isup>+x. Real (?f x) \<partial>M1) \<noteq> \<omega>"
- using positive_integral_fst_measurable[OF borel(2)] int by simp
- have "(\<integral>\<^isup>+x. Real (- ?f x) \<partial>M1) = (\<integral>\<^isup>+x. 0 \<partial>M1)"
- by (intro M1.positive_integral_cong) simp
- then show "(\<integral>\<^isup>+x. Real (- ?f x) \<partial>M1) \<noteq> \<omega>" by simp
- qed
- moreover have "integrable M1 (\<lambda>x. real (\<integral>\<^isup>+ y. Real (- f (x, y)) \<partial>M2))"
- (is "integrable M1 ?f")
- proof (intro integrable_def[THEN iffD2] conjI)
- show "?f \<in> borel_measurable M1"
- using borel by (auto intro!: M1.borel_measurable_real positive_integral_fst_measurable)
- have "(\<integral>\<^isup>+x. Real (?f x) \<partial>M1) = (\<integral>\<^isup>+x. (\<integral>\<^isup>+y. Real (- f (x, y)) \<partial>M2) \<partial>M1)"
- apply (rule M1.positive_integral_cong_AE)
- apply (rule M1.AE_mp[OF AE(2)])
- apply (rule M1.AE_cong)
- by (auto simp: Real_real)
- then show "(\<integral>\<^isup>+x. Real (?f x) \<partial>M1) \<noteq> \<omega>"
- using positive_integral_fst_measurable[OF borel(1)] int by simp
- have "(\<integral>\<^isup>+x. Real (- ?f x) \<partial>M1) = (\<integral>\<^isup>+x. 0 \<partial>M1)"
- by (intro M1.positive_integral_cong) simp
- then show "(\<integral>\<^isup>+x. Real (- ?f x) \<partial>M1) \<noteq> \<omega>" by simp
- qed
- ultimately show ?INT
+ then show ?AE using assms
+ by (simp add: measurable_pair_image_snd integrable_def)
+ { fix f assume borel: "(\<lambda>x. Real (f x)) \<in> borel_measurable P"
+ and int: "integral\<^isup>P P (\<lambda>x. Real (f x)) \<noteq> \<omega>"
+ and AE: "M1.almost_everywhere (\<lambda>x. (\<integral>\<^isup>+y. Real (f (x, y)) \<partial>M2) \<noteq> \<omega>)"
+ have "integrable M1 (\<lambda>x. real (\<integral>\<^isup>+y. Real (f (x, y)) \<partial>M2))" (is "integrable M1 ?f")
+ proof (intro integrable_def[THEN iffD2] conjI)
+ show "?f \<in> borel_measurable M1"
+ using borel by (auto intro!: M1.borel_measurable_real positive_integral_fst_measurable)
+ have "(\<integral>\<^isup>+x. Real (?f x) \<partial>M1) = (\<integral>\<^isup>+x. (\<integral>\<^isup>+y. Real (f (x, y)) \<partial>M2) \<partial>M1)"
+ using AE by (auto intro!: M1.positive_integral_cong_AE simp: Real_real)
+ then show "(\<integral>\<^isup>+x. Real (?f x) \<partial>M1) \<noteq> \<omega>"
+ using positive_integral_fst_measurable[OF borel] int by simp
+ have "(\<integral>\<^isup>+x. Real (- ?f x) \<partial>M1) = (\<integral>\<^isup>+x. 0 \<partial>M1)"
+ by (intro M1.positive_integral_cong) simp
+ then show "(\<integral>\<^isup>+x. Real (- ?f x) \<partial>M1) \<noteq> \<omega>" by simp
+ qed }
+ from this[OF borel(1) int(1) AE(2)] this[OF borel(2) int(2) AE(1)]
+ show ?INT
unfolding lebesgue_integral_def[of P] lebesgue_integral_def[of M2]
borel[THEN positive_integral_fst_measurable(2), symmetric]
- by (simp add: M1.integral_real[OF AE(1)] M1.integral_real[OF AE(2)])
+ using AE by (simp add: M1.integral_real)
qed
lemma (in pair_sigma_finite) integrable_snd_measurable:
--- a/src/HOL/Probability/Radon_Nikodym.thy Fri Feb 04 14:16:48 2011 +0100
+++ b/src/HOL/Probability/Radon_Nikodym.thy Fri Feb 04 14:16:55 2011 +0100
@@ -817,8 +817,8 @@
(is "(\<forall>A\<in>sets M. ?P f A = ?P g A) \<longleftrightarrow> _")
proof (intro iffI ballI)
fix A assume eq: "AE x. f x = g x"
- show "?P f A = ?P g A"
- by (rule positive_integral_cong_AE[OF AE_mp[OF eq]]) simp
+ then show "?P f A = ?P g A"
+ by (auto intro: positive_integral_cong_AE)
next
assume eq: "\<forall>A\<in>sets M. ?P f A = ?P g A"
from this[THEN bspec, OF top] fin
@@ -879,11 +879,10 @@
have "?N \<in> sets M" using borel by auto
have *: "\<And>i x A. \<And>y::pextreal. y * indicator (Q i) x * indicator A x = y * indicator (Q i \<inter> A) x"
unfolding indicator_def by auto
- have 1: "\<forall>i. AE x. ?f (Q i) x = ?f' (Q i) x"
- using borel Q_fin Q
+ have "\<forall>i. AE x. ?f (Q i) x = ?f' (Q i) x" using borel Q_fin Q
by (intro finite_density_unique[THEN iffD1] allI)
(auto intro!: borel_measurable_pextreal_times f Int simp: *)
- have 2: "AE x. ?f Q0 x = ?f' Q0 x"
+ moreover have "AE x. ?f Q0 x = ?f' Q0 x"
proof (rule AE_I')
{ fix f :: "'a \<Rightarrow> pextreal" assume borel: "f \<in> borel_measurable M"
and eq: "\<And>A. A \<in> sets M \<Longrightarrow> ?\<nu> A = (\<integral>\<^isup>+x. f x * indicator A x \<partial>M)"
@@ -911,13 +910,12 @@
show "{x \<in> space M. ?f Q0 x \<noteq> ?f' Q0 x} \<subseteq>
(Q0 \<inter> {x\<in>space M. f x \<noteq> \<omega>}) \<union> (Q0 \<inter> {x\<in>space M. f' x \<noteq> \<omega>})" by (auto simp: indicator_def)
qed
- have **: "\<And>x. (?f Q0 x = ?f' Q0 x) \<longrightarrow> (\<forall>i. ?f (Q i) x = ?f' (Q i) x) \<longrightarrow>
+ moreover have "\<And>x. (?f Q0 x = ?f' Q0 x) \<longrightarrow> (\<forall>i. ?f (Q i) x = ?f' (Q i) x) \<longrightarrow>
?f (space M) x = ?f' (space M) x"
by (auto simp: indicator_def Q0)
- have 3: "AE x. ?f (space M) x = ?f' (space M) x"
- by (rule AE_mp[OF 1[unfolded all_AE_countable] AE_mp[OF 2]]) (simp add: **)
- then show "AE x. f x = f' x"
- by (rule AE_mp) (auto intro!: AE_cong simp: indicator_def)
+ ultimately have "AE x. ?f (space M) x = ?f' (space M) x"
+ by (auto simp: all_AE_countable)
+ then show "AE x. f x = f' x" by auto
qed
lemma (in sigma_finite_measure) density_unique:
@@ -978,25 +976,20 @@
and "sets ?N = sets M" and "space ?N = space M" by (auto simp: measurable_def)
from \<nu>.Ex_finite_integrable_function obtain h where
h: "h \<in> borel_measurable M" "integral\<^isup>P ?N h \<noteq> \<omega>"
- and fin: "\<And>x. x \<in> space M \<Longrightarrow> 0 < h x \<and> h x < \<omega>" by auto
+ and fin: "\<forall>x\<in>space M. 0 < h x \<and> h x < \<omega>" by auto
have "AE x. f x * h x \<noteq> \<omega>"
proof (rule AE_I')
- have "integral\<^isup>P ?N h = (\<integral>\<^isup>+x. f x * h x \<partial>M)"
- apply (subst \<nu>.positive_integral_cong_measure[symmetric,
- of "M\<lparr> measure := \<lambda> A. \<integral>\<^isup>+x. f x * indicator A x \<partial>M \<rparr>"])
- apply (simp_all add: eq)
- apply (rule positive_integral_translated_density)
- using f h by auto
+ have "integral\<^isup>P ?N h = (\<integral>\<^isup>+x. f x * h x \<partial>M)" using f h
+ by (subst \<nu>.positive_integral_cong_measure[symmetric,
+ of "M\<lparr> measure := \<lambda> A. \<integral>\<^isup>+x. f x * indicator A x \<partial>M \<rparr>"])
+ (auto intro!: positive_integral_translated_density simp: eq)
then have "(\<integral>\<^isup>+x. f x * h x \<partial>M) \<noteq> \<omega>"
using h(2) by simp
then show "(\<lambda>x. f x * h x) -` {\<omega>} \<inter> space M \<in> null_sets"
using f h(1) by (auto intro!: positive_integral_omega borel_measurable_vimage)
qed auto
then show "AE x. f x \<noteq> \<omega>"
- proof (rule AE_mp, intro AE_cong)
- fix x assume "x \<in> space M" from this[THEN fin]
- show "f x * h x \<noteq> \<omega> \<longrightarrow> f x \<noteq> \<omega>" by auto
- qed
+ using fin by (auto elim!: AE_Ball_mp)
next
assume AE: "AE x. f x \<noteq> \<omega>"
from sigma_finite guess Q .. note Q = this
@@ -1043,16 +1036,8 @@
proof (cases i)
case 0
have "AE x. f x * indicator (A i \<inter> Q j) x = 0"
- using AE by (rule AE_mp) (auto intro!: AE_cong simp: A_def `i = 0`)
- then have "(\<integral>\<^isup>+x. f x * indicator (A i \<inter> Q j) x \<partial>M) = 0"
- using A_in_sets f
- apply (subst positive_integral_0_iff)
- apply fast
- apply (subst (asm) AE_iff_null_set)
- apply (intro borel_measurable_pextreal_neq_const)
- apply fast
- by simp
- then show ?thesis by simp
+ using AE by (auto simp: A_def `i = 0`)
+ from positive_integral_cong_AE[OF this] show ?thesis by simp
next
case (Suc n)
then have "(\<integral>\<^isup>+x. f x * indicator (A i \<inter> Q j) x \<partial>M) \<le>
@@ -1157,11 +1142,8 @@
by (simp add: mult_le_0_iff)
then have "RN_deriv M \<nu> x * Real (f x) = Real (real (RN_deriv M \<nu> x) * f x)"
using * by (simp add: Real_real) }
- note * = this
- have "(\<integral>\<^isup>+x. RN_deriv M \<nu> x * Real (f x) \<partial>M) = (\<integral>\<^isup>+x. Real (real (RN_deriv M \<nu> x) * f x) \<partial>M)"
- apply (rule positive_integral_cong_AE)
- apply (rule AE_mp[OF RN_deriv_finite[OF \<nu>]])
- by (auto intro!: AE_cong simp: *) }
+ then have "(\<integral>\<^isup>+x. RN_deriv M \<nu> x * Real (f x) \<partial>M) = (\<integral>\<^isup>+x. Real (real (RN_deriv M \<nu> x) * f x) \<partial>M)"
+ using RN_deriv_finite[OF \<nu>] by (auto intro: positive_integral_cong_AE) }
with this this f f' Nf
show ?integral ?integrable
unfolding lebesgue_integral_def integrable_def