--- a/NEWS Mon May 19 15:23:08 2014 +0200
+++ b/NEWS Mon May 19 16:14:08 2014 +0200
@@ -733,6 +733,13 @@
integral_cmul_indicator
integral_real
+ - Renamed positive_integral to nn_integral:
+
+ * Renamed all lemmas "*positive_integral*" to *nn_integral*"
+ positive_integral_positive ~> nn_integral_nonneg
+
+ * Renamed abbreviation integral\<^sup>P to integral\<^sup>N.
+
*** Scala ***
* The signature and semantics of Document.Snapshot.cumulate_markup /
--- a/src/HOL/Probability/Binary_Product_Measure.thy Mon May 19 15:23:08 2014 +0200
+++ b/src/HOL/Probability/Binary_Product_Measure.thy Mon May 19 16:14:08 2014 +0200
@@ -239,7 +239,7 @@
shows "emeasure (N \<Otimes>\<^sub>M M) X = (\<integral>\<^sup>+ x. \<integral>\<^sup>+ y. indicator X (x, y) \<partial>M \<partial>N)" (is "_ = ?\<mu> X")
proof (rule emeasure_measure_of[OF pair_measure_def])
show "positive (sets (N \<Otimes>\<^sub>M M)) ?\<mu>"
- by (auto simp: positive_def positive_integral_positive)
+ by (auto simp: positive_def nn_integral_nonneg)
have eq[simp]: "\<And>A x y. indicator A (x, y) = indicator (Pair x -` A) y"
by (auto simp: indicator_def)
show "countably_additive (sets (N \<Otimes>\<^sub>M M)) ?\<mu>"
@@ -253,8 +253,8 @@
moreover have "\<And>x. range (\<lambda>i. Pair x -` F i) \<subseteq> sets M"
using F by (auto simp: sets_Pair1)
ultimately show "(\<Sum>n. ?\<mu> (F n)) = ?\<mu> (\<Union>i. F i)"
- by (auto simp add: vimage_UN positive_integral_suminf[symmetric] suminf_emeasure subset_eq emeasure_nonneg sets_Pair1
- intro!: positive_integral_cong positive_integral_indicator[symmetric])
+ by (auto simp add: vimage_UN nn_integral_suminf[symmetric] suminf_emeasure subset_eq emeasure_nonneg sets_Pair1
+ intro!: nn_integral_cong nn_integral_indicator[symmetric])
qed
show "{a \<times> b |a b. a \<in> sets N \<and> b \<in> sets M} \<subseteq> Pow (space N \<times> space M)"
using sets.space_closed[of N] sets.space_closed[of M] by auto
@@ -267,7 +267,7 @@
have [simp]: "\<And>x y. indicator X (x, y) = indicator (Pair x -` X) y"
by (auto simp: indicator_def)
show ?thesis
- using X by (auto intro!: positive_integral_cong simp: emeasure_pair_measure sets_Pair1)
+ using X by (auto intro!: nn_integral_cong simp: emeasure_pair_measure sets_Pair1)
qed
lemma (in sigma_finite_measure) emeasure_pair_measure_Times:
@@ -275,9 +275,9 @@
shows "emeasure (N \<Otimes>\<^sub>M M) (A \<times> B) = emeasure N A * emeasure M B"
proof -
have "emeasure (N \<Otimes>\<^sub>M M) (A \<times> B) = (\<integral>\<^sup>+x. emeasure M B * indicator A x \<partial>N)"
- using A B by (auto intro!: positive_integral_cong simp: emeasure_pair_measure_alt)
+ using A B by (auto intro!: nn_integral_cong simp: emeasure_pair_measure_alt)
also have "\<dots> = emeasure M B * emeasure N A"
- using A by (simp add: emeasure_nonneg positive_integral_cmult_indicator)
+ using A by (simp add: emeasure_nonneg nn_integral_cmult_indicator)
finally show ?thesis
by (simp add: ac_simps)
qed
@@ -418,7 +418,7 @@
proof (rule AE_I)
from N measurable_emeasure_Pair1[OF `N \<in> sets (M1 \<Otimes>\<^sub>M M2)`]
show "emeasure M1 {x\<in>space M1. emeasure M2 (Pair x -` N) \<noteq> 0} = 0"
- by (auto simp: M2.emeasure_pair_measure_alt positive_integral_0_iff emeasure_nonneg)
+ by (auto simp: M2.emeasure_pair_measure_alt nn_integral_0_iff emeasure_nonneg)
show "{x \<in> space M1. emeasure M2 (Pair x -` N) \<noteq> 0} \<in> sets M1"
by (intro borel_measurable_ereal_neq_const measurable_emeasure_Pair1 N)
{ fix x assume "x \<in> space M1" "emeasure M2 (Pair x -` N) = 0"
@@ -446,9 +446,9 @@
by (simp add: M2.emeasure_pair_measure)
also have "\<dots> = (\<integral>\<^sup>+ x. \<integral>\<^sup>+ y. 0 \<partial>M2 \<partial>M1)"
using ae
- apply (safe intro!: positive_integral_cong_AE)
+ apply (safe intro!: nn_integral_cong_AE)
apply (intro AE_I2)
- apply (safe intro!: positive_integral_cong_AE)
+ apply (safe intro!: nn_integral_cong_AE)
apply auto
done
finally show "emeasure (M1 \<Otimes>\<^sub>M M2) {x \<in> space (M1 \<Otimes>\<^sub>M M2). \<not> P x} = 0" by simp
@@ -486,7 +486,7 @@
"x \<in> space M1 \<Longrightarrow> g \<in> measurable (M1 \<Otimes>\<^sub>M M2) L \<Longrightarrow> (\<lambda>y. g (x, y)) \<in> measurable M2 L"
by simp
-lemma (in sigma_finite_measure) borel_measurable_positive_integral_fst':
+lemma (in sigma_finite_measure) borel_measurable_nn_integral_fst':
assumes f: "f \<in> borel_measurable (M1 \<Otimes>\<^sub>M M)" "\<And>x. 0 \<le> f x"
shows "(\<lambda>x. \<integral>\<^sup>+ y. f (x, y) \<partial>M) \<in> borel_measurable M1"
using f proof induct
@@ -495,7 +495,7 @@
by (auto simp: space_pair_measure)
show ?case
apply (subst measurable_cong)
- apply (rule positive_integral_cong)
+ apply (rule nn_integral_cong)
apply fact+
done
next
@@ -506,56 +506,56 @@
by (simp add: sets_Pair1[OF set])
from this measurable_emeasure_Pair[OF set] show ?case
by (rule measurable_cong[THEN iffD1])
-qed (simp_all add: positive_integral_add positive_integral_cmult measurable_compose_Pair1
- positive_integral_monotone_convergence_SUP incseq_def le_fun_def
+qed (simp_all add: nn_integral_add nn_integral_cmult measurable_compose_Pair1
+ nn_integral_monotone_convergence_SUP incseq_def le_fun_def
cong: measurable_cong)
-lemma (in sigma_finite_measure) positive_integral_fst':
+lemma (in sigma_finite_measure) nn_integral_fst':
assumes f: "f \<in> borel_measurable (M1 \<Otimes>\<^sub>M M)" "\<And>x. 0 \<le> f x"
- shows "(\<integral>\<^sup>+ x. \<integral>\<^sup>+ y. f (x, y) \<partial>M \<partial>M1) = integral\<^sup>P (M1 \<Otimes>\<^sub>M M) f" (is "?I f = _")
+ shows "(\<integral>\<^sup>+ x. \<integral>\<^sup>+ y. f (x, y) \<partial>M \<partial>M1) = integral\<^sup>N (M1 \<Otimes>\<^sub>M M) f" (is "?I f = _")
using f proof induct
case (cong u v)
then have "?I u = ?I v"
- by (intro positive_integral_cong) (auto simp: space_pair_measure)
+ by (intro nn_integral_cong) (auto simp: space_pair_measure)
with cong show ?case
- by (simp cong: positive_integral_cong)
-qed (simp_all add: emeasure_pair_measure positive_integral_cmult positive_integral_add
- positive_integral_monotone_convergence_SUP
- measurable_compose_Pair1 positive_integral_positive
- borel_measurable_positive_integral_fst' positive_integral_mono incseq_def le_fun_def
- cong: positive_integral_cong)
+ by (simp cong: nn_integral_cong)
+qed (simp_all add: emeasure_pair_measure nn_integral_cmult nn_integral_add
+ nn_integral_monotone_convergence_SUP
+ measurable_compose_Pair1 nn_integral_nonneg
+ borel_measurable_nn_integral_fst' nn_integral_mono incseq_def le_fun_def
+ cong: nn_integral_cong)
-lemma (in sigma_finite_measure) positive_integral_fst:
+lemma (in sigma_finite_measure) nn_integral_fst:
assumes f: "f \<in> borel_measurable (M1 \<Otimes>\<^sub>M M)"
- shows "(\<integral>\<^sup>+ x. (\<integral>\<^sup>+ y. f (x, y) \<partial>M) \<partial>M1) = integral\<^sup>P (M1 \<Otimes>\<^sub>M M) f"
+ shows "(\<integral>\<^sup>+ x. (\<integral>\<^sup>+ y. f (x, y) \<partial>M) \<partial>M1) = integral\<^sup>N (M1 \<Otimes>\<^sub>M M) f"
using f
- borel_measurable_positive_integral_fst'[of "\<lambda>x. max 0 (f x)"]
- positive_integral_fst'[of "\<lambda>x. max 0 (f x)"]
- unfolding positive_integral_max_0 by auto
+ borel_measurable_nn_integral_fst'[of "\<lambda>x. max 0 (f x)"]
+ nn_integral_fst'[of "\<lambda>x. max 0 (f x)"]
+ unfolding nn_integral_max_0 by auto
-lemma (in sigma_finite_measure) borel_measurable_positive_integral[measurable (raw)]:
+lemma (in sigma_finite_measure) borel_measurable_nn_integral[measurable (raw)]:
"split f \<in> borel_measurable (N \<Otimes>\<^sub>M M) \<Longrightarrow> (\<lambda>x. \<integral>\<^sup>+ y. f x y \<partial>M) \<in> borel_measurable N"
- using borel_measurable_positive_integral_fst'[of "\<lambda>x. max 0 (split f x)" N]
- by (simp add: positive_integral_max_0)
+ using borel_measurable_nn_integral_fst'[of "\<lambda>x. max 0 (split f x)" N]
+ by (simp add: nn_integral_max_0)
-lemma (in pair_sigma_finite) positive_integral_snd:
+lemma (in pair_sigma_finite) nn_integral_snd:
assumes f: "f \<in> borel_measurable (M1 \<Otimes>\<^sub>M M2)"
- shows "(\<integral>\<^sup>+ y. (\<integral>\<^sup>+ x. f (x, y) \<partial>M1) \<partial>M2) = integral\<^sup>P (M1 \<Otimes>\<^sub>M M2) f"
+ shows "(\<integral>\<^sup>+ y. (\<integral>\<^sup>+ x. f (x, y) \<partial>M1) \<partial>M2) = integral\<^sup>N (M1 \<Otimes>\<^sub>M M2) f"
proof -
note measurable_pair_swap[OF f]
- from M1.positive_integral_fst[OF this]
+ from M1.nn_integral_fst[OF this]
have "(\<integral>\<^sup>+ y. (\<integral>\<^sup>+ x. f (x, y) \<partial>M1) \<partial>M2) = (\<integral>\<^sup>+ (x, y). f (y, x) \<partial>(M2 \<Otimes>\<^sub>M M1))"
by simp
- also have "(\<integral>\<^sup>+ (x, y). f (y, x) \<partial>(M2 \<Otimes>\<^sub>M M1)) = integral\<^sup>P (M1 \<Otimes>\<^sub>M M2) f"
+ also have "(\<integral>\<^sup>+ (x, y). f (y, x) \<partial>(M2 \<Otimes>\<^sub>M M1)) = integral\<^sup>N (M1 \<Otimes>\<^sub>M M2) f"
by (subst distr_pair_swap)
- (auto simp: positive_integral_distr[OF measurable_pair_swap' f] intro!: positive_integral_cong)
+ (auto simp: nn_integral_distr[OF measurable_pair_swap' f] intro!: nn_integral_cong)
finally show ?thesis .
qed
lemma (in pair_sigma_finite) Fubini:
assumes f: "f \<in> borel_measurable (M1 \<Otimes>\<^sub>M M2)"
shows "(\<integral>\<^sup>+ y. (\<integral>\<^sup>+ x. f (x, y) \<partial>M1) \<partial>M2) = (\<integral>\<^sup>+ x. (\<integral>\<^sup>+ y. f (x, y) \<partial>M2) \<partial>M1)"
- unfolding positive_integral_snd[OF assms] M2.positive_integral_fst[OF assms] ..
+ unfolding nn_integral_snd[OF assms] M2.nn_integral_fst[OF assms] ..
subsection {* Products on counting spaces, densities and distributions *}
@@ -602,7 +602,7 @@
apply (subst emeasure_count_space)
using X_subset apply auto []
apply (simp add: fin_Pair emeasure_count_space X_subset fin_X)
- apply (subst positive_integral_count_space)
+ apply (subst nn_integral_count_space)
using A apply simp
apply (simp del: real_of_nat_setsum add: real_of_nat_setsum[symmetric])
apply (subst card_gt_0_iff)
@@ -626,12 +626,12 @@
fix A assume A: "A \<in> sets ?L"
with f g have "(\<integral>\<^sup>+ x. f x * \<integral>\<^sup>+ y. g y * indicator A (x, y) \<partial>M2 \<partial>M1) =
(\<integral>\<^sup>+ x. \<integral>\<^sup>+ y. f x * g y * indicator A (x, y) \<partial>M2 \<partial>M1)"
- by (intro positive_integral_cong_AE)
- (auto simp add: positive_integral_cmult[symmetric] ac_simps)
+ by (intro nn_integral_cong_AE)
+ (auto simp add: nn_integral_cmult[symmetric] ac_simps)
with A f g show "emeasure ?L A = emeasure ?R A"
- by (simp add: D2.emeasure_pair_measure emeasure_density positive_integral_density
- M2.positive_integral_fst[symmetric]
- cong: positive_integral_cong)
+ by (simp add: D2.emeasure_pair_measure emeasure_density nn_integral_density
+ M2.nn_integral_fst[symmetric]
+ cong: nn_integral_cong)
qed simp
lemma sigma_finite_measure_distr:
@@ -662,8 +662,8 @@
fix A assume A: "A \<in> sets ?P"
with f g show "emeasure ?P A = emeasure ?D A"
by (auto simp add: N.emeasure_pair_measure_alt space_pair_measure emeasure_distr
- T.emeasure_pair_measure_alt positive_integral_distr
- intro!: positive_integral_cong arg_cong[where f="emeasure N"])
+ T.emeasure_pair_measure_alt nn_integral_distr
+ intro!: nn_integral_cong arg_cong[where f="emeasure N"])
qed simp
lemma pair_measure_eqI:
--- a/src/HOL/Probability/Bochner_Integration.thy Mon May 19 15:23:08 2014 +0200
+++ b/src/HOL/Probability/Bochner_Integration.thy Mon May 19 16:14:08 2014 +0200
@@ -284,10 +284,10 @@
from m have "m * emeasure M {x\<in>space M. 0 \<noteq> f x} =
(\<integral>\<^sup>+x. m * indicator {x\<in>space M. 0 \<noteq> f x} x \<partial>M)"
- using f by (intro positive_integral_cmult_indicator[symmetric]) auto
+ using f by (intro nn_integral_cmult_indicator[symmetric]) auto
also have "\<dots> \<le> (\<integral>\<^sup>+x. f x \<partial>M)"
using AE_space
- proof (intro positive_integral_mono_AE, eventually_elim)
+ proof (intro nn_integral_mono_AE, eventually_elim)
fix x assume "x \<in> space M"
with nn show "m * indicator {x \<in> space M. 0 \<noteq> f x} x \<le> f x"
using f by (auto split: split_indicator simp: simple_function_def m_def)
@@ -447,7 +447,7 @@
finally show ?thesis .
qed
-lemma simple_bochner_integral_eq_positive_integral:
+lemma simple_bochner_integral_eq_nn_integral:
assumes f: "simple_bochner_integrable M f" "\<And>x. 0 \<le> f x"
shows "simple_bochner_integral M f = (\<integral>\<^sup>+x. f x \<partial>M)"
proof -
@@ -479,7 +479,7 @@
simp del: setsum_ereal times_ereal.simps(1))
also have "\<dots> = (\<integral>\<^sup>+x. f x \<partial>M)"
using f
- by (intro positive_integral_eq_simple_integral[symmetric])
+ by (intro nn_integral_eq_simple_integral[symmetric])
(auto simp: simple_function_compose1 simple_bochner_integrable.simps)
finally show ?thesis .
qed
@@ -502,13 +502,13 @@
by (auto intro!: simple_bochner_integral_norm_bound)
also have "\<dots> = (\<integral>\<^sup>+x. norm (s x - t x) \<partial>M)"
using simple_bochner_integrable_compose2[of "\<lambda>x y. norm (x - y)" M "s" "t"] s t
- by (auto intro!: simple_bochner_integral_eq_positive_integral)
+ by (auto intro!: simple_bochner_integral_eq_nn_integral)
also have "\<dots> \<le> (\<integral>\<^sup>+x. ereal (norm (f x - s x)) + ereal (norm (f x - t x)) \<partial>M)"
- by (auto intro!: positive_integral_mono)
+ by (auto intro!: nn_integral_mono)
(metis (erased, hide_lams) add_diff_cancel_left add_diff_eq diff_add_eq order_trans
norm_minus_commute norm_triangle_ineq4 order_refl)
also have "\<dots> = ?S + ?T"
- by (rule positive_integral_add) auto
+ by (rule nn_integral_add) auto
finally show ?thesis .
qed
@@ -524,14 +524,14 @@
assumes "M = N" "\<And>x. x \<in> space N \<Longrightarrow> f x = g x" "x = y"
shows "has_bochner_integral M f x \<longleftrightarrow> has_bochner_integral N g y"
unfolding has_bochner_integral.simps assms(1,3)
- using assms(2) by (simp cong: measurable_cong_strong positive_integral_cong_strong)
+ using assms(2) by (simp cong: measurable_cong_strong nn_integral_cong_strong)
lemma has_bochner_integral_cong_AE:
"f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (AE x in M. f x = g x) \<Longrightarrow>
has_bochner_integral M f x \<longleftrightarrow> has_bochner_integral M g x"
unfolding has_bochner_integral.simps
by (intro arg_cong[where f=Ex] ext conj_cong rev_conj_cong refl arg_cong[where f="\<lambda>x. x ----> 0"]
- positive_integral_cong_AE)
+ nn_integral_cong_AE)
auto
lemma borel_measurable_has_bochner_integral[measurable_dest]:
@@ -557,7 +557,7 @@
using A by auto
qed (rule simple_function_indicator assms)+
moreover have "simple_bochner_integral M (indicator A) = measure M A"
- using simple_bochner_integral_eq_positive_integral[OF sbi] A
+ using simple_bochner_integral_eq_nn_integral[OF sbi] A
by (simp add: ereal_indicator emeasure_eq_ereal_measure)
ultimately show ?thesis
by (metis has_bochner_integral_simple_bochner_integrable)
@@ -584,14 +584,14 @@
(is "?f ----> 0")
proof (rule tendsto_sandwich)
show "eventually (\<lambda>n. 0 \<le> ?f n) sequentially" "(\<lambda>_. 0) ----> 0"
- by (auto simp: positive_integral_positive)
+ by (auto simp: nn_integral_nonneg)
show "eventually (\<lambda>i. ?f i \<le> (\<integral>\<^sup>+ x. (norm (f x - sf i x)) \<partial>M) + \<integral>\<^sup>+ x. (norm (g x - sg i x)) \<partial>M) sequentially"
(is "eventually (\<lambda>i. ?f i \<le> ?g i) sequentially")
proof (intro always_eventually allI)
fix i have "?f i \<le> (\<integral>\<^sup>+ x. (norm (f x - sf i x)) + ereal (norm (g x - sg i x)) \<partial>M)"
- by (auto intro!: positive_integral_mono norm_diff_triangle_ineq)
+ by (auto intro!: nn_integral_mono norm_diff_triangle_ineq)
also have "\<dots> = ?g i"
- by (intro positive_integral_add) auto
+ by (intro nn_integral_add) auto
finally show "?f i \<le> ?g i" .
qed
show "?g ----> 0"
@@ -625,15 +625,15 @@
(is "?f ----> 0")
proof (rule tendsto_sandwich)
show "eventually (\<lambda>n. 0 \<le> ?f n) sequentially" "(\<lambda>_. 0) ----> 0"
- by (auto simp: positive_integral_positive)
+ by (auto simp: nn_integral_nonneg)
show "eventually (\<lambda>i. ?f i \<le> K * (\<integral>\<^sup>+ x. norm (f x - s i x) \<partial>M)) sequentially"
(is "eventually (\<lambda>i. ?f i \<le> ?g i) sequentially")
proof (intro always_eventually allI)
fix i have "?f i \<le> (\<integral>\<^sup>+ x. ereal K * norm (f x - s i x) \<partial>M)"
- using K by (intro positive_integral_mono) (auto simp: mult_ac)
+ using K by (intro nn_integral_mono) (auto simp: mult_ac)
also have "\<dots> = ?g i"
- using K by (intro positive_integral_cmult) auto
+ using K by (intro nn_integral_cmult) auto
finally show "?f i \<le> ?g i" .
qed
show "?g ----> 0"
@@ -738,15 +738,15 @@
then have "\<And>x. x \<in> space M \<Longrightarrow> norm (s i x) \<le> m" "0 \<le> m"
by (auto simp: m_def image_comp comp_def Max_ge_iff)
then have "(\<integral>\<^sup>+x. norm (s i x) \<partial>M) \<le> (\<integral>\<^sup>+x. ereal m * indicator {x\<in>space M. s i x \<noteq> 0} x \<partial>M)"
- by (auto split: split_indicator intro!: Max_ge positive_integral_mono simp:)
+ by (auto split: split_indicator intro!: Max_ge nn_integral_mono simp:)
also have "\<dots> < \<infinity>"
- using s by (subst positive_integral_cmult_indicator) (auto simp: `0 \<le> m` simple_bochner_integrable.simps)
+ using s by (subst nn_integral_cmult_indicator) (auto simp: `0 \<le> m` simple_bochner_integrable.simps)
finally have s_fin: "(\<integral>\<^sup>+x. norm (s i x) \<partial>M) < \<infinity>" .
have "(\<integral>\<^sup>+ x. norm (f x) \<partial>M) \<le> (\<integral>\<^sup>+ x. ereal (norm (f x - s i x)) + ereal (norm (s i x)) \<partial>M)"
- by (auto intro!: positive_integral_mono) (metis add_commute norm_triangle_sub)
+ by (auto intro!: nn_integral_mono) (metis add_commute norm_triangle_sub)
also have "\<dots> = (\<integral>\<^sup>+x. norm (f x - s i x) \<partial>M) + (\<integral>\<^sup>+x. norm (s i x) \<partial>M)"
- by (rule positive_integral_add) auto
+ by (rule nn_integral_add) auto
also have "\<dots> < \<infinity>"
using s_fin f_s_fin by auto
finally show "(\<integral>\<^sup>+ x. ereal (norm (f x)) \<partial>M) < \<infinity>" .
@@ -776,13 +776,13 @@
have "ereal (norm (?s n)) \<le> simple_bochner_integral M (\<lambda>x. norm (s n x))"
by (auto intro!: simple_bochner_integral_norm_bound)
also have "\<dots> = (\<integral>\<^sup>+x. norm (s n x) \<partial>M)"
- by (intro simple_bochner_integral_eq_positive_integral)
+ by (intro simple_bochner_integral_eq_nn_integral)
(auto intro: s simple_bochner_integrable_compose2)
also have "\<dots> \<le> (\<integral>\<^sup>+x. ereal (norm (f x - s n x)) + norm (f x) \<partial>M)"
- by (auto intro!: positive_integral_mono)
+ by (auto intro!: nn_integral_mono)
(metis add_commute norm_minus_commute norm_triangle_sub)
also have "\<dots> = ?t n"
- by (rule positive_integral_add) auto
+ by (rule nn_integral_add) auto
finally show "norm (?s n) \<le> ?t n" .
qed
have "?t ----> 0 + (\<integral>\<^sup>+ x. ereal (norm (f x)) \<partial>M)"
@@ -816,7 +816,7 @@
have "(\<lambda>i. ereal (norm (?s i - ?t i))) ----> ereal 0"
proof (rule tendsto_sandwich)
show "eventually (\<lambda>i. 0 \<le> ereal (norm (?s i - ?t i))) sequentially" "(\<lambda>_. 0) ----> ereal 0"
- by (auto simp: positive_integral_positive zero_ereal_def[symmetric])
+ by (auto simp: nn_integral_nonneg zero_ereal_def[symmetric])
show "eventually (\<lambda>i. norm (?s i - ?t i) \<le> ?S i + ?T i) sequentially"
by (intro always_eventually allI simple_bochner_integral_bounded s t f)
@@ -841,7 +841,7 @@
fix s assume "(\<lambda>i. \<integral>\<^sup>+ x. ereal (norm (f x - s i x)) \<partial>M) ----> 0"
also have "(\<lambda>i. \<integral>\<^sup>+ x. ereal (norm (f x - s i x)) \<partial>M) = (\<lambda>i. \<integral>\<^sup>+ x. ereal (norm (g x - s i x)) \<partial>M)"
using ae
- by (intro ext positive_integral_cong_AE, eventually_elim) simp
+ by (intro ext nn_integral_cong_AE, eventually_elim) simp
finally show "(\<lambda>i. \<integral>\<^sup>+ x. ereal (norm (g x - s i x)) \<partial>M) ----> 0" .
qed (auto intro: g)
@@ -1087,7 +1087,7 @@
by (intro simple_bochner_integral_bounded s f)
also have "\<dots> < ereal (e / 2) + e / 2"
using ereal_add_strict_mono[OF less_imp_le[OF M[OF n]] _ `?S n \<noteq> \<infinity>` M[OF m]]
- by (auto simp: positive_integral_positive)
+ by (auto simp: nn_integral_nonneg)
also have "\<dots> = e" by simp
finally show "dist (?s n) (?s m) < e"
by (simp add: dist_norm)
@@ -1098,7 +1098,7 @@
by (rule, rule) fact+
qed
-lemma positive_integral_dominated_convergence_norm:
+lemma nn_integral_dominated_convergence_norm:
fixes u' :: "_ \<Rightarrow> _::{real_normed_vector, second_countable_topology}"
assumes [measurable]:
"\<And>i. u i \<in> borel_measurable M" "u' \<in> borel_measurable M" "w \<in> borel_measurable M"
@@ -1122,9 +1122,9 @@
qed
have "(\<lambda>i. (\<integral>\<^sup>+x. norm (u' x - u i x) \<partial>M)) ----> (\<integral>\<^sup>+x. 0 \<partial>M)"
- proof (rule positive_integral_dominated_convergence)
+ proof (rule nn_integral_dominated_convergence)
show "(\<integral>\<^sup>+x. 2 * w x \<partial>M) < \<infinity>"
- by (rule positive_integral_mult_bounded_inf[OF _ w, of 2]) auto
+ by (rule nn_integral_mult_bounded_inf[OF _ w, of 2]) auto
show "AE x in M. (\<lambda>i. ereal (norm (u' x - u i x))) ----> 0"
using u'
proof eventually_elim
@@ -1152,9 +1152,9 @@
proof (rule integrableI_sequence)
{ fix i
have "(\<integral>\<^sup>+x. norm (s i x) \<partial>M) \<le> (\<integral>\<^sup>+x. 2 * ereal (norm (f x)) \<partial>M)"
- by (intro positive_integral_mono) (simp add: bound)
+ by (intro nn_integral_mono) (simp add: bound)
also have "\<dots> = 2 * (\<integral>\<^sup>+x. ereal (norm (f x)) \<partial>M)"
- by (rule positive_integral_cmult) auto
+ by (rule nn_integral_cmult) auto
finally have "(\<integral>\<^sup>+x. norm (s i x) \<partial>M) < \<infinity>"
using fin by auto }
note fin_s = this
@@ -1163,13 +1163,13 @@
by (rule simple_bochner_integrableI_bounded) fact+
show "(\<lambda>i. \<integral>\<^sup>+ x. ereal (norm (f x - s i x)) \<partial>M) ----> 0"
- proof (rule positive_integral_dominated_convergence_norm)
+ proof (rule nn_integral_dominated_convergence_norm)
show "\<And>j. AE x in M. norm (s j x) \<le> 2 * norm (f x)"
using bound by auto
show "\<And>i. s i \<in> borel_measurable M" "(\<lambda>x. 2 * norm (f x)) \<in> borel_measurable M"
using s by (auto intro: borel_measurable_simple_function)
show "(\<integral>\<^sup>+ x. ereal (2 * norm (f x)) \<partial>M) < \<infinity>"
- using fin unfolding times_ereal.simps(1)[symmetric] by (subst positive_integral_cmult) auto
+ using fin unfolding times_ereal.simps(1)[symmetric] by (subst nn_integral_cmult) auto
show "AE x in M. (\<lambda>i. s i x) ----> f x"
using pointwise by auto
qed fact
@@ -1182,7 +1182,7 @@
shows "integrable M f"
proof -
have "(\<integral>\<^sup>+x. norm (f x) \<partial>M) = (\<integral>\<^sup>+x. f x \<partial>M)"
- using assms by (intro positive_integral_cong_AE) auto
+ using assms by (intro nn_integral_cong_AE) auto
then show ?thesis
using assms by (intro integrableI_bounded) auto
qed
@@ -1203,7 +1203,7 @@
assume "f \<in> borel_measurable M" "g \<in> borel_measurable M"
assume "AE x in M. norm (g x) \<le> norm (f x)"
then have "(\<integral>\<^sup>+ x. ereal (norm (g x)) \<partial>M) \<le> (\<integral>\<^sup>+ x. ereal (norm (f x)) \<partial>M)"
- by (intro positive_integral_mono_AE) auto
+ by (intro nn_integral_mono_AE) auto
also assume "(\<integral>\<^sup>+ x. ereal (norm (f x)) \<partial>M) < \<infinity>"
finally show "(\<integral>\<^sup>+ x. ereal (norm (g x)) \<partial>M) < \<infinity>" .
qed
@@ -1249,7 +1249,7 @@
lemma integrable_indicator_iff:
"integrable M (indicator A::_ \<Rightarrow> real) \<longleftrightarrow> A \<inter> space M \<in> sets M \<and> emeasure M (A \<inter> space M) < \<infinity>"
- by (simp add: integrable_iff_bounded borel_measurable_indicator_iff ereal_indicator positive_integral_indicator'
+ by (simp add: integrable_iff_bounded borel_measurable_indicator_iff ereal_indicator nn_integral_indicator'
cong: conj_cong)
lemma integral_dominated_convergence:
@@ -1264,7 +1264,7 @@
have "AE x in M. 0 \<le> w x"
using bound[of 0] by eventually_elim (auto intro: norm_ge_zero order_trans)
then have "(\<integral>\<^sup>+x. w x \<partial>M) = (\<integral>\<^sup>+x. norm (w x) \<partial>M)"
- by (intro positive_integral_cong_AE) auto
+ by (intro nn_integral_cong_AE) auto
with `integrable M w` have w: "w \<in> borel_measurable M" "(\<integral>\<^sup>+x. w x \<partial>M) < \<infinity>"
unfolding integrable_iff_bounded by auto
@@ -1273,7 +1273,7 @@
proof
fix i
have "(\<integral>\<^sup>+ x. ereal (norm (s i x)) \<partial>M) \<le> (\<integral>\<^sup>+x. w x \<partial>M)"
- using bound by (intro positive_integral_mono_AE) auto
+ using bound by (intro nn_integral_mono_AE) auto
with w show "(\<integral>\<^sup>+ x. ereal (norm (s i x)) \<partial>M) < \<infinity>" by auto
qed fact
@@ -1285,7 +1285,7 @@
proof
have "(\<integral>\<^sup>+ x. ereal (norm (f x)) \<partial>M) \<le> (\<integral>\<^sup>+x. w x \<partial>M)"
using all_bound lim
- proof (intro positive_integral_mono_AE, eventually_elim)
+ proof (intro nn_integral_mono_AE, eventually_elim)
fix x assume "\<forall>i. norm (s i x) \<le> w x" "(\<lambda>i. s i x) ----> f x"
then show "ereal (norm (f x)) \<le> ereal (w x)"
by (intro LIMSEQ_le_const2[where X="\<lambda>i. ereal (norm (s i x))"] tendsto_intros lim_ereal[THEN iffD2]) auto
@@ -1308,7 +1308,7 @@
show "(\<lambda>n. \<integral>\<^sup>+x. norm (s n x - f x) \<partial>M) ----> ereal 0"
unfolding zero_ereal_def[symmetric]
apply (subst norm_minus_commute)
- proof (rule positive_integral_dominated_convergence_norm[where w=w])
+ proof (rule nn_integral_dominated_convergence_norm[where w=w])
show "\<And>n. s n \<in> borel_measurable M"
using int_s unfolding integrable_iff_bounded by auto
qed fact+
@@ -1325,7 +1325,7 @@
using integrable_mult_left[of c M f] integrable_mult_left[of "1 / c" M "\<lambda>x. c * f x"]
by (cases "c = 0") auto
-lemma positive_integral_eq_integral:
+lemma nn_integral_eq_integral:
assumes f: "integrable M f"
assumes nonneg: "AE x in M. 0 \<le> f x"
shows "(\<integral>\<^sup>+ x. f x \<partial>M) = integral\<^sup>L M f"
@@ -1338,7 +1338,7 @@
next
case (mult f c) then show ?case
unfolding times_ereal.simps(1)[symmetric]
- by (subst positive_integral_cmult)
+ by (subst nn_integral_cmult)
(auto simp add: integrable_mult_left_iff zero_ereal_def[symmetric])
next
case (add g f)
@@ -1346,7 +1346,7 @@
by (auto intro!: integrable_bound[OF add(8)])
with add show ?case
unfolding plus_ereal.simps(1)[symmetric]
- by (subst positive_integral_add) auto
+ by (subst nn_integral_add) auto
next
case (seq s)
{ fix i x assume "x \<in> space M" with seq(4) have "s i x \<le> f x"
@@ -1366,7 +1366,7 @@
using seq f s_le_f by (intro integrable_bound[OF f(3)]) auto
have "(\<lambda>i. \<integral>\<^sup>+ x. s i x \<partial>M) ----> \<integral>\<^sup>+ x. f x \<partial>M"
using seq s_le_f f
- by (intro positive_integral_dominated_convergence[where w=f])
+ by (intro nn_integral_dominated_convergence[where w=f])
(auto simp: integrable_iff_bounded)
also have "(\<lambda>i. \<integral>\<^sup>+x. s i x \<partial>M) = (\<lambda>i. \<integral>x. s i x \<partial>M)"
using seq int_s by simp
@@ -1379,19 +1379,19 @@
also have "\<dots> = integral\<^sup>L M f"
using assms by (auto intro!: integral_cong_AE)
also have "(\<integral>\<^sup>+ x. max 0 (f x) \<partial>M) = (\<integral>\<^sup>+ x. f x \<partial>M)"
- using assms by (auto intro!: positive_integral_cong_AE simp: max_def)
+ using assms by (auto intro!: nn_integral_cong_AE simp: max_def)
finally show ?thesis .
qed
lemma integral_norm_bound:
fixes f :: "_ \<Rightarrow> 'a :: {banach, second_countable_topology}"
shows "integrable M f \<Longrightarrow> norm (integral\<^sup>L M f) \<le> (\<integral>x. norm (f x) \<partial>M)"
- using positive_integral_eq_integral[of M "\<lambda>x. norm (f x)"]
+ using nn_integral_eq_integral[of M "\<lambda>x. norm (f x)"]
using integral_norm_bound_ereal[of M f] by simp
-lemma integral_eq_positive_integral:
+lemma integral_eq_nn_integral:
"integrable M f \<Longrightarrow> (\<And>x. 0 \<le> f x) \<Longrightarrow> integral\<^sup>L M f = real (\<integral>\<^sup>+ x. ereal (f x) \<partial>M)"
- by (subst positive_integral_eq_integral) auto
+ by (subst nn_integral_eq_integral) auto
lemma integrableI_simple_bochner_integrable:
fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
@@ -1445,9 +1445,9 @@
fix i
have "(\<integral>\<^sup>+x. norm (s' i x) \<partial>M) \<le> (\<integral>\<^sup>+x. 2 * ereal (norm (f x)) \<partial>M)"
- using s by (intro positive_integral_mono) (auto simp: s'_eq_s)
+ using s by (intro nn_integral_mono) (auto simp: s'_eq_s)
also have "\<dots> < \<infinity>"
- using f by (subst positive_integral_cmult) auto
+ using f by (subst nn_integral_cmult) auto
finally have sbi: "simple_bochner_integrable M (s' i)"
using sf by (intro simple_bochner_integrableI_bounded) auto
then show "integrable M (s' i)"
@@ -1475,8 +1475,8 @@
shows "0 \<le> integral\<^sup>L M f"
proof -
have "0 \<le> ereal (integral\<^sup>L M (\<lambda>x. max 0 (f x)))"
- by (subst integral_eq_positive_integral)
- (auto intro: real_of_ereal_pos positive_integral_positive integrable_max assms)
+ by (subst integral_eq_nn_integral)
+ (auto intro: real_of_ereal_pos nn_integral_nonneg integrable_max assms)
also have "integral\<^sup>L M (\<lambda>x. max 0 (f x)) = integral\<^sup>L M f"
using assms(2) by (intro integral_cong_AE assms integrable_max) auto
finally show ?thesis
@@ -1493,10 +1493,10 @@
shows "integral\<^sup>L M f = 0 \<longleftrightarrow> (AE x in M. f x = 0)"
proof
assume "integral\<^sup>L M f = 0"
- then have "integral\<^sup>P M f = 0"
- using positive_integral_eq_integral[OF f nonneg] by simp
+ then have "integral\<^sup>N M f = 0"
+ using nn_integral_eq_integral[OF f nonneg] by simp
then have "AE x in M. ereal (f x) \<le> 0"
- by (simp add: positive_integral_0_iff_AE)
+ by (simp add: nn_integral_0_iff_AE)
with nonneg show "AE x in M. f x = 0"
by auto
qed (auto simp add: integral_eq_zero_AE)
@@ -1527,8 +1527,8 @@
and nn: "AE x in M. 0 \<le> g x"
shows "integrable (density M g) f \<longleftrightarrow> integrable M (\<lambda>x. g x *\<^sub>R f x)"
unfolding integrable_iff_bounded using nn
- apply (simp add: positive_integral_density )
- apply (intro arg_cong2[where f="op ="] refl positive_integral_cong_AE)
+ apply (simp add: nn_integral_density )
+ apply (intro arg_cong2[where f="op ="] refl nn_integral_cong_AE)
apply auto
done
@@ -1547,9 +1547,9 @@
have int: "integrable M (\<lambda>x. g x * indicator A x)"
using g base integrable_density[of "indicator A :: 'a \<Rightarrow> real" M g] by simp
then have "integral\<^sup>L M (\<lambda>x. g x * indicator A x) = (\<integral>\<^sup>+ x. ereal (g x * indicator A x) \<partial>M)"
- using g by (subst positive_integral_eq_integral) auto
+ using g by (subst nn_integral_eq_integral) auto
also have "\<dots> = (\<integral>\<^sup>+ x. ereal (g x) * indicator A x \<partial>M)"
- by (intro positive_integral_cong) (auto split: split_indicator)
+ by (intro nn_integral_cong) (auto split: split_indicator)
also have "\<dots> = emeasure (density M g) A"
by (rule emeasure_density[symmetric]) auto
also have "\<dots> = ereal (measure (density M g) A)"
@@ -1607,7 +1607,7 @@
fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
assumes [measurable]: "g \<in> measurable M N" "f \<in> borel_measurable N"
shows "integrable (distr M N g) f \<longleftrightarrow> integrable M (\<lambda>x. f (g x))"
- unfolding integrable_iff_bounded by (simp_all add: positive_integral_distr)
+ unfolding integrable_iff_bounded by (simp_all add: nn_integral_distr)
lemma integrable_distr:
fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
@@ -1678,7 +1678,7 @@
lemma integrable_count_space:
fixes f :: "'a \<Rightarrow> 'b::{banach,second_countable_topology}"
shows "finite X \<Longrightarrow> integrable (count_space X) f"
- by (auto simp: positive_integral_count_space integrable_iff_bounded)
+ by (auto simp: nn_integral_count_space integrable_iff_bounded)
lemma measure_count_space[simp]:
"B \<subseteq> A \<Longrightarrow> finite B \<Longrightarrow> measure (count_space A) B = card B"
@@ -1731,15 +1731,15 @@
also have "\<dots> = integral\<^sup>L M (\<lambda>x. max 0 (f x)) - integral\<^sup>L M (\<lambda>x. max 0 (- f x))"
by (intro integral_diff integrable_max integrable_minus integrable_zero f)
also have "integral\<^sup>L M (\<lambda>x. max 0 (f x)) = real (\<integral>\<^sup>+x. max 0 (f x) \<partial>M)"
- by (subst integral_eq_positive_integral[symmetric]) (auto intro!: integrable_max f)
+ by (subst integral_eq_nn_integral[symmetric]) (auto intro!: integrable_max f)
also have "integral\<^sup>L M (\<lambda>x. max 0 (- f x)) = real (\<integral>\<^sup>+x. max 0 (- f x) \<partial>M)"
- by (subst integral_eq_positive_integral[symmetric]) (auto intro!: integrable_max f)
+ by (subst integral_eq_nn_integral[symmetric]) (auto intro!: integrable_max f)
also have "(\<lambda>x. ereal (max 0 (f x))) = (\<lambda>x. max 0 (ereal (f x)))"
by (auto simp: max_def)
also have "(\<lambda>x. ereal (max 0 (- f x))) = (\<lambda>x. max 0 (- ereal (f x)))"
by (auto simp: max_def)
finally show ?thesis
- unfolding positive_integral_max_0 .
+ unfolding nn_integral_max_0 .
qed
lemma real_integrable_def:
@@ -1749,12 +1749,12 @@
proof (safe del: notI)
assume *: "(\<integral>\<^sup>+ x. ereal (norm (f x)) \<partial>M) < \<infinity>"
have "(\<integral>\<^sup>+ x. ereal (f x) \<partial>M) \<le> (\<integral>\<^sup>+ x. ereal (norm (f x)) \<partial>M)"
- by (intro positive_integral_mono) auto
+ by (intro nn_integral_mono) auto
also note *
finally show "(\<integral>\<^sup>+ x. ereal (f x) \<partial>M) \<noteq> \<infinity>"
by simp
have "(\<integral>\<^sup>+ x. ereal (- f x) \<partial>M) \<le> (\<integral>\<^sup>+ x. ereal (norm (f x)) \<partial>M)"
- by (intro positive_integral_mono) auto
+ by (intro nn_integral_mono) auto
also note *
finally show "(\<integral>\<^sup>+ x. ereal (- f x) \<partial>M) \<noteq> \<infinity>"
by simp
@@ -1762,11 +1762,11 @@
assume [measurable]: "f \<in> borel_measurable M"
assume fin: "(\<integral>\<^sup>+ x. ereal (f x) \<partial>M) \<noteq> \<infinity>" "(\<integral>\<^sup>+ x. ereal (- f x) \<partial>M) \<noteq> \<infinity>"
have "(\<integral>\<^sup>+ x. norm (f x) \<partial>M) = (\<integral>\<^sup>+ x. max 0 (ereal (f x)) + max 0 (ereal (- f x)) \<partial>M)"
- by (intro positive_integral_cong) (auto simp: max_def)
+ by (intro nn_integral_cong) (auto simp: max_def)
also have"\<dots> = (\<integral>\<^sup>+ x. max 0 (ereal (f x)) \<partial>M) + (\<integral>\<^sup>+ x. max 0 (ereal (- f x)) \<partial>M)"
- by (intro positive_integral_add) auto
+ by (intro nn_integral_add) auto
also have "\<dots> < \<infinity>"
- using fin by (auto simp: positive_integral_max_0)
+ using fin by (auto simp: nn_integral_max_0)
finally show "(\<integral>\<^sup>+ x. norm (f x) \<partial>M) < \<infinity>" .
qed
@@ -1782,8 +1782,8 @@
"(\<integral>\<^sup>+x. ereal (-f x)\<partial>M) = ereal q"
"f \<in> borel_measurable M" "integral\<^sup>L M f = r - q"
using assms unfolding real_integrable_def real_lebesgue_integral_def[OF assms]
- using positive_integral_positive[of M "\<lambda>x. ereal (f x)"]
- using positive_integral_positive[of M "\<lambda>x. ereal (-f x)"]
+ using nn_integral_nonneg[of M "\<lambda>x. ereal (f x)"]
+ using nn_integral_nonneg[of M "\<lambda>x. ereal (-f x)"]
by (cases rule: ereal2_cases[of "(\<integral>\<^sup>+x. ereal (-f x)\<partial>M)" "(\<integral>\<^sup>+x. ereal (f x)\<partial>M)"]) auto
lemma integral_monotone_convergence_nonneg:
@@ -1797,7 +1797,7 @@
and "integral\<^sup>L M u = x"
proof -
have "(\<integral>\<^sup>+ x. ereal (u x) \<partial>M) = (SUP n. (\<integral>\<^sup>+ x. ereal (f n x) \<partial>M))"
- proof (subst positive_integral_monotone_convergence_SUP_AE[symmetric])
+ proof (subst nn_integral_monotone_convergence_SUP_AE[symmetric])
fix i
from mono pos show "AE x in M. ereal (f i x) \<le> ereal (f (Suc i) x) \<and> 0 \<le> ereal (f i x)"
by eventually_elim (auto simp: mono_def)
@@ -1805,16 +1805,16 @@
using i by auto
next
show "(\<integral>\<^sup>+ x. ereal (u x) \<partial>M) = \<integral>\<^sup>+ x. (SUP i. ereal (f i x)) \<partial>M"
- apply (rule positive_integral_cong_AE)
+ apply (rule nn_integral_cong_AE)
using lim mono
by eventually_elim (simp add: SUP_eq_LIMSEQ[THEN iffD2])
qed
also have "\<dots> = ereal x"
- using mono i unfolding positive_integral_eq_integral[OF i pos]
+ using mono i unfolding nn_integral_eq_integral[OF i pos]
by (subst SUP_eq_LIMSEQ) (auto simp: mono_def intro!: integral_mono_AE ilim)
finally have "(\<integral>\<^sup>+ x. ereal (u x) \<partial>M) = ereal x" .
moreover have "(\<integral>\<^sup>+ x. ereal (- u x) \<partial>M) = 0"
- proof (subst positive_integral_0_iff_AE)
+ proof (subst nn_integral_0_iff_AE)
show "(\<lambda>x. ereal (- u x)) \<in> borel_measurable M"
using u by auto
from mono pos[of 0] lim show "AE x in M. ereal (- u x) \<le> 0"
@@ -1865,11 +1865,11 @@
shows "(\<integral>x. norm (f x) \<partial>M) = 0 \<longleftrightarrow> emeasure M {x\<in>space M. f x \<noteq> 0} = 0"
proof -
have "(\<integral>\<^sup>+x. norm (f x) \<partial>M) = (\<integral>x. norm (f x) \<partial>M)"
- using f by (intro positive_integral_eq_integral integrable_norm) auto
+ using f by (intro nn_integral_eq_integral integrable_norm) auto
then have "(\<integral>x. norm (f x) \<partial>M) = 0 \<longleftrightarrow> (\<integral>\<^sup>+x. norm (f x) \<partial>M) = 0"
by simp
also have "\<dots> \<longleftrightarrow> emeasure M {x\<in>space M. ereal (norm (f x)) \<noteq> 0} = 0"
- by (intro positive_integral_0_iff) auto
+ by (intro nn_integral_0_iff) auto
finally show ?thesis
by simp
qed
@@ -1917,7 +1917,7 @@
using int by (simp add: integral_0_iff)
moreover
have "(\<integral>\<^sup>+x. indicator A x \<partial>M) \<le> (\<integral>\<^sup>+x. indicator {x \<in> space M. Y x - X x \<noteq> 0} x \<partial>M)"
- using A by (intro positive_integral_mono_AE) auto
+ using A by (intro nn_integral_mono_AE) auto
then have "(emeasure M) A \<le> (emeasure M) {x \<in> space M. Y x - X x \<noteq> 0}"
using int A by (simp add: integrable_def)
ultimately have "emeasure M A = 0"
@@ -2221,7 +2221,7 @@
by (intro simple_function_borel_measurable)
(auto simp: space_pair_measure dest: finite_subset)
have "(\<integral>\<^sup>+ y. ereal (norm (s i (x, y))) \<partial>M) \<le> (\<integral>\<^sup>+ y. 2 * norm (f x y) \<partial>M)"
- using x s by (intro positive_integral_mono) auto
+ using x s by (intro nn_integral_mono) auto
also have "(\<integral>\<^sup>+ y. 2 * norm (f x y) \<partial>M) < \<infinity>"
using int_2f by (simp add: integrable_iff_bounded)
finally show "(\<integral>\<^sup>+ xa. ereal (norm (s i (x, xa))) \<partial>M) < \<infinity>" .
@@ -2276,7 +2276,7 @@
have "(\<integral>\<^sup>+ x. emeasure M2 (Pair x -` A) \<partial>M1) \<noteq> \<infinity>"
by simp
then have "AE x in M1. emeasure M2 (Pair x -` A) \<noteq> \<infinity>"
- by (rule positive_integral_PInf_AE[rotated]) (intro M2.measurable_emeasure_Pair A)
+ by (rule nn_integral_PInf_AE[rotated]) (intro M2.measurable_emeasure_Pair A)
moreover have "\<And>x. x \<in> space M1 \<Longrightarrow> Pair x -` A = {y\<in>space M2. (x, y) \<in> A}"
using sets.sets_into_space[OF A] by (auto simp: space_pair_measure)
ultimately show ?thesis by auto
@@ -2288,11 +2288,11 @@
shows "AE x in M1. integrable M2 (\<lambda>y. f (x, y))"
proof -
have "(\<integral>\<^sup>+x. (\<integral>\<^sup>+y. norm (f (x, y)) \<partial>M2) \<partial>M1) = (\<integral>\<^sup>+x. norm (f x) \<partial>(M1 \<Otimes>\<^sub>M M2))"
- by (rule M2.positive_integral_fst) simp
+ by (rule M2.nn_integral_fst) simp
also have "(\<integral>\<^sup>+x. norm (f x) \<partial>(M1 \<Otimes>\<^sub>M M2)) \<noteq> \<infinity>"
using f unfolding integrable_iff_bounded by simp
finally have "AE x in M1. (\<integral>\<^sup>+y. norm (f (x, y)) \<partial>M2) \<noteq> \<infinity>"
- by (intro positive_integral_PInf_AE M2.borel_measurable_positive_integral )
+ by (intro nn_integral_PInf_AE M2.borel_measurable_nn_integral )
(auto simp: measurable_split_conv)
with AE_space show ?thesis
by eventually_elim
@@ -2308,9 +2308,9 @@
show "(\<lambda>x. \<integral> y. f (x, y) \<partial>M2) \<in> borel_measurable M1"
by (rule M2.borel_measurable_lebesgue_integral) simp
have "(\<integral>\<^sup>+ x. ereal (norm (\<integral> y. f (x, y) \<partial>M2)) \<partial>M1) \<le> (\<integral>\<^sup>+x. (\<integral>\<^sup>+y. norm (f (x, y)) \<partial>M2) \<partial>M1)"
- using AE_integrable_fst'[OF f] by (auto intro!: positive_integral_mono_AE integral_norm_bound_ereal)
+ using AE_integrable_fst'[OF f] by (auto intro!: nn_integral_mono_AE integral_norm_bound_ereal)
also have "(\<integral>\<^sup>+x. (\<integral>\<^sup>+y. norm (f (x, y)) \<partial>M2) \<partial>M1) = (\<integral>\<^sup>+x. norm (f x) \<partial>(M1 \<Otimes>\<^sub>M M2))"
- by (rule M2.positive_integral_fst) simp
+ by (rule M2.nn_integral_fst) simp
also have "(\<integral>\<^sup>+x. norm (f x) \<partial>(M1 \<Otimes>\<^sub>M M2)) < \<infinity>"
using f unfolding integrable_iff_bounded by simp
finally show "(\<integral>\<^sup>+ x. ereal (norm (\<integral> y. f (x, y) \<partial>M2)) \<partial>M1) < \<infinity>" .
@@ -2341,18 +2341,18 @@
have "(\<integral>\<^sup>+x. ereal (measure M2 {y \<in> space M2. (x, y) \<in> A}) \<partial>M1) =
(\<integral>\<^sup>+x. emeasure M2 {y \<in> space M2. (x, y) \<in> A} \<partial>M1)"
using emeasure_pair_measure_finite[OF base]
- by (intro positive_integral_cong_AE, eventually_elim) (simp add: emeasure_eq_ereal_measure)
+ by (intro nn_integral_cong_AE, eventually_elim) (simp add: emeasure_eq_ereal_measure)
also have "\<dots> = emeasure (M1 \<Otimes>\<^sub>M M2) A"
using sets.sets_into_space[OF A]
by (subst M2.emeasure_pair_measure_alt)
- (auto intro!: positive_integral_cong arg_cong[where f="emeasure M2"] simp: space_pair_measure)
+ (auto intro!: nn_integral_cong arg_cong[where f="emeasure M2"] simp: space_pair_measure)
finally have *: "(\<integral>\<^sup>+x. ereal (measure M2 {y \<in> space M2. (x, y) \<in> A}) \<partial>M1) = emeasure (M1 \<Otimes>\<^sub>M M2) A" .
from base * show "integrable M1 (\<lambda>x. measure M2 {y \<in> space M2. (x, y) \<in> A})"
by (simp add: measure_nonneg integrable_iff_bounded)
then have "(\<integral>x. measure M2 {y \<in> space M2. (x, y) \<in> A} \<partial>M1) =
(\<integral>\<^sup>+x. ereal (measure M2 {y \<in> space M2. (x, y) \<in> A}) \<partial>M1)"
- by (rule positive_integral_eq_integral[symmetric]) (simp add: measure_nonneg)
+ by (rule nn_integral_eq_integral[symmetric]) (simp add: measure_nonneg)
also note *
finally show "(\<integral>x. measure M2 {y \<in> space M2. (x, y) \<in> A} \<partial>M1) *\<^sub>R c = measure (M1 \<Otimes>\<^sub>M M2) A *\<^sub>R c"
using base by (simp add: emeasure_eq_ereal_measure)
@@ -2417,9 +2417,9 @@
from s have "norm (\<integral> y. s i (x, y) \<partial>M2) \<le> (\<integral>\<^sup>+y. norm (s i (x, y)) \<partial>M2)"
by (rule integral_norm_bound_ereal)
also have "\<dots> \<le> (\<integral>\<^sup>+y. 2 * norm (f (x, y)) \<partial>M2)"
- using x lim by (auto intro!: positive_integral_mono simp: space_pair_measure)
+ using x lim by (auto intro!: nn_integral_mono simp: space_pair_measure)
also have "\<dots> = (\<integral>y. 2 * norm (f (x, y)) \<partial>M2)"
- using f by (intro positive_integral_eq_integral) auto
+ using f by (intro nn_integral_eq_integral) auto
finally show "norm (\<integral> y. s i (x, y) \<partial>M2) \<le> (\<integral> y. 2 * norm (f (x, y)) \<partial>M2)"
by simp
qed
@@ -2530,9 +2530,9 @@
(\<integral>\<^sup>+ x. (\<Prod>i\<in>I. ereal (norm (f i (x i)))) \<partial>Pi\<^sub>M I M)"
by (simp add: setprod_norm setprod_ereal)
also have "\<dots> = (\<Prod>i\<in>I. \<integral>\<^sup>+ x. ereal (norm (f i x)) \<partial>M i)"
- using assms by (intro product_positive_integral_setprod) auto
+ using assms by (intro product_nn_integral_setprod) auto
also have "\<dots> < \<infinity>"
- using integrable by (simp add: setprod_PInf positive_integral_positive integrable_iff_bounded)
+ using integrable by (simp add: setprod_PInf nn_integral_nonneg integrable_iff_bounded)
finally show "(\<integral>\<^sup>+ x. ereal (norm (\<Prod>i\<in>I. f i (x i))) \<partial>Pi\<^sub>M I M) < \<infinity>" .
qed
@@ -2568,7 +2568,7 @@
have "f \<in> borel_measurable M"
using assms by (auto simp: measurable_def)
with assms show ?thesis
- using assms by (auto simp: integrable_iff_bounded positive_integral_subalgebra)
+ using assms by (auto simp: integrable_iff_bounded nn_integral_subalgebra)
qed
lemma integral_subalgebra:
--- a/src/HOL/Probability/Distributions.thy Mon May 19 15:23:08 2014 +0200
+++ b/src/HOL/Probability/Distributions.thy Mon May 19 16:14:08 2014 +0200
@@ -56,9 +56,9 @@
have "emeasure ?D (space ?D) = (\<integral>\<^sup>+ x. ereal (?f x) * indicator {0..} x \<partial>lborel)"
by (auto simp: emeasure_density exponential_density_def
- intro!: positive_integral_cong split: split_indicator)
+ intro!: nn_integral_cong split: split_indicator)
also have "\<dots> = ereal (0 - ?F 0)"
- proof (rule positive_integral_FTC_atLeast)
+ proof (rule nn_integral_FTC_atLeast)
have "((\<lambda>x. exp (l * x)) ---> 0) at_bot"
by (rule filterlim_compose[OF exp_at_bot filterlim_tendsto_pos_mult_at_bot[of _ l]])
(simp_all add: tendsto_const filterlim_ident)
@@ -72,10 +72,10 @@
assume "0 \<le> a"
have "emeasure ?D {..a} = (\<integral>\<^sup>+x. ereal (?f x) * indicator {0..a} x \<partial>lborel)"
- by (auto simp add: emeasure_density intro!: positive_integral_cong split: split_indicator)
+ by (auto simp add: emeasure_density intro!: nn_integral_cong split: split_indicator)
(auto simp: exponential_density_def)
also have "(\<integral>\<^sup>+x. ereal (?f x) * indicator {0..a} x \<partial>lborel) = ereal (?F a) - ereal (?F 0)"
- using `0 \<le> a` deriv by (intro positive_integral_FTC_atLeastAtMost) auto
+ using `0 \<le> a` deriv by (intro nn_integral_FTC_atLeastAtMost) auto
also have "\<dots> = 1 - exp (- a * l)"
by simp
finally show "emeasure ?D {.. a} = 1 - exp (- a * l)" .
@@ -241,9 +241,9 @@
by simp
also have "\<dots> = (\<integral>\<^sup>+ x. (1 / emeasure M' A) * indicator (A \<inter> B) x \<partial>M')"
using A B
- by (intro positive_integral_cmult_indicator[symmetric]) (auto intro!: zero_le_divide_ereal)
+ by (intro nn_integral_cmult_indicator[symmetric]) (auto intro!: zero_le_divide_ereal)
also have "\<dots> = (\<integral>\<^sup>+ x. ?f x * indicator B x \<partial>M')"
- by (rule positive_integral_cong) (auto split: split_indicator)
+ by (rule nn_integral_cong) (auto split: split_indicator)
finally show "emeasure (distr M M' X) B = emeasure (density M' ?f) B"
using A B X by (auto simp add: emeasure_distr emeasure_density)
qed simp
@@ -271,10 +271,10 @@
have "(\<integral>\<^sup>+ x. ereal (indicator A x / measure lborel A * indicator {..a} x) \<partial>lborel) =
(\<integral>\<^sup>+ x. ereal (1 / measure lborel A) * indicator (A \<inter> {..a}) x \<partial>lborel)"
- by (auto intro!: positive_integral_cong split: split_indicator)
+ by (auto intro!: nn_integral_cong split: split_indicator)
also have "\<dots> = ereal (1 / measure lborel A) * emeasure lborel (A \<inter> {..a})"
using `A \<in> sets borel`
- by (intro positive_integral_cmult_indicator) (auto simp: measure_nonneg)
+ by (intro nn_integral_cmult_indicator) (auto simp: measure_nonneg)
also have "\<dots> = ereal (measure lborel (A \<inter> {..a}) / r)"
unfolding emeasure_eq_ereal_measure[OF fin] using A by (simp add: measure_def)
finally show "(\<integral>\<^sup>+ x. ereal (indicator A x / measure lborel A * indicator {..a} x) \<partial>lborel) =
@@ -331,10 +331,10 @@
using distributed_borel_measurable[OF D] `a \<le> t` `t \<le> b`
unfolding distributed_distr_eq_density[OF D]
by (subst emeasure_density)
- (auto intro!: positive_integral_cong simp: measure_def split: split_indicator)
+ (auto intro!: nn_integral_cong simp: measure_def split: split_indicator)
also have "\<dots> = ereal (1 / (b - a)) * (t - a)"
using `a \<le> t` `t \<le> b`
- by (subst positive_integral_cmult_indicator) auto
+ by (subst nn_integral_cmult_indicator) auto
finally show ?thesis
by (simp add: measure_def)
qed
--- a/src/HOL/Probability/Finite_Product_Measure.thy Mon May 19 15:23:08 2014 +0200
+++ b/src/HOL/Probability/Finite_Product_Measure.thy Mon May 19 16:14:08 2014 +0200
@@ -688,15 +688,15 @@
"(\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets (M i)) \<Longrightarrow> emeasure (Pi\<^sub>M I M) (Pi\<^sub>E I A) = (\<Prod>i\<in>I. emeasure (M i) (A i))"
using emeasure_PiM[OF finite_index] by auto
-lemma (in product_sigma_finite) positive_integral_empty:
+lemma (in product_sigma_finite) nn_integral_empty:
assumes pos: "0 \<le> f (\<lambda>k. undefined)"
- shows "integral\<^sup>P (Pi\<^sub>M {} M) f = f (\<lambda>k. undefined)"
+ shows "integral\<^sup>N (Pi\<^sub>M {} M) f = f (\<lambda>k. undefined)"
proof -
interpret finite_product_sigma_finite M "{}" by default (fact finite.emptyI)
have "\<And>A. emeasure (Pi\<^sub>M {} M) (Pi\<^sub>E {} A) = 1"
using assms by (subst measure_times) auto
then show ?thesis
- unfolding positive_integral_def simple_function_def simple_integral_def[abs_def]
+ unfolding nn_integral_def simple_function_def simple_integral_def[abs_def]
proof (simp add: space_PiM_empty sets_PiM_empty, intro antisym)
show "f (\<lambda>k. undefined) \<le> (SUP f:{g. g \<le> max 0 \<circ> f}. f (\<lambda>k. undefined))"
by (intro SUP_upper) (auto simp: le_fun_def split: split_max)
@@ -768,10 +768,10 @@
qed
qed
-lemma (in product_sigma_finite) product_positive_integral_fold:
+lemma (in product_sigma_finite) product_nn_integral_fold:
assumes IJ: "I \<inter> J = {}" "finite I" "finite J"
and f: "f \<in> borel_measurable (Pi\<^sub>M (I \<union> J) M)"
- shows "integral\<^sup>P (Pi\<^sub>M (I \<union> J) M) f =
+ shows "integral\<^sup>N (Pi\<^sub>M (I \<union> J) M) f =
(\<integral>\<^sup>+ x. (\<integral>\<^sup>+ y. f (merge I J (x, y)) \<partial>(Pi\<^sub>M J M)) \<partial>(Pi\<^sub>M I M))"
proof -
interpret I: finite_product_sigma_finite M I by default fact
@@ -781,8 +781,8 @@
using measurable_comp[OF measurable_merge f] by (simp add: comp_def)
show ?thesis
apply (subst distr_merge[OF IJ, symmetric])
- apply (subst positive_integral_distr[OF measurable_merge f])
- apply (subst J.positive_integral_fst[symmetric, OF P_borel])
+ apply (subst nn_integral_distr[OF measurable_merge f])
+ apply (subst J.nn_integral_fst[symmetric, OF P_borel])
apply simp
done
qed
@@ -799,30 +799,30 @@
by (simp add: emeasure_distr measurable_component_singleton)
qed simp
-lemma (in product_sigma_finite) product_positive_integral_singleton:
+lemma (in product_sigma_finite) product_nn_integral_singleton:
assumes f: "f \<in> borel_measurable (M i)"
- shows "integral\<^sup>P (Pi\<^sub>M {i} M) (\<lambda>x. f (x i)) = integral\<^sup>P (M i) f"
+ shows "integral\<^sup>N (Pi\<^sub>M {i} M) (\<lambda>x. f (x i)) = integral\<^sup>N (M i) f"
proof -
interpret I: finite_product_sigma_finite M "{i}" by default simp
from f show ?thesis
apply (subst distr_singleton[symmetric])
- apply (subst positive_integral_distr[OF measurable_component_singleton])
+ apply (subst nn_integral_distr[OF measurable_component_singleton])
apply simp_all
done
qed
-lemma (in product_sigma_finite) product_positive_integral_insert:
+lemma (in product_sigma_finite) product_nn_integral_insert:
assumes I[simp]: "finite I" "i \<notin> I"
and f: "f \<in> borel_measurable (Pi\<^sub>M (insert i I) M)"
- shows "integral\<^sup>P (Pi\<^sub>M (insert i I) M) f = (\<integral>\<^sup>+ x. (\<integral>\<^sup>+ y. f (x(i := y)) \<partial>(M i)) \<partial>(Pi\<^sub>M I M))"
+ shows "integral\<^sup>N (Pi\<^sub>M (insert i I) M) f = (\<integral>\<^sup>+ x. (\<integral>\<^sup>+ y. f (x(i := y)) \<partial>(M i)) \<partial>(Pi\<^sub>M I M))"
proof -
interpret I: finite_product_sigma_finite M I by default auto
interpret i: finite_product_sigma_finite M "{i}" by default auto
have IJ: "I \<inter> {i} = {}" and insert: "I \<union> {i} = insert i I"
using f by auto
show ?thesis
- unfolding product_positive_integral_fold[OF IJ, unfolded insert, OF I(1) i.finite_index f]
- proof (rule positive_integral_cong, subst product_positive_integral_singleton[symmetric])
+ unfolding product_nn_integral_fold[OF IJ, unfolded insert, OF I(1) i.finite_index f]
+ proof (rule nn_integral_cong, subst product_nn_integral_singleton[symmetric])
fix x assume x: "x \<in> space (Pi\<^sub>M I M)"
let ?f = "\<lambda>y. f (x(i := y))"
show "?f \<in> borel_measurable (M i)"
@@ -830,16 +830,16 @@
unfolding comp_def .
show "(\<integral>\<^sup>+ y. f (merge I {i} (x, y)) \<partial>Pi\<^sub>M {i} M) = (\<integral>\<^sup>+ y. f (x(i := y i)) \<partial>Pi\<^sub>M {i} M)"
using x
- by (auto intro!: positive_integral_cong arg_cong[where f=f]
+ by (auto intro!: nn_integral_cong arg_cong[where f=f]
simp add: space_PiM extensional_def PiE_def)
qed
qed
-lemma (in product_sigma_finite) product_positive_integral_setprod:
+lemma (in product_sigma_finite) product_nn_integral_setprod:
fixes f :: "'i \<Rightarrow> 'a \<Rightarrow> ereal"
assumes "finite I" and borel: "\<And>i. i \<in> I \<Longrightarrow> f i \<in> borel_measurable (M i)"
and pos: "\<And>i x. i \<in> I \<Longrightarrow> 0 \<le> f i x"
- shows "(\<integral>\<^sup>+ x. (\<Prod>i\<in>I. f i (x i)) \<partial>Pi\<^sub>M I M) = (\<Prod>i\<in>I. integral\<^sup>P (M i) (f i))"
+ shows "(\<integral>\<^sup>+ x. (\<Prod>i\<in>I. f i (x i)) \<partial>Pi\<^sub>M I M) = (\<Prod>i\<in>I. integral\<^sup>N (M i) (f i))"
using assms proof induct
case (insert i I)
note `finite I`[intro, simp]
@@ -852,10 +852,10 @@
measurable_comp[OF measurable_component_singleton, unfolded comp_def])
auto
then show ?case
- apply (simp add: product_positive_integral_insert[OF insert(1,2) prod])
- apply (simp add: insert(2-) * pos borel setprod_ereal_pos positive_integral_multc)
- apply (subst positive_integral_cmult)
- apply (auto simp add: pos borel insert(2-) setprod_ereal_pos positive_integral_positive)
+ apply (simp add: product_nn_integral_insert[OF insert(1,2) prod])
+ apply (simp add: insert(2-) * pos borel setprod_ereal_pos nn_integral_multc)
+ apply (subst nn_integral_cmult)
+ apply (auto simp add: pos borel insert(2-) setprod_ereal_pos nn_integral_nonneg)
done
qed (simp add: space_PiM)
@@ -871,9 +871,9 @@
then have "emeasure ?P A = (\<integral>\<^sup>+x. indicator A x \<partial>?P)"
by simp
also have "\<dots> = (\<integral>\<^sup>+x. indicator ((\<lambda>x. \<lambda>i\<in>{i}. x) -` A \<inter> space (M i)) (x i) \<partial>PiM {i} M)"
- by (intro positive_integral_cong) (auto simp: space_PiM indicator_def PiE_def eq)
+ by (intro nn_integral_cong) (auto simp: space_PiM indicator_def PiE_def eq)
also have "\<dots> = emeasure ?D A"
- using A by (simp add: product_positive_integral_singleton emeasure_distr)
+ using A by (simp add: product_nn_integral_singleton emeasure_distr)
finally show "emeasure (Pi\<^sub>M {i} M) A = emeasure ?D A" .
qed simp
@@ -894,7 +894,7 @@
apply (subst distr_merge[symmetric, OF IJ])
apply (subst emeasure_distr[OF measurable_merge A])
apply (subst J.emeasure_pair_measure_alt[OF merge])
- apply (auto intro!: positive_integral_cong arg_cong2[where f=emeasure] simp: space_pair_measure)
+ apply (auto intro!: nn_integral_cong arg_cong2[where f=emeasure] simp: space_pair_measure)
done
show ?B
--- a/src/HOL/Probability/Infinite_Product_Measure.thy Mon May 19 15:23:08 2014 +0200
+++ b/src/HOL/Probability/Infinite_Product_Measure.thy Mon May 19 16:14:08 2014 +0200
@@ -59,7 +59,7 @@
using K J by (subst emeasure_fold_integral) auto
also have "\<dots> = (\<integral>\<^sup>+ y. \<mu>G ((\<lambda>x. merge J (I - J) (y, x)) -` Z \<inter> space (Pi\<^sub>M I M)) \<partial>Pi\<^sub>M J M)"
(is "_ = (\<integral>\<^sup>+x. \<mu>G (?MZ x) \<partial>Pi\<^sub>M J M)")
- proof (intro positive_integral_cong)
+ proof (intro nn_integral_cong)
fix x assume x: "x \<in> space (Pi\<^sub>M J M)"
with K merge_in_G(2)[OF this]
show "emeasure (Pi\<^sub>M (K - J) M) (?M x) = \<mu>G (?MZ x)"
@@ -141,7 +141,7 @@
have "?a / 2^k \<le> \<mu>G (Z n)" using Z by auto
also have "\<dots> \<le> (\<integral>\<^sup>+ x. indicator (?Q n) x + ?a / 2^(k+1) \<partial>Pi\<^sub>M J' M)"
unfolding fold(2)[OF J' `Z n \<in> ?G`]
- proof (intro positive_integral_mono)
+ proof (intro nn_integral_mono)
fix x assume x: "x \<in> space (Pi\<^sub>M J' M)"
then have "?q n x \<le> 1 + 0"
using J' Z fold(3) Z_sets by auto
@@ -153,7 +153,7 @@
qed
also have "\<dots> = emeasure (Pi\<^sub>M J' M) (?Q n) + ?a / 2^(k+1)"
using `0 \<le> ?a` Q_sets J'.emeasure_space_1
- by (subst positive_integral_add) auto
+ by (subst nn_integral_add) auto
finally show "?a / 2^(k+1) \<le> emeasure (Pi\<^sub>M J' M) (?Q n)" using `?a \<le> 1`
by (cases rule: ereal2_cases[of ?a "emeasure (Pi\<^sub>M J' M) (?Q n)"])
(auto simp: field_simps)
--- a/src/HOL/Probability/Information.thy Mon May 19 15:23:08 2014 +0200
+++ b/src/HOL/Probability/Information.thy Mon May 19 16:14:08 2014 +0200
@@ -143,10 +143,10 @@
using D by auto
have D_neg: "(\<integral>\<^sup>+ x. ereal (- D x) \<partial>M) = 0"
- using D by (subst positive_integral_0_iff_AE) auto
+ using D by (subst nn_integral_0_iff_AE) auto
have "(\<integral>\<^sup>+ x. ereal (D x) \<partial>M) = emeasure (density M D) (space M)"
- using D by (simp add: emeasure_density cong: positive_integral_cong)
+ using D by (simp add: emeasure_density cong: nn_integral_cong)
then have D_pos: "(\<integral>\<^sup>+ x. ereal (D x) \<partial>M) = 1"
using N.emeasure_space_1 by simp
@@ -178,11 +178,11 @@
have "emeasure M {x\<in>space M. D x = 1} = (\<integral>\<^sup>+ x. indicator {x\<in>space M. D x = 1} x \<partial>M)"
using D(1) by auto
also have "\<dots> = (\<integral>\<^sup>+ x. ereal (D x) \<partial>M)"
- using disj by (auto intro!: positive_integral_cong_AE simp: indicator_def one_ereal_def)
+ using disj by (auto intro!: nn_integral_cong_AE simp: indicator_def one_ereal_def)
finally have "AE x in M. D x = 1"
using D D_pos by (intro AE_I_eq_1) auto
then have "(\<integral>\<^sup>+x. indicator A x\<partial>M) = (\<integral>\<^sup>+x. ereal (D x) * indicator A x\<partial>M)"
- by (intro positive_integral_cong_AE) (auto simp: one_ereal_def[symmetric])
+ by (intro nn_integral_cong_AE) (auto simp: one_ereal_def[symmetric])
also have "\<dots> = density M D A"
using `A \<in> sets M` D by (simp add: emeasure_density)
finally show False using `A \<in> sets M` `emeasure (density M D) A \<noteq> emeasure M A` by simp
@@ -844,9 +844,9 @@
from X.emeasure_space_1 have "(\<integral>\<^sup>+x. Px x \<partial>MX) = 1"
unfolding distributed_distr_eq_density[OF X] using Px
by (subst (asm) emeasure_density)
- (auto simp: borel_measurable_ereal_iff intro!: integral_cong cong: positive_integral_cong)
+ (auto simp: borel_measurable_ereal_iff intro!: integral_cong cong: nn_integral_cong)
ultimately show False
- by (simp add: positive_integral_cong_AE)
+ by (simp add: nn_integral_cong_AE)
qed
lemma (in information_space) entropy_le:
@@ -876,11 +876,11 @@
have [simp]: "\<And>x. x \<in> space MX \<Longrightarrow> ereal (if Px x = 0 then 0 else 1) = indicator {x \<in> space MX. Px x \<noteq> 0} x"
by (auto simp: one_ereal_def)
have "(\<integral>\<^sup>+ x. max 0 (ereal (- (if Px x = 0 then 0 else 1))) \<partial>MX) = (\<integral>\<^sup>+ x. 0 \<partial>MX)"
- by (intro positive_integral_cong) (auto split: split_max)
+ by (intro nn_integral_cong) (auto split: split_max)
then show "integrable (distr M MX X) (\<lambda>x. 1 / Px x)"
unfolding distributed_distr_eq_density[OF X] using Px
- by (auto simp: positive_integral_density real_integrable_def borel_measurable_ereal_iff fin positive_integral_max_0
- cong: positive_integral_cong)
+ by (auto simp: nn_integral_density real_integrable_def borel_measurable_ereal_iff fin nn_integral_max_0
+ cong: nn_integral_cong)
have "integrable MX (\<lambda>x. Px x * log b (1 / Px x)) =
integrable MX (\<lambda>x. - Px x * log b (Px x))"
using Px
@@ -1084,37 +1084,37 @@
by (intro TP.AE_pair_measure) (auto dest: distributed_real_AE)
have "(\<integral>\<^sup>+ x. ?f x \<partial>?P) \<le> (\<integral>\<^sup>+ (x, y, z). Pxz (x, z) * (Pyz (y, z) / Pz z) \<partial>(S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P))"
- apply (subst positive_integral_density)
+ apply (subst nn_integral_density)
apply simp
apply (rule distributed_AE[OF Pxyz])
apply auto []
- apply (rule positive_integral_mono_AE)
+ apply (rule nn_integral_mono_AE)
using ae5 ae6 ae7 ae8
apply eventually_elim
apply auto
done
also have "\<dots> = (\<integral>\<^sup>+(y, z). \<integral>\<^sup>+ x. ereal (Pxz (x, z)) * ereal (Pyz (y, z) / Pz z) \<partial>S \<partial>T \<Otimes>\<^sub>M P)"
- by (subst STP.positive_integral_snd[symmetric]) (auto simp add: split_beta')
+ by (subst STP.nn_integral_snd[symmetric]) (auto simp add: split_beta')
also have "\<dots> = (\<integral>\<^sup>+x. ereal (Pyz x) * 1 \<partial>T \<Otimes>\<^sub>M P)"
- apply (rule positive_integral_cong_AE)
+ apply (rule nn_integral_cong_AE)
using aeX1 aeX2 aeX3 distributed_AE[OF Pyz] AE_space
apply eventually_elim
proof (case_tac x, simp del: times_ereal.simps add: space_pair_measure)
fix a b assume "Pz b = 0 \<longrightarrow> Pyz (a, b) = 0" "0 \<le> Pz b" "a \<in> space T \<and> b \<in> space P"
"(\<integral>\<^sup>+ x. ereal (Pxz (x, b)) \<partial>S) = ereal (Pz b)" "0 \<le> Pyz (a, b)"
then show "(\<integral>\<^sup>+ x. ereal (Pxz (x, b)) * ereal (Pyz (a, b) / Pz b) \<partial>S) = ereal (Pyz (a, b))"
- by (subst positive_integral_multc)
+ by (subst nn_integral_multc)
(auto split: prod.split)
qed
also have "\<dots> = 1"
using Q.emeasure_space_1 distributed_AE[OF Pyz] distributed_distr_eq_density[OF Pyz]
- by (subst positive_integral_density[symmetric]) auto
+ by (subst nn_integral_density[symmetric]) auto
finally have le1: "(\<integral>\<^sup>+ x. ?f x \<partial>?P) \<le> 1" .
also have "\<dots> < \<infinity>" by simp
finally have fin: "(\<integral>\<^sup>+ x. ?f x \<partial>?P) \<noteq> \<infinity>" by simp
have pos: "(\<integral>\<^sup>+x. ?f x \<partial>?P) \<noteq> 0"
- apply (subst positive_integral_density)
+ apply (subst nn_integral_density)
apply simp
apply (rule distributed_AE[OF Pxyz])
apply auto []
@@ -1123,18 +1123,18 @@
let ?g = "\<lambda>x. ereal (if Pxyz x = 0 then 0 else Pxz (fst x, snd (snd x)) * Pyz (snd x) / Pz (snd (snd x)))"
assume "(\<integral>\<^sup>+x. ?g x \<partial>(S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P)) = 0"
then have "AE x in S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P. ?g x \<le> 0"
- by (intro positive_integral_0_iff_AE[THEN iffD1]) auto
+ by (intro nn_integral_0_iff_AE[THEN iffD1]) auto
then have "AE x in S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P. Pxyz x = 0"
using ae1 ae2 ae3 ae4 ae5 ae6 ae7 ae8 Pxyz[THEN distributed_real_AE]
by eventually_elim (auto split: split_if_asm simp: mult_le_0_iff divide_le_0_iff)
then have "(\<integral>\<^sup>+ x. ereal (Pxyz x) \<partial>S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P) = 0"
- by (subst positive_integral_cong_AE[of _ "\<lambda>x. 0"]) auto
+ by (subst nn_integral_cong_AE[of _ "\<lambda>x. 0"]) auto
with P.emeasure_space_1 show False
- by (subst (asm) emeasure_density) (auto cong: positive_integral_cong)
+ by (subst (asm) emeasure_density) (auto cong: nn_integral_cong)
qed
have neg: "(\<integral>\<^sup>+ x. - ?f x \<partial>?P) = 0"
- apply (rule positive_integral_0_iff_AE[THEN iffD2])
+ apply (rule nn_integral_0_iff_AE[THEN iffD2])
apply simp
apply (subst AE_density)
apply simp
@@ -1160,14 +1160,14 @@
by simp
qed simp
then have "(\<integral>\<^sup>+ x. ?f x \<partial>?P) = (\<integral>x. ?f x \<partial>?P)"
- apply (rule positive_integral_eq_integral)
+ apply (rule nn_integral_eq_integral)
apply (subst AE_density)
apply simp
using ae5 ae6 ae7 ae8
apply eventually_elim
apply auto
done
- with positive_integral_positive[of ?P ?f] pos le1
+ with nn_integral_nonneg[of ?P ?f] pos le1
show "0 < (\<integral>x. ?f x \<partial>?P)" "(\<integral>x. ?f x \<partial>?P) \<le> 1"
by (simp_all add: one_ereal_def)
qed
@@ -1341,36 +1341,36 @@
using Pz distributed_marginal_eq_joint2[OF P S Pz Pxz]
by (intro TP.AE_pair_measure) (auto dest: distributed_real_AE)
have "(\<integral>\<^sup>+ x. ?f x \<partial>?P) \<le> (\<integral>\<^sup>+ (x, y, z). Pxz (x, z) * (Pyz (y, z) / Pz z) \<partial>(S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P))"
- apply (subst positive_integral_density)
+ apply (subst nn_integral_density)
apply (rule distributed_borel_measurable[OF Pxyz])
apply (rule distributed_AE[OF Pxyz])
apply simp
- apply (rule positive_integral_mono_AE)
+ apply (rule nn_integral_mono_AE)
using ae5 ae6 ae7 ae8
apply eventually_elim
apply auto
done
also have "\<dots> = (\<integral>\<^sup>+(y, z). \<integral>\<^sup>+ x. ereal (Pxz (x, z)) * ereal (Pyz (y, z) / Pz z) \<partial>S \<partial>T \<Otimes>\<^sub>M P)"
- by (subst STP.positive_integral_snd[symmetric]) (auto simp add: split_beta')
+ by (subst STP.nn_integral_snd[symmetric]) (auto simp add: split_beta')
also have "\<dots> = (\<integral>\<^sup>+x. ereal (Pyz x) * 1 \<partial>T \<Otimes>\<^sub>M P)"
- apply (rule positive_integral_cong_AE)
+ apply (rule nn_integral_cong_AE)
using aeX1 aeX2 aeX3 distributed_AE[OF Pyz] AE_space
apply eventually_elim
proof (case_tac x, simp del: times_ereal.simps add: space_pair_measure)
fix a b assume "Pz b = 0 \<longrightarrow> Pyz (a, b) = 0" "0 \<le> Pz b" "a \<in> space T \<and> b \<in> space P"
"(\<integral>\<^sup>+ x. ereal (Pxz (x, b)) \<partial>S) = ereal (Pz b)" "0 \<le> Pyz (a, b)"
then show "(\<integral>\<^sup>+ x. ereal (Pxz (x, b)) * ereal (Pyz (a, b) / Pz b) \<partial>S) = ereal (Pyz (a, b))"
- by (subst positive_integral_multc) auto
+ by (subst nn_integral_multc) auto
qed
also have "\<dots> = 1"
using Q.emeasure_space_1 distributed_AE[OF Pyz] distributed_distr_eq_density[OF Pyz]
- by (subst positive_integral_density[symmetric]) auto
+ by (subst nn_integral_density[symmetric]) auto
finally have le1: "(\<integral>\<^sup>+ x. ?f x \<partial>?P) \<le> 1" .
also have "\<dots> < \<infinity>" by simp
finally have fin: "(\<integral>\<^sup>+ x. ?f x \<partial>?P) \<noteq> \<infinity>" by simp
have pos: "(\<integral>\<^sup>+ x. ?f x \<partial>?P) \<noteq> 0"
- apply (subst positive_integral_density)
+ apply (subst nn_integral_density)
apply simp
apply (rule distributed_AE[OF Pxyz])
apply simp
@@ -1379,18 +1379,18 @@
let ?g = "\<lambda>x. ereal (if Pxyz x = 0 then 0 else Pxz (fst x, snd (snd x)) * Pyz (snd x) / Pz (snd (snd x)))"
assume "(\<integral>\<^sup>+ x. ?g x \<partial>(S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P)) = 0"
then have "AE x in S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P. ?g x \<le> 0"
- by (intro positive_integral_0_iff_AE[THEN iffD1]) (auto intro!: borel_measurable_ereal measurable_If)
+ by (intro nn_integral_0_iff_AE[THEN iffD1]) (auto intro!: borel_measurable_ereal measurable_If)
then have "AE x in S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P. Pxyz x = 0"
using ae1 ae2 ae3 ae4 ae5 ae6 ae7 ae8 Pxyz[THEN distributed_real_AE]
by eventually_elim (auto split: split_if_asm simp: mult_le_0_iff divide_le_0_iff)
then have "(\<integral>\<^sup>+ x. ereal (Pxyz x) \<partial>S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P) = 0"
- by (subst positive_integral_cong_AE[of _ "\<lambda>x. 0"]) auto
+ by (subst nn_integral_cong_AE[of _ "\<lambda>x. 0"]) auto
with P.emeasure_space_1 show False
- by (subst (asm) emeasure_density) (auto cong: positive_integral_cong)
+ by (subst (asm) emeasure_density) (auto cong: nn_integral_cong)
qed
have neg: "(\<integral>\<^sup>+ x. - ?f x \<partial>?P) = 0"
- apply (rule positive_integral_0_iff_AE[THEN iffD2])
+ apply (rule nn_integral_0_iff_AE[THEN iffD2])
apply (auto simp: split_beta') []
apply (subst AE_density)
apply (auto simp: split_beta') []
@@ -1416,14 +1416,14 @@
by simp
qed simp
then have "(\<integral>\<^sup>+ x. ?f x \<partial>?P) = (\<integral>x. ?f x \<partial>?P)"
- apply (rule positive_integral_eq_integral)
+ apply (rule nn_integral_eq_integral)
apply (subst AE_density)
apply simp
using ae5 ae6 ae7 ae8
apply eventually_elim
apply auto
done
- with positive_integral_positive[of ?P ?f] pos le1
+ with nn_integral_nonneg[of ?P ?f] pos le1
show "0 < (\<integral>x. ?f x \<partial>?P)" "(\<integral>x. ?f x \<partial>?P) \<le> 1"
by (simp_all add: one_ereal_def)
qed
--- a/src/HOL/Probability/Lebesgue_Measure.thy Mon May 19 15:23:08 2014 +0200
+++ b/src/HOL/Probability/Lebesgue_Measure.thy Mon May 19 16:14:08 2014 +0200
@@ -544,7 +544,7 @@
by (auto simp: field_simps)
with `0 < c` show ?thesis
by (cases "a \<le> b")
- (auto simp: field_simps emeasure_density positive_integral_distr positive_integral_cmult
+ (auto simp: field_simps emeasure_density nn_integral_distr nn_integral_cmult
borel_measurable_indicator' emeasure_distr)
next
assume "\<not> 0 < c" with `c \<noteq> 0` have "c < 0" by auto
@@ -552,23 +552,23 @@
by (auto simp: field_simps)
with `c < 0` show ?thesis
by (cases "a \<le> b")
- (auto simp: field_simps emeasure_density positive_integral_distr
- positive_integral_cmult borel_measurable_indicator' emeasure_distr)
+ (auto simp: field_simps emeasure_density nn_integral_distr
+ nn_integral_cmult borel_measurable_indicator' emeasure_distr)
qed
qed simp
-lemma positive_integral_real_affine:
+lemma nn_integral_real_affine:
fixes c :: real assumes [measurable]: "f \<in> borel_measurable borel" and c: "c \<noteq> 0"
shows "(\<integral>\<^sup>+x. f x \<partial>lborel) = \<bar>c\<bar> * (\<integral>\<^sup>+x. f (t + c * x) \<partial>lborel)"
by (subst lborel_real_affine[OF c, of t])
- (simp add: positive_integral_density positive_integral_distr positive_integral_cmult)
+ (simp add: nn_integral_density nn_integral_distr nn_integral_cmult)
lemma lborel_integrable_real_affine:
fixes f :: "real \<Rightarrow> _ :: {banach, second_countable_topology}"
assumes f: "integrable lborel f"
shows "c \<noteq> 0 \<Longrightarrow> integrable lborel (\<lambda>x. f (t + c * x))"
using f f[THEN borel_measurable_integrable] unfolding integrable_iff_bounded
- by (subst (asm) positive_integral_real_affine[where c=c and t=t]) auto
+ by (subst (asm) nn_integral_real_affine[where c=c and t=t]) auto
lemma lborel_integrable_real_affine_iff:
fixes f :: "real \<Rightarrow> 'a :: {banach, second_countable_topology}"
@@ -638,7 +638,7 @@
by simp
qed
-lemma positive_integral_has_integral:
+lemma nn_integral_has_integral:
fixes f::"'a::ordered_euclidean_space \<Rightarrow> real"
assumes f: "f \<in> borel_measurable lebesgue" "\<And>x. 0 \<le> f x" "(\<integral>\<^sup>+x. f x \<partial>lebesgue) = ereal r"
shows "(f has_integral r) UNIV"
@@ -648,7 +648,7 @@
next
case (mult g c)
then have "ereal c * (\<integral>\<^sup>+ x. g x \<partial>lebesgue) = ereal r"
- by (subst positive_integral_cmult[symmetric]) auto
+ by (subst nn_integral_cmult[symmetric]) auto
then obtain r' where "(c = 0 \<and> r = 0) \<or> ((\<integral>\<^sup>+ x. ereal (g x) \<partial>lebesgue) = ereal r' \<and> r = c * r')"
by (cases "\<integral>\<^sup>+ x. ereal (g x) \<partial>lebesgue") (auto split: split_if_asm)
with mult show ?case
@@ -657,7 +657,7 @@
case (add g h)
moreover
then have "(\<integral>\<^sup>+ x. h x + g x \<partial>lebesgue) = (\<integral>\<^sup>+ x. h x \<partial>lebesgue) + (\<integral>\<^sup>+ x. g x \<partial>lebesgue)"
- unfolding plus_ereal.simps[symmetric] by (subst positive_integral_add) auto
+ unfolding plus_ereal.simps[symmetric] by (subst nn_integral_add) auto
with add obtain a b where "(\<integral>\<^sup>+ x. h x \<partial>lebesgue) = ereal a" "(\<integral>\<^sup>+ x. g x \<partial>lebesgue) = ereal b" "r = a + b"
by (cases "\<integral>\<^sup>+ x. h x \<partial>lebesgue" "\<integral>\<^sup>+ x. g x \<partial>lebesgue" rule: ereal2_cases) auto
ultimately show ?case
@@ -677,11 +677,11 @@
{ fix i
have "(\<integral>\<^sup>+x. ereal (U i x) \<partial>lebesgue) \<le> (\<integral>\<^sup>+x. ereal (f x) \<partial>lebesgue)"
- using U_le_f by (intro positive_integral_mono) simp
+ using U_le_f by (intro nn_integral_mono) simp
then obtain p where "(\<integral>\<^sup>+x. U i x \<partial>lebesgue) = ereal p" "p \<le> r"
using seq(6) by (cases "\<integral>\<^sup>+x. U i x \<partial>lebesgue") auto
moreover then have "0 \<le> p"
- by (metis ereal_less_eq(5) positive_integral_positive)
+ by (metis ereal_less_eq(5) nn_integral_nonneg)
moreover note seq
ultimately have "\<exists>p. (\<integral>\<^sup>+x. U i x \<partial>lebesgue) = ereal p \<and> 0 \<le> p \<and> p \<le> r \<and> (U i has_integral p) UNIV"
by auto }
@@ -701,7 +701,7 @@
using seq by auto
qed
moreover have "(\<lambda>i. (\<integral>\<^sup>+x. U i x \<partial>lebesgue)) ----> (\<integral>\<^sup>+x. f x \<partial>lebesgue)"
- using seq U_le_f by (intro positive_integral_dominated_convergence[where w=f]) auto
+ using seq U_le_f by (intro nn_integral_dominated_convergence[where w=f]) auto
ultimately have "integral UNIV f = r"
by (auto simp add: int_eq p seq intro: LIMSEQ_unique)
with * show ?case
@@ -712,9 +712,9 @@
fixes f::"'a::ordered_euclidean_space \<Rightarrow> real"
assumes f: "integrable lebesgue f" "\<And>x. 0 \<le> f x"
shows "(f has_integral integral\<^sup>L lebesgue f) UNIV"
-proof (rule positive_integral_has_integral)
+proof (rule nn_integral_has_integral)
show "(\<integral>\<^sup>+ x. ereal (f x) \<partial>lebesgue) = ereal (integral\<^sup>L lebesgue f)"
- using f by (intro positive_integral_eq_integral) auto
+ using f by (intro nn_integral_eq_integral) auto
qed (insert f, auto)
lemma has_integral_lebesgue_integral_lebesgue:
@@ -744,13 +744,13 @@
qed
qed
-lemma lebesgue_positive_integral_eq_borel:
+lemma lebesgue_nn_integral_eq_borel:
assumes f: "f \<in> borel_measurable borel"
- shows "integral\<^sup>P lebesgue f = integral\<^sup>P lborel f"
+ shows "integral\<^sup>N lebesgue f = integral\<^sup>N lborel f"
proof -
- from f have "integral\<^sup>P lebesgue (\<lambda>x. max 0 (f x)) = integral\<^sup>P lborel (\<lambda>x. max 0 (f x))"
- by (auto intro!: positive_integral_subalgebra[symmetric])
- then show ?thesis unfolding positive_integral_max_0 .
+ from f have "integral\<^sup>N lebesgue (\<lambda>x. max 0 (f x)) = integral\<^sup>N lborel (\<lambda>x. max 0 (f x))"
+ by (auto intro!: nn_integral_subalgebra[symmetric])
+ then show ?thesis unfolding nn_integral_max_0 .
qed
lemma lebesgue_integral_eq_borel:
@@ -777,29 +777,29 @@
unfolding lebesgue_integral_eq_borel[OF borel] by simp
qed
-lemma positive_integral_bound_simple_function:
+lemma nn_integral_bound_simple_function:
assumes bnd: "\<And>x. x \<in> space M \<Longrightarrow> 0 \<le> f x" "\<And>x. x \<in> space M \<Longrightarrow> f x < \<infinity>"
assumes f[measurable]: "simple_function M f"
assumes supp: "emeasure M {x\<in>space M. f x \<noteq> 0} < \<infinity>"
- shows "positive_integral M f < \<infinity>"
+ shows "nn_integral M f < \<infinity>"
proof cases
assume "space M = {}"
- then have "positive_integral M f = (\<integral>\<^sup>+x. 0 \<partial>M)"
- by (intro positive_integral_cong) auto
+ then have "nn_integral M f = (\<integral>\<^sup>+x. 0 \<partial>M)"
+ by (intro nn_integral_cong) auto
then show ?thesis by simp
next
assume "space M \<noteq> {}"
with simple_functionD(1)[OF f] bnd have bnd: "0 \<le> Max (f`space M) \<and> Max (f`space M) < \<infinity>"
by (subst Max_less_iff) (auto simp: Max_ge_iff)
- have "positive_integral M f \<le> (\<integral>\<^sup>+x. Max (f`space M) * indicator {x\<in>space M. f x \<noteq> 0} x \<partial>M)"
- proof (rule positive_integral_mono)
+ have "nn_integral M f \<le> (\<integral>\<^sup>+x. Max (f`space M) * indicator {x\<in>space M. f x \<noteq> 0} x \<partial>M)"
+ proof (rule nn_integral_mono)
fix x assume "x \<in> space M"
with f show "f x \<le> Max (f ` space M) * indicator {x \<in> space M. f x \<noteq> 0} x"
by (auto split: split_indicator intro!: Max_ge simple_functionD)
qed
also have "\<dots> < \<infinity>"
- using bnd supp by (subst positive_integral_cmult) auto
+ using bnd supp by (subst nn_integral_cmult) auto
finally show ?thesis .
qed
@@ -814,10 +814,10 @@
from f_borel have "(\<lambda>x. ereal (f x)) \<in> borel_measurable lebesgue" by auto
from borel_measurable_implies_simple_function_sequence'[OF this] guess F . note F = this
- have "(\<integral>\<^sup>+ x. ereal (f x) \<partial>lebesgue) = (SUP i. integral\<^sup>P lebesgue (F i))"
+ have "(\<integral>\<^sup>+ x. ereal (f x) \<partial>lebesgue) = (SUP i. integral\<^sup>N lebesgue (F i))"
using F
- by (subst positive_integral_monotone_convergence_SUP[symmetric])
- (simp_all add: positive_integral_max_0 borel_measurable_simple_function)
+ by (subst nn_integral_monotone_convergence_SUP[symmetric])
+ (simp_all add: nn_integral_max_0 borel_measurable_simple_function)
also have "\<dots> \<le> ereal I"
proof (rule SUP_least)
fix i :: nat
@@ -873,7 +873,7 @@
unfolding integrable_iff_bounded
proof
have "(\<integral>\<^sup>+x. F i x \<partial>lebesgue) < \<infinity>"
- proof (rule positive_integral_bound_simple_function)
+ proof (rule nn_integral_bound_simple_function)
fix x::'a assume "x \<in> space lebesgue" then show "0 \<le> F i x" "F i x < \<infinity>"
using F by (auto simp: image_iff eq_commute)
next
@@ -890,9 +890,9 @@
by (rule has_integral_lebesgue_integral_lebesgue)
from this I have "integral\<^sup>L lebesgue (\<lambda>x. real (F i x)) \<le> I"
by (rule has_integral_le) (intro ballI F_bound)
- moreover have "integral\<^sup>P lebesgue (F i) = integral\<^sup>L lebesgue (\<lambda>x. real (F i x))"
- using int F by (subst positive_integral_eq_integral[symmetric]) (auto simp: F_eq2[symmetric] real_of_ereal_pos)
- ultimately show "integral\<^sup>P lebesgue (F i) \<le> ereal I"
+ moreover have "integral\<^sup>N lebesgue (F i) = integral\<^sup>L lebesgue (\<lambda>x. real (F i x))"
+ using int F by (subst nn_integral_eq_integral[symmetric]) (auto simp: F_eq2[symmetric] real_of_ereal_pos)
+ ultimately show "integral\<^sup>N lebesgue (F i) \<le> ereal I"
by simp
qed
finally show "integrable lebesgue f"
@@ -1003,8 +1003,8 @@
lemma borel_fubini_positiv_integral:
fixes f :: "'a::ordered_euclidean_space \<Rightarrow> ereal"
assumes f: "f \<in> borel_measurable borel"
- shows "integral\<^sup>P lborel f = \<integral>\<^sup>+x. f (p2e x) \<partial>(\<Pi>\<^sub>M (i::'a)\<in>Basis. lborel)"
- by (subst lborel_eq_lborel_space) (simp add: positive_integral_distr measurable_p2e f)
+ shows "integral\<^sup>N lborel f = \<integral>\<^sup>+x. f (p2e x) \<partial>(\<Pi>\<^sub>M (i::'a)\<in>Basis. lborel)"
+ by (subst lborel_eq_lborel_space) (simp add: nn_integral_distr measurable_p2e f)
lemma borel_fubini_integrable:
fixes f :: "'a::ordered_euclidean_space \<Rightarrow> _::{banach, second_countable_topology}"
@@ -1125,21 +1125,21 @@
by (intro integrable_has_integral_nonneg) (auto split: split_indicator)
qed
-lemma positive_integral_FTC_atLeastAtMost:
+lemma nn_integral_FTC_atLeastAtMost:
assumes "f \<in> borel_measurable borel" "\<And>x. x \<in> {a..b} \<Longrightarrow> DERIV F x :> f x" "\<And>x. x \<in> {a..b} \<Longrightarrow> 0 \<le> f x" "a \<le> b"
shows "(\<integral>\<^sup>+x. f x * indicator {a .. b} x \<partial>lborel) = F b - F a"
proof -
have "integrable lborel (\<lambda>x. f x * indicator {a .. b} x)"
by (rule integrable_FTC_Icc_nonneg) fact+
then have "(\<integral>\<^sup>+x. f x * indicator {a .. b} x \<partial>lborel) = (\<integral>x. f x * indicator {a .. b} x \<partial>lborel)"
- using assms by (intro positive_integral_eq_integral) (auto simp: indicator_def)
+ using assms by (intro nn_integral_eq_integral) (auto simp: indicator_def)
also have "(\<integral>x. f x * indicator {a .. b} x \<partial>lborel) = F b - F a"
by (rule integral_FTC_Icc_nonneg) fact+
finally show ?thesis
unfolding ereal_indicator[symmetric] by simp
qed
-lemma positive_integral_FTC_atLeast:
+lemma nn_integral_FTC_atLeast:
fixes f :: "real \<Rightarrow> real"
assumes f_borel: "f \<in> borel_measurable borel"
assumes f: "\<And>x. a \<le> x \<Longrightarrow> DERIV F x :> f x"
@@ -1161,10 +1161,10 @@
then show "(\<lambda>n. ?f n x) ----> ?fR x"
by (rule Lim_eventually)
qed
- then have "integral\<^sup>P lborel ?fR = (\<integral>\<^sup>+ x. (SUP i::nat. ?f i x) \<partial>lborel)"
+ then have "integral\<^sup>N lborel ?fR = (\<integral>\<^sup>+ x. (SUP i::nat. ?f i x) \<partial>lborel)"
by simp
also have "\<dots> = (SUP i::nat. (\<integral>\<^sup>+ x. ?f i x \<partial>lborel))"
- proof (rule positive_integral_monotone_convergence_SUP)
+ proof (rule nn_integral_monotone_convergence_SUP)
show "incseq ?f"
using nonneg by (auto simp: incseq_def le_fun_def split: split_indicator)
show "\<And>i. (?f i) \<in> borel_measurable lborel"
@@ -1173,7 +1173,7 @@
using nonneg by (auto split: split_indicator)
qed
also have "\<dots> = (SUP i::nat. ereal (F (a + real i) - F a))"
- by (subst positive_integral_FTC_atLeastAtMost[OF f_borel f nonneg]) auto
+ by (subst nn_integral_FTC_atLeastAtMost[OF f_borel f nonneg]) auto
also have "\<dots> = T - F a"
proof (rule SUP_Lim_ereal)
show "incseq (\<lambda>n. ereal (F (a + real n) - F a))"
--- a/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy Mon May 19 15:23:08 2014 +0200
+++ b/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy Mon May 19 16:14:08 2014 +0200
@@ -17,7 +17,7 @@
text {*
-Our simple functions are not restricted to positive real numbers. Instead
+Our simple functions are not restricted to nonnegative real numbers. Instead
they are just functions with a finite range and are measurable when singleton
sets are measurable.
@@ -725,7 +725,7 @@
using simple_integral_mult[OF simple_function_indicator[OF A]]
unfolding simple_integral_indicator_only[OF A] by simp
-lemma simple_integral_positive:
+lemma simple_integral_nonneg:
assumes f: "simple_function M f" and ae: "AE x in M. 0 \<le> f x"
shows "0 \<le> integral\<^sup>S M f"
proof -
@@ -736,26 +736,26 @@
subsection {* Integral on nonnegative functions *}
-definition positive_integral :: "'a measure \<Rightarrow> ('a \<Rightarrow> ereal) \<Rightarrow> ereal" ("integral\<^sup>P") where
- "integral\<^sup>P M f = (SUP g : {g. simple_function M g \<and> g \<le> max 0 \<circ> f}. integral\<^sup>S M g)"
+definition nn_integral :: "'a measure \<Rightarrow> ('a \<Rightarrow> ereal) \<Rightarrow> ereal" ("integral\<^sup>N") where
+ "integral\<^sup>N M f = (SUP g : {g. simple_function M g \<and> g \<le> max 0 \<circ> f}. integral\<^sup>S M g)"
syntax
- "_positive_integral" :: "pttrn \<Rightarrow> ereal \<Rightarrow> 'a measure \<Rightarrow> ereal" ("\<integral>\<^sup>+ _. _ \<partial>_" [60,61] 110)
+ "_nn_integral" :: "pttrn \<Rightarrow> ereal \<Rightarrow> 'a measure \<Rightarrow> ereal" ("\<integral>\<^sup>+ _. _ \<partial>_" [60,61] 110)
translations
- "\<integral>\<^sup>+ x. f \<partial>M" == "CONST positive_integral M (%x. f)"
+ "\<integral>\<^sup>+x. f \<partial>M" == "CONST nn_integral M (\<lambda>x. f)"
-lemma positive_integral_positive:
- "0 \<le> integral\<^sup>P M f"
- by (auto intro!: SUP_upper2[of "\<lambda>x. 0"] simp: positive_integral_def le_fun_def)
+lemma nn_integral_nonneg:
+ "0 \<le> integral\<^sup>N M f"
+ by (auto intro!: SUP_upper2[of "\<lambda>x. 0"] simp: nn_integral_def le_fun_def)
-lemma positive_integral_not_MInfty[simp]: "integral\<^sup>P M f \<noteq> -\<infinity>"
- using positive_integral_positive[of M f] by auto
+lemma nn_integral_not_MInfty[simp]: "integral\<^sup>N M f \<noteq> -\<infinity>"
+ using nn_integral_nonneg[of M f] by auto
-lemma positive_integral_def_finite:
- "integral\<^sup>P M f = (SUP g : {g. simple_function M g \<and> g \<le> max 0 \<circ> f \<and> range g \<subseteq> {0 ..< \<infinity>}}. integral\<^sup>S M g)"
+lemma nn_integral_def_finite:
+ "integral\<^sup>N M f = (SUP g : {g. simple_function M g \<and> g \<le> max 0 \<circ> f \<and> range g \<subseteq> {0 ..< \<infinity>}}. integral\<^sup>S M g)"
(is "_ = SUPREMUM ?A ?f")
- unfolding positive_integral_def
+ unfolding nn_integral_def
proof (safe intro!: antisym SUP_least)
fix g assume g: "simple_function M g" "g \<le> max 0 \<circ> f"
let ?G = "{x \<in> space M. \<not> g x \<noteq> \<infinity>}"
@@ -797,9 +797,9 @@
qed
qed (auto intro: SUP_upper)
-lemma positive_integral_mono_AE:
- assumes ae: "AE x in M. u x \<le> v x" shows "integral\<^sup>P M u \<le> integral\<^sup>P M v"
- unfolding positive_integral_def
+lemma nn_integral_mono_AE:
+ assumes ae: "AE x in M. u x \<le> v x" shows "integral\<^sup>N M u \<le> integral\<^sup>N M v"
+ unfolding nn_integral_def
proof (safe intro!: SUP_mono)
fix n assume n: "simple_function M n" "n \<le> max 0 \<circ> u"
from ae[THEN AE_E] guess N . note N = this
@@ -822,57 +822,57 @@
by force
qed
-lemma positive_integral_mono:
- "(\<And>x. x \<in> space M \<Longrightarrow> u x \<le> v x) \<Longrightarrow> integral\<^sup>P M u \<le> integral\<^sup>P M v"
- by (auto intro: positive_integral_mono_AE)
+lemma nn_integral_mono:
+ "(\<And>x. x \<in> space M \<Longrightarrow> u x \<le> v x) \<Longrightarrow> integral\<^sup>N M u \<le> integral\<^sup>N M v"
+ by (auto intro: nn_integral_mono_AE)
-lemma positive_integral_cong_AE:
- "AE x in M. u x = v x \<Longrightarrow> integral\<^sup>P M u = integral\<^sup>P M v"
- by (auto simp: eq_iff intro!: positive_integral_mono_AE)
+lemma nn_integral_cong_AE:
+ "AE x in M. u x = v x \<Longrightarrow> integral\<^sup>N M u = integral\<^sup>N M v"
+ by (auto simp: eq_iff intro!: nn_integral_mono_AE)
-lemma positive_integral_cong:
- "(\<And>x. x \<in> space M \<Longrightarrow> u x = v x) \<Longrightarrow> integral\<^sup>P M u = integral\<^sup>P M v"
- by (auto intro: positive_integral_cong_AE)
+lemma nn_integral_cong:
+ "(\<And>x. x \<in> space M \<Longrightarrow> u x = v x) \<Longrightarrow> integral\<^sup>N M u = integral\<^sup>N M v"
+ by (auto intro: nn_integral_cong_AE)
-lemma positive_integral_cong_strong:
- "M = N \<Longrightarrow> (\<And>x. x \<in> space M \<Longrightarrow> u x = v x) \<Longrightarrow> integral\<^sup>P M u = integral\<^sup>P N v"
- by (auto intro: positive_integral_cong)
+lemma nn_integral_cong_strong:
+ "M = N \<Longrightarrow> (\<And>x. x \<in> space M \<Longrightarrow> u x = v x) \<Longrightarrow> integral\<^sup>N M u = integral\<^sup>N N v"
+ by (auto intro: nn_integral_cong)
-lemma positive_integral_eq_simple_integral:
- assumes f: "simple_function M f" "\<And>x. 0 \<le> f x" shows "integral\<^sup>P M f = integral\<^sup>S M f"
+lemma nn_integral_eq_simple_integral:
+ assumes f: "simple_function M f" "\<And>x. 0 \<le> f x" shows "integral\<^sup>N M f = integral\<^sup>S M f"
proof -
let ?f = "\<lambda>x. f x * indicator (space M) x"
have f': "simple_function M ?f" using f by auto
with f(2) have [simp]: "max 0 \<circ> ?f = ?f"
by (auto simp: fun_eq_iff max_def split: split_indicator)
- have "integral\<^sup>P M ?f \<le> integral\<^sup>S M ?f" using f'
- by (force intro!: SUP_least simple_integral_mono simp: le_fun_def positive_integral_def)
- moreover have "integral\<^sup>S M ?f \<le> integral\<^sup>P M ?f"
- unfolding positive_integral_def
+ have "integral\<^sup>N M ?f \<le> integral\<^sup>S M ?f" using f'
+ by (force intro!: SUP_least simple_integral_mono simp: le_fun_def nn_integral_def)
+ moreover have "integral\<^sup>S M ?f \<le> integral\<^sup>N M ?f"
+ unfolding nn_integral_def
using f' by (auto intro!: SUP_upper)
ultimately show ?thesis
- by (simp cong: positive_integral_cong simple_integral_cong)
+ by (simp cong: nn_integral_cong simple_integral_cong)
qed
-lemma positive_integral_eq_simple_integral_AE:
- assumes f: "simple_function M f" "AE x in M. 0 \<le> f x" shows "integral\<^sup>P M f = integral\<^sup>S M f"
+lemma nn_integral_eq_simple_integral_AE:
+ assumes f: "simple_function M f" "AE x in M. 0 \<le> f x" shows "integral\<^sup>N M f = integral\<^sup>S M f"
proof -
have "AE x in M. f x = max 0 (f x)" using f by (auto split: split_max)
- with f have "integral\<^sup>P M f = integral\<^sup>S M (\<lambda>x. max 0 (f x))"
- by (simp cong: positive_integral_cong_AE simple_integral_cong_AE
- add: positive_integral_eq_simple_integral)
+ with f have "integral\<^sup>N M f = integral\<^sup>S M (\<lambda>x. max 0 (f x))"
+ by (simp cong: nn_integral_cong_AE simple_integral_cong_AE
+ add: nn_integral_eq_simple_integral)
with assms show ?thesis
by (auto intro!: simple_integral_cong_AE split: split_max)
qed
-lemma positive_integral_SUP_approx:
+lemma nn_integral_SUP_approx:
assumes f: "incseq f" "\<And>i. f i \<in> borel_measurable M" "\<And>i x. 0 \<le> f i x"
and u: "simple_function M u" "u \<le> (SUP i. f i)" "u`space M \<subseteq> {0..<\<infinity>}"
- shows "integral\<^sup>S M u \<le> (SUP i. integral\<^sup>P M (f i))" (is "_ \<le> ?S")
+ shows "integral\<^sup>S M u \<le> (SUP i. integral\<^sup>N M (f i))" (is "_ \<le> ?S")
proof (rule ereal_le_mult_one_interval)
- have "0 \<le> (SUP i. integral\<^sup>P M (f i))"
- using f(3) by (auto intro!: SUP_upper2 positive_integral_positive)
- then show "(SUP i. integral\<^sup>P M (f i)) \<noteq> -\<infinity>" by auto
+ have "0 \<le> (SUP i. integral\<^sup>N M (f i))"
+ using f(3) by (auto intro!: SUP_upper2 nn_integral_nonneg)
+ then show "(SUP i. integral\<^sup>N M (f i)) \<noteq> -\<infinity>" by auto
have u_range: "\<And>x. x \<in> space M \<Longrightarrow> 0 \<le> u x \<and> u x \<noteq> \<infinity>"
using u(3) by auto
fix a :: ereal assume "0 < a" "a < 1"
@@ -940,55 +940,55 @@
have "a * integral\<^sup>S M (?uB i) = (\<integral>\<^sup>Sx. a * ?uB i x \<partial>M)"
using B `simple_function M u` u_range
by (subst simple_integral_mult) (auto split: split_indicator)
- also have "\<dots> \<le> integral\<^sup>P M (f i)"
+ also have "\<dots> \<le> integral\<^sup>N M (f i)"
proof -
have *: "simple_function M (\<lambda>x. a * ?uB i x)" using B `0 < a` u(1) by auto
show ?thesis using f(3) * u_range `0 < a`
- by (subst positive_integral_eq_simple_integral[symmetric])
- (auto intro!: positive_integral_mono split: split_indicator)
+ by (subst nn_integral_eq_simple_integral[symmetric])
+ (auto intro!: nn_integral_mono split: split_indicator)
qed
- finally show "a * integral\<^sup>S M (?uB i) \<le> integral\<^sup>P M (f i)"
+ finally show "a * integral\<^sup>S M (?uB i) \<le> integral\<^sup>N M (f i)"
by auto
next
fix i show "0 \<le> \<integral>\<^sup>S x. ?uB i x \<partial>M" using B `0 < a` u(1) u_range
- by (intro simple_integral_positive) (auto split: split_indicator)
+ by (intro simple_integral_nonneg) (auto split: split_indicator)
qed (insert `0 < a`, auto)
ultimately show "a * integral\<^sup>S M u \<le> ?S" by simp
qed
-lemma incseq_positive_integral:
- assumes "incseq f" shows "incseq (\<lambda>i. integral\<^sup>P M (f i))"
+lemma incseq_nn_integral:
+ assumes "incseq f" shows "incseq (\<lambda>i. integral\<^sup>N M (f i))"
proof -
have "\<And>i x. f i x \<le> f (Suc i) x"
using assms by (auto dest!: incseq_SucD simp: le_fun_def)
then show ?thesis
- by (auto intro!: incseq_SucI positive_integral_mono)
+ by (auto intro!: incseq_SucI nn_integral_mono)
qed
text {* Beppo-Levi monotone convergence theorem *}
-lemma positive_integral_monotone_convergence_SUP:
+lemma nn_integral_monotone_convergence_SUP:
assumes f: "incseq f" "\<And>i. f i \<in> borel_measurable M" "\<And>i x. 0 \<le> f i x"
- shows "(\<integral>\<^sup>+ x. (SUP i. f i x) \<partial>M) = (SUP i. integral\<^sup>P M (f i))"
+ shows "(\<integral>\<^sup>+ x. (SUP i. f i x) \<partial>M) = (SUP i. integral\<^sup>N M (f i))"
proof (rule antisym)
- show "(SUP j. integral\<^sup>P M (f j)) \<le> (\<integral>\<^sup>+ x. (SUP i. f i x) \<partial>M)"
- by (auto intro!: SUP_least SUP_upper positive_integral_mono)
+ show "(SUP j. integral\<^sup>N M (f j)) \<le> (\<integral>\<^sup>+ x. (SUP i. f i x) \<partial>M)"
+ by (auto intro!: SUP_least SUP_upper nn_integral_mono)
next
- show "(\<integral>\<^sup>+ x. (SUP i. f i x) \<partial>M) \<le> (SUP j. integral\<^sup>P M (f j))"
- unfolding positive_integral_def_finite[of _ "\<lambda>x. SUP i. f i x"]
+ show "(\<integral>\<^sup>+ x. (SUP i. f i x) \<partial>M) \<le> (SUP j. integral\<^sup>N M (f j))"
+ unfolding nn_integral_def_finite[of _ "\<lambda>x. SUP i. f i x"]
proof (safe intro!: SUP_least)
fix g assume g: "simple_function M g"
and *: "g \<le> max 0 \<circ> (\<lambda>x. SUP i. f i x)" "range g \<subseteq> {0..<\<infinity>}"
then have "\<And>x. 0 \<le> (SUP i. f i x)" and g': "g`space M \<subseteq> {0..<\<infinity>}"
using f by (auto intro!: SUP_upper2)
- with * show "integral\<^sup>S M g \<le> (SUP j. integral\<^sup>P M (f j))"
- by (intro positive_integral_SUP_approx[OF f g _ g'])
+ with * show "integral\<^sup>S M g \<le> (SUP j. integral\<^sup>N M (f j))"
+ by (intro nn_integral_SUP_approx[OF f g _ g'])
(auto simp: le_fun_def max_def)
qed
qed
-lemma positive_integral_monotone_convergence_SUP_AE:
+lemma nn_integral_monotone_convergence_SUP_AE:
assumes f: "\<And>i. AE x in M. f i x \<le> f (Suc i) x \<and> 0 \<le> f i x" "\<And>i. f i \<in> borel_measurable M"
- shows "(\<integral>\<^sup>+ x. (SUP i. f i x) \<partial>M) = (SUP i. integral\<^sup>P M (f i))"
+ shows "(\<integral>\<^sup>+ x. (SUP i. f i x) \<partial>M) = (SUP i. integral\<^sup>N M (f i))"
proof -
from f have "AE x in M. \<forall>i. f i x \<le> f (Suc i) x \<and> 0 \<le> f i x"
by (simp add: AE_all_countable)
@@ -996,9 +996,9 @@
let ?f = "\<lambda>i x. if x \<in> space M - N then f i x else 0"
have f_eq: "AE x in M. \<forall>i. ?f i x = f i x" using N by (auto intro!: AE_I[of _ _ N])
then have "(\<integral>\<^sup>+ x. (SUP i. f i x) \<partial>M) = (\<integral>\<^sup>+ x. (SUP i. ?f i x) \<partial>M)"
- by (auto intro!: positive_integral_cong_AE)
+ by (auto intro!: nn_integral_cong_AE)
also have "\<dots> = (SUP i. (\<integral>\<^sup>+ x. ?f i x \<partial>M))"
- proof (rule positive_integral_monotone_convergence_SUP)
+ proof (rule nn_integral_monotone_convergence_SUP)
show "incseq ?f" using N(1) by (force intro!: incseq_SucI le_funI)
{ fix i show "(\<lambda>x. if x \<in> space M - N then f i x else 0) \<in> borel_measurable M"
using f N(3) by (intro measurable_If_set) auto
@@ -1006,39 +1006,39 @@
using N(1) by auto }
qed
also have "\<dots> = (SUP i. (\<integral>\<^sup>+ x. f i x \<partial>M))"
- using f_eq by (force intro!: arg_cong[where f="SUPREMUM UNIV"] positive_integral_cong_AE ext)
+ using f_eq by (force intro!: arg_cong[where f="SUPREMUM UNIV"] nn_integral_cong_AE ext)
finally show ?thesis .
qed
-lemma positive_integral_monotone_convergence_SUP_AE_incseq:
+lemma nn_integral_monotone_convergence_SUP_AE_incseq:
assumes f: "incseq f" "\<And>i. AE x in M. 0 \<le> f i x" and borel: "\<And>i. f i \<in> borel_measurable M"
- shows "(\<integral>\<^sup>+ x. (SUP i. f i x) \<partial>M) = (SUP i. integral\<^sup>P M (f i))"
+ shows "(\<integral>\<^sup>+ x. (SUP i. f i x) \<partial>M) = (SUP i. integral\<^sup>N M (f i))"
using f[unfolded incseq_Suc_iff le_fun_def]
- by (intro positive_integral_monotone_convergence_SUP_AE[OF _ borel])
+ by (intro nn_integral_monotone_convergence_SUP_AE[OF _ borel])
auto
-lemma positive_integral_monotone_convergence_simple:
+lemma nn_integral_monotone_convergence_simple:
assumes f: "incseq f" "\<And>i x. 0 \<le> f i x" "\<And>i. simple_function M (f i)"
shows "(SUP i. integral\<^sup>S M (f i)) = (\<integral>\<^sup>+x. (SUP i. f i x) \<partial>M)"
- using assms unfolding positive_integral_monotone_convergence_SUP[OF f(1)
+ using assms unfolding nn_integral_monotone_convergence_SUP[OF f(1)
f(3)[THEN borel_measurable_simple_function] f(2)]
- by (auto intro!: positive_integral_eq_simple_integral[symmetric] arg_cong[where f="SUPREMUM UNIV"] ext)
+ by (auto intro!: nn_integral_eq_simple_integral[symmetric] arg_cong[where f="SUPREMUM UNIV"] ext)
-lemma positive_integral_max_0:
- "(\<integral>\<^sup>+x. max 0 (f x) \<partial>M) = integral\<^sup>P M f"
- by (simp add: le_fun_def positive_integral_def)
+lemma nn_integral_max_0:
+ "(\<integral>\<^sup>+x. max 0 (f x) \<partial>M) = integral\<^sup>N M f"
+ by (simp add: le_fun_def nn_integral_def)
-lemma positive_integral_cong_pos:
+lemma nn_integral_cong_pos:
assumes "\<And>x. x \<in> space M \<Longrightarrow> f x \<le> 0 \<and> g x \<le> 0 \<or> f x = g x"
- shows "integral\<^sup>P M f = integral\<^sup>P M g"
+ shows "integral\<^sup>N M f = integral\<^sup>N M g"
proof -
- have "integral\<^sup>P M (\<lambda>x. max 0 (f x)) = integral\<^sup>P M (\<lambda>x. max 0 (g x))"
- proof (intro positive_integral_cong)
+ have "integral\<^sup>N M (\<lambda>x. max 0 (f x)) = integral\<^sup>N M (\<lambda>x. max 0 (g x))"
+ proof (intro nn_integral_cong)
fix x assume "x \<in> space M"
from assms[OF this] show "max 0 (f x) = max 0 (g x)"
by (auto split: split_max)
qed
- then show ?thesis by (simp add: positive_integral_max_0)
+ then show ?thesis by (simp add: nn_integral_max_0)
qed
lemma SUP_simple_integral_sequences:
@@ -1049,40 +1049,40 @@
(is "SUPREMUM _ ?F = SUPREMUM _ ?G")
proof -
have "(SUP i. integral\<^sup>S M (f i)) = (\<integral>\<^sup>+x. (SUP i. f i x) \<partial>M)"
- using f by (rule positive_integral_monotone_convergence_simple)
+ using f by (rule nn_integral_monotone_convergence_simple)
also have "\<dots> = (\<integral>\<^sup>+x. (SUP i. g i x) \<partial>M)"
- unfolding eq[THEN positive_integral_cong_AE] ..
+ unfolding eq[THEN nn_integral_cong_AE] ..
also have "\<dots> = (SUP i. ?G i)"
- using g by (rule positive_integral_monotone_convergence_simple[symmetric])
+ using g by (rule nn_integral_monotone_convergence_simple[symmetric])
finally show ?thesis by simp
qed
-lemma positive_integral_const[simp]:
+lemma nn_integral_const[simp]:
"0 \<le> c \<Longrightarrow> (\<integral>\<^sup>+ x. c \<partial>M) = c * (emeasure M) (space M)"
- by (subst positive_integral_eq_simple_integral) auto
+ by (subst nn_integral_eq_simple_integral) auto
-lemma positive_integral_linear:
+lemma nn_integral_linear:
assumes f: "f \<in> borel_measurable M" "\<And>x. 0 \<le> f x" and "0 \<le> a"
and g: "g \<in> borel_measurable M" "\<And>x. 0 \<le> g x"
- shows "(\<integral>\<^sup>+ x. a * f x + g x \<partial>M) = a * integral\<^sup>P M f + integral\<^sup>P M g"
- (is "integral\<^sup>P M ?L = _")
+ shows "(\<integral>\<^sup>+ x. a * f x + g x \<partial>M) = a * integral\<^sup>N M f + integral\<^sup>N M g"
+ (is "integral\<^sup>N M ?L = _")
proof -
from borel_measurable_implies_simple_function_sequence'[OF f(1)] guess u .
- note u = positive_integral_monotone_convergence_simple[OF this(2,5,1)] this
+ note u = nn_integral_monotone_convergence_simple[OF this(2,5,1)] this
from borel_measurable_implies_simple_function_sequence'[OF g(1)] guess v .
- note v = positive_integral_monotone_convergence_simple[OF this(2,5,1)] this
+ note v = nn_integral_monotone_convergence_simple[OF this(2,5,1)] this
let ?L' = "\<lambda>i x. a * u i x + v i x"
have "?L \<in> borel_measurable M" using assms by auto
from borel_measurable_implies_simple_function_sequence'[OF this] guess l .
- note l = positive_integral_monotone_convergence_simple[OF this(2,5,1)] this
+ note l = nn_integral_monotone_convergence_simple[OF this(2,5,1)] this
have inc: "incseq (\<lambda>i. a * integral\<^sup>S M (u i))" "incseq (\<lambda>i. integral\<^sup>S M (v i))"
using u v `0 \<le> a`
by (auto simp: incseq_Suc_iff le_fun_def
intro!: add_mono ereal_mult_left_mono simple_integral_mono)
have pos: "\<And>i. 0 \<le> integral\<^sup>S M (u i)" "\<And>i. 0 \<le> integral\<^sup>S M (v i)" "\<And>i. 0 \<le> a * integral\<^sup>S M (u i)"
- using u v `0 \<le> a` by (auto simp: simple_integral_positive)
+ using u v `0 \<le> a` by (auto simp: simple_integral_nonneg)
{ fix i from pos[of i] have "a * integral\<^sup>S M (u i) \<noteq> -\<infinity>" "integral\<^sup>S M (v i) \<noteq> -\<infinity>"
by (auto split: split_if_asm) }
note not_MInf = this
@@ -1111,69 +1111,69 @@
unfolding l(1)[symmetric] u(1)[symmetric] v(1)[symmetric]
apply (subst SUP_ereal_cmult [symmetric, OF pos(1) `0 \<le> a`])
apply (subst SUP_ereal_add [symmetric, OF inc not_MInf]) .
- then show ?thesis by (simp add: positive_integral_max_0)
+ then show ?thesis by (simp add: nn_integral_max_0)
qed
-lemma positive_integral_cmult:
+lemma nn_integral_cmult:
assumes f: "f \<in> borel_measurable M" "0 \<le> c"
- shows "(\<integral>\<^sup>+ x. c * f x \<partial>M) = c * integral\<^sup>P M f"
+ shows "(\<integral>\<^sup>+ x. c * f x \<partial>M) = c * integral\<^sup>N M f"
proof -
have [simp]: "\<And>x. c * max 0 (f x) = max 0 (c * f x)" using `0 \<le> c`
by (auto split: split_max simp: ereal_zero_le_0_iff)
have "(\<integral>\<^sup>+ x. c * f x \<partial>M) = (\<integral>\<^sup>+ x. c * max 0 (f x) \<partial>M)"
- by (simp add: positive_integral_max_0)
+ by (simp add: nn_integral_max_0)
then show ?thesis
- using positive_integral_linear[OF _ _ `0 \<le> c`, of "\<lambda>x. max 0 (f x)" _ "\<lambda>x. 0"] f
- by (auto simp: positive_integral_max_0)
+ using nn_integral_linear[OF _ _ `0 \<le> c`, of "\<lambda>x. max 0 (f x)" _ "\<lambda>x. 0"] f
+ by (auto simp: nn_integral_max_0)
qed
-lemma positive_integral_multc:
+lemma nn_integral_multc:
assumes "f \<in> borel_measurable M" "0 \<le> c"
- shows "(\<integral>\<^sup>+ x. f x * c \<partial>M) = integral\<^sup>P M f * c"
- unfolding mult_commute[of _ c] positive_integral_cmult[OF assms] by simp
+ shows "(\<integral>\<^sup>+ x. f x * c \<partial>M) = integral\<^sup>N M f * c"
+ unfolding mult_commute[of _ c] nn_integral_cmult[OF assms] by simp
-lemma positive_integral_indicator[simp]:
+lemma nn_integral_indicator[simp]:
"A \<in> sets M \<Longrightarrow> (\<integral>\<^sup>+ x. indicator A x\<partial>M) = (emeasure M) A"
- by (subst positive_integral_eq_simple_integral)
+ by (subst nn_integral_eq_simple_integral)
(auto simp: simple_integral_indicator)
-lemma positive_integral_cmult_indicator:
+lemma nn_integral_cmult_indicator:
"0 \<le> c \<Longrightarrow> A \<in> sets M \<Longrightarrow> (\<integral>\<^sup>+ x. c * indicator A x \<partial>M) = c * (emeasure M) A"
- by (subst positive_integral_eq_simple_integral)
+ by (subst nn_integral_eq_simple_integral)
(auto simp: simple_function_indicator simple_integral_indicator)
-lemma positive_integral_indicator':
+lemma nn_integral_indicator':
assumes [measurable]: "A \<inter> space M \<in> sets M"
shows "(\<integral>\<^sup>+ x. indicator A x \<partial>M) = emeasure M (A \<inter> space M)"
proof -
have "(\<integral>\<^sup>+ x. indicator A x \<partial>M) = (\<integral>\<^sup>+ x. indicator (A \<inter> space M) x \<partial>M)"
- by (intro positive_integral_cong) (simp split: split_indicator)
+ by (intro nn_integral_cong) (simp split: split_indicator)
also have "\<dots> = emeasure M (A \<inter> space M)"
by simp
finally show ?thesis .
qed
-lemma positive_integral_add:
+lemma nn_integral_add:
assumes f: "f \<in> borel_measurable M" "AE x in M. 0 \<le> f x"
and g: "g \<in> borel_measurable M" "AE x in M. 0 \<le> g x"
- shows "(\<integral>\<^sup>+ x. f x + g x \<partial>M) = integral\<^sup>P M f + integral\<^sup>P M g"
+ shows "(\<integral>\<^sup>+ x. f x + g x \<partial>M) = integral\<^sup>N M f + integral\<^sup>N M g"
proof -
have ae: "AE x in M. max 0 (f x) + max 0 (g x) = max 0 (f x + g x)"
using assms by (auto split: split_max)
have "(\<integral>\<^sup>+ x. f x + g x \<partial>M) = (\<integral>\<^sup>+ x. max 0 (f x + g x) \<partial>M)"
- by (simp add: positive_integral_max_0)
+ by (simp add: nn_integral_max_0)
also have "\<dots> = (\<integral>\<^sup>+ x. max 0 (f x) + max 0 (g x) \<partial>M)"
- unfolding ae[THEN positive_integral_cong_AE] ..
+ unfolding ae[THEN nn_integral_cong_AE] ..
also have "\<dots> = (\<integral>\<^sup>+ x. max 0 (f x) \<partial>M) + (\<integral>\<^sup>+ x. max 0 (g x) \<partial>M)"
- using positive_integral_linear[of "\<lambda>x. max 0 (f x)" _ 1 "\<lambda>x. max 0 (g x)"] f g
+ using nn_integral_linear[of "\<lambda>x. max 0 (f x)" _ 1 "\<lambda>x. max 0 (g x)"] f g
by auto
finally show ?thesis
- by (simp add: positive_integral_max_0)
+ by (simp add: nn_integral_max_0)
qed
-lemma positive_integral_setsum:
+lemma nn_integral_setsum:
assumes "\<And>i. i\<in>P \<Longrightarrow> f i \<in> borel_measurable M" "\<And>i. i\<in>P \<Longrightarrow> AE x in M. 0 \<le> f i x"
- shows "(\<integral>\<^sup>+ x. (\<Sum>i\<in>P. f i x) \<partial>M) = (\<Sum>i\<in>P. integral\<^sup>P M (f i))"
+ shows "(\<integral>\<^sup>+ x. (\<Sum>i\<in>P. f i x) \<partial>M) = (\<Sum>i\<in>P. integral\<^sup>N M (f i))"
proof cases
assume f: "finite P"
from assms have "AE x in M. \<forall>i\<in>P. 0 \<le> f i x" unfolding AE_finite_all[OF f] by auto
@@ -1183,12 +1183,12 @@
then have "f i \<in> borel_measurable M" "AE x in M. 0 \<le> f i x"
"(\<lambda>x. \<Sum>i\<in>P. f i x) \<in> borel_measurable M" "AE x in M. 0 \<le> (\<Sum>i\<in>P. f i x)"
by (auto intro!: setsum_nonneg)
- from positive_integral_add[OF this]
+ from nn_integral_add[OF this]
show ?case using insert by auto
qed simp
qed simp
-lemma positive_integral_Markov_inequality:
+lemma nn_integral_Markov_inequality:
assumes u: "u \<in> borel_measurable M" "AE x in M. 0 \<le> u x" and "A \<in> sets M" and c: "0 \<le> c"
shows "(emeasure M) ({x\<in>space M. 1 \<le> c * u x} \<inter> A) \<le> c * (\<integral>\<^sup>+ x. u x * indicator A x \<partial>M)"
(is "(emeasure M) ?A \<le> _ * ?PI")
@@ -1196,19 +1196,19 @@
have "?A \<in> sets M"
using `A \<in> sets M` u by auto
hence "(emeasure M) ?A = (\<integral>\<^sup>+ x. indicator ?A x \<partial>M)"
- using positive_integral_indicator by simp
+ using nn_integral_indicator by simp
also have "\<dots> \<le> (\<integral>\<^sup>+ x. c * (u x * indicator A x) \<partial>M)" using u c
- by (auto intro!: positive_integral_mono_AE
+ by (auto intro!: nn_integral_mono_AE
simp: indicator_def ereal_zero_le_0_iff)
also have "\<dots> = c * (\<integral>\<^sup>+ x. u x * indicator A x \<partial>M)"
using assms
- by (auto intro!: positive_integral_cmult simp: ereal_zero_le_0_iff)
+ by (auto intro!: nn_integral_cmult simp: ereal_zero_le_0_iff)
finally show ?thesis .
qed
-lemma positive_integral_noteq_infinite:
+lemma nn_integral_noteq_infinite:
assumes g: "g \<in> borel_measurable M" "AE x in M. 0 \<le> g x"
- and "integral\<^sup>P M g \<noteq> \<infinity>"
+ and "integral\<^sup>N M g \<noteq> \<infinity>"
shows "AE x in M. g x \<noteq> \<infinity>"
proof (rule ccontr)
assume c: "\<not> (AE x in M. g x \<noteq> \<infinity>)"
@@ -1218,34 +1218,34 @@
ultimately have "0 < (emeasure M) {x\<in>space M. g x = \<infinity>}" by auto
then have "\<infinity> = \<infinity> * (emeasure M) {x\<in>space M. g x = \<infinity>}" by auto
also have "\<dots> \<le> (\<integral>\<^sup>+x. \<infinity> * indicator {x\<in>space M. g x = \<infinity>} x \<partial>M)"
- using g by (subst positive_integral_cmult_indicator) auto
- also have "\<dots> \<le> integral\<^sup>P M g"
- using assms by (auto intro!: positive_integral_mono_AE simp: indicator_def)
- finally show False using `integral\<^sup>P M g \<noteq> \<infinity>` by auto
+ using g by (subst nn_integral_cmult_indicator) auto
+ also have "\<dots> \<le> integral\<^sup>N M g"
+ using assms by (auto intro!: nn_integral_mono_AE simp: indicator_def)
+ finally show False using `integral\<^sup>N M g \<noteq> \<infinity>` by auto
qed
-lemma positive_integral_PInf:
+lemma nn_integral_PInf:
assumes f: "f \<in> borel_measurable M"
- and not_Inf: "integral\<^sup>P M f \<noteq> \<infinity>"
+ and not_Inf: "integral\<^sup>N M f \<noteq> \<infinity>"
shows "(emeasure M) (f -` {\<infinity>} \<inter> space M) = 0"
proof -
have "\<infinity> * (emeasure M) (f -` {\<infinity>} \<inter> space M) = (\<integral>\<^sup>+ x. \<infinity> * indicator (f -` {\<infinity>} \<inter> space M) x \<partial>M)"
- using f by (subst positive_integral_cmult_indicator) (auto simp: measurable_sets)
- also have "\<dots> \<le> integral\<^sup>P M (\<lambda>x. max 0 (f x))"
- by (auto intro!: positive_integral_mono simp: indicator_def max_def)
- finally have "\<infinity> * (emeasure M) (f -` {\<infinity>} \<inter> space M) \<le> integral\<^sup>P M f"
- by (simp add: positive_integral_max_0)
+ using f by (subst nn_integral_cmult_indicator) (auto simp: measurable_sets)
+ also have "\<dots> \<le> integral\<^sup>N M (\<lambda>x. max 0 (f x))"
+ by (auto intro!: nn_integral_mono simp: indicator_def max_def)
+ finally have "\<infinity> * (emeasure M) (f -` {\<infinity>} \<inter> space M) \<le> integral\<^sup>N M f"
+ by (simp add: nn_integral_max_0)
moreover have "0 \<le> (emeasure M) (f -` {\<infinity>} \<inter> space M)"
by (rule emeasure_nonneg)
ultimately show ?thesis
using assms by (auto split: split_if_asm)
qed
-lemma positive_integral_PInf_AE:
- assumes "f \<in> borel_measurable M" "integral\<^sup>P M f \<noteq> \<infinity>" shows "AE x in M. f x \<noteq> \<infinity>"
+lemma nn_integral_PInf_AE:
+ assumes "f \<in> borel_measurable M" "integral\<^sup>N M f \<noteq> \<infinity>" shows "AE x in M. f x \<noteq> \<infinity>"
proof (rule AE_I)
show "(emeasure M) (f -` {\<infinity>} \<inter> space M) = 0"
- by (rule positive_integral_PInf[OF assms])
+ by (rule nn_integral_PInf[OF assms])
show "f -` {\<infinity>} \<inter> space M \<in> sets M"
using assms by (auto intro: borel_measurable_vimage)
qed auto
@@ -1254,18 +1254,18 @@
assumes "simple_function M f" "\<And>x. 0 \<le> f x"
and "integral\<^sup>S M f \<noteq> \<infinity>"
shows "(emeasure M) (f -` {\<infinity>} \<inter> space M) = 0"
-proof (rule positive_integral_PInf)
+proof (rule nn_integral_PInf)
show "f \<in> borel_measurable M" using assms by (auto intro: borel_measurable_simple_function)
- show "integral\<^sup>P M f \<noteq> \<infinity>"
- using assms by (simp add: positive_integral_eq_simple_integral)
+ show "integral\<^sup>N M f \<noteq> \<infinity>"
+ using assms by (simp add: nn_integral_eq_simple_integral)
qed
-lemma positive_integral_diff:
+lemma nn_integral_diff:
assumes f: "f \<in> borel_measurable M"
and g: "g \<in> borel_measurable M" "AE x in M. 0 \<le> g x"
- and fin: "integral\<^sup>P M g \<noteq> \<infinity>"
+ and fin: "integral\<^sup>N M g \<noteq> \<infinity>"
and mono: "AE x in M. g x \<le> f x"
- shows "(\<integral>\<^sup>+ x. f x - g x \<partial>M) = integral\<^sup>P M f - integral\<^sup>P M g"
+ shows "(\<integral>\<^sup>+ x. f x - g x \<partial>M) = integral\<^sup>N M f - integral\<^sup>N M g"
proof -
have diff: "(\<lambda>x. f x - g x) \<in> borel_measurable M" "AE x in M. 0 \<le> f x - g x"
using assms by (auto intro: ereal_diff_positive)
@@ -1274,61 +1274,61 @@
by (cases rule: ereal2_cases[of a b]) auto }
note * = this
then have "AE x in M. f x = f x - g x + g x"
- using mono positive_integral_noteq_infinite[OF g fin] assms by auto
- then have **: "integral\<^sup>P M f = (\<integral>\<^sup>+x. f x - g x \<partial>M) + integral\<^sup>P M g"
- unfolding positive_integral_add[OF diff g, symmetric]
- by (rule positive_integral_cong_AE)
+ using mono nn_integral_noteq_infinite[OF g fin] assms by auto
+ then have **: "integral\<^sup>N M f = (\<integral>\<^sup>+x. f x - g x \<partial>M) + integral\<^sup>N M g"
+ unfolding nn_integral_add[OF diff g, symmetric]
+ by (rule nn_integral_cong_AE)
show ?thesis unfolding **
- using fin positive_integral_positive[of M g]
- by (cases rule: ereal2_cases[of "\<integral>\<^sup>+ x. f x - g x \<partial>M" "integral\<^sup>P M g"]) auto
+ using fin nn_integral_nonneg[of M g]
+ by (cases rule: ereal2_cases[of "\<integral>\<^sup>+ x. f x - g x \<partial>M" "integral\<^sup>N M g"]) auto
qed
-lemma positive_integral_suminf:
+lemma nn_integral_suminf:
assumes f: "\<And>i. f i \<in> borel_measurable M" "\<And>i. AE x in M. 0 \<le> f i x"
- shows "(\<integral>\<^sup>+ x. (\<Sum>i. f i x) \<partial>M) = (\<Sum>i. integral\<^sup>P M (f i))"
+ shows "(\<integral>\<^sup>+ x. (\<Sum>i. f i x) \<partial>M) = (\<Sum>i. integral\<^sup>N M (f i))"
proof -
have all_pos: "AE x in M. \<forall>i. 0 \<le> f i x"
using assms by (auto simp: AE_all_countable)
- have "(\<Sum>i. integral\<^sup>P M (f i)) = (SUP n. \<Sum>i<n. integral\<^sup>P M (f i))"
- using positive_integral_positive by (rule suminf_ereal_eq_SUP)
+ have "(\<Sum>i. integral\<^sup>N M (f i)) = (SUP n. \<Sum>i<n. integral\<^sup>N M (f i))"
+ using nn_integral_nonneg by (rule suminf_ereal_eq_SUP)
also have "\<dots> = (SUP n. \<integral>\<^sup>+x. (\<Sum>i<n. f i x) \<partial>M)"
- unfolding positive_integral_setsum[OF f] ..
+ unfolding nn_integral_setsum[OF f] ..
also have "\<dots> = \<integral>\<^sup>+x. (SUP n. \<Sum>i<n. f i x) \<partial>M" using f all_pos
- by (intro positive_integral_monotone_convergence_SUP_AE[symmetric])
+ by (intro nn_integral_monotone_convergence_SUP_AE[symmetric])
(elim AE_mp, auto simp: setsum_nonneg simp del: setsum_lessThan_Suc intro!: AE_I2 setsum_mono3)
also have "\<dots> = \<integral>\<^sup>+x. (\<Sum>i. f i x) \<partial>M" using all_pos
- by (intro positive_integral_cong_AE) (auto simp: suminf_ereal_eq_SUP)
+ by (intro nn_integral_cong_AE) (auto simp: suminf_ereal_eq_SUP)
finally show ?thesis by simp
qed
-lemma positive_integral_mult_bounded_inf:
+lemma nn_integral_mult_bounded_inf:
assumes f: "f \<in> borel_measurable M" "(\<integral>\<^sup>+x. f x \<partial>M) < \<infinity>"
and c: "0 \<le> c" "c \<noteq> \<infinity>" and ae: "AE x in M. g x \<le> c * f x"
shows "(\<integral>\<^sup>+x. g x \<partial>M) < \<infinity>"
proof -
have "(\<integral>\<^sup>+x. g x \<partial>M) \<le> (\<integral>\<^sup>+x. c * f x \<partial>M)"
- by (intro positive_integral_mono_AE ae)
+ by (intro nn_integral_mono_AE ae)
also have "(\<integral>\<^sup>+x. c * f x \<partial>M) < \<infinity>"
- using c f by (subst positive_integral_cmult) auto
+ using c f by (subst nn_integral_cmult) auto
finally show ?thesis .
qed
text {* Fatou's lemma: convergence theorem on limes inferior *}
-lemma positive_integral_liminf:
+lemma nn_integral_liminf:
fixes u :: "nat \<Rightarrow> 'a \<Rightarrow> ereal"
assumes u: "\<And>i. u i \<in> borel_measurable M" "\<And>i. AE x in M. 0 \<le> u i x"
- shows "(\<integral>\<^sup>+ x. liminf (\<lambda>n. u n x) \<partial>M) \<le> liminf (\<lambda>n. integral\<^sup>P M (u n))"
+ shows "(\<integral>\<^sup>+ x. liminf (\<lambda>n. u n x) \<partial>M) \<le> liminf (\<lambda>n. integral\<^sup>N M (u n))"
proof -
have pos: "AE x in M. \<forall>i. 0 \<le> u i x" using u by (auto simp: AE_all_countable)
have "(\<integral>\<^sup>+ x. liminf (\<lambda>n. u n x) \<partial>M) =
(SUP n. \<integral>\<^sup>+ x. (INF i:{n..}. u i x) \<partial>M)"
unfolding liminf_SUP_INF using pos u
- by (intro positive_integral_monotone_convergence_SUP_AE)
+ by (intro nn_integral_monotone_convergence_SUP_AE)
(elim AE_mp, auto intro!: AE_I2 intro: INF_greatest INF_superset_mono)
- also have "\<dots> \<le> liminf (\<lambda>n. integral\<^sup>P M (u n))"
+ also have "\<dots> \<le> liminf (\<lambda>n. integral\<^sup>N M (u n))"
unfolding liminf_SUP_INF
- by (auto intro!: SUP_mono exI INF_greatest positive_integral_mono INF_lower)
+ by (auto intro!: SUP_mono exI INF_greatest nn_integral_mono INF_lower)
finally show ?thesis .
qed
@@ -1345,11 +1345,11 @@
shows "c - a \<le> c - b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c < \<infinity> \<Longrightarrow> b \<le> a"
by (cases a b c rule: ereal3_cases) auto
-lemma positive_integral_limsup:
+lemma nn_integral_limsup:
fixes u :: "nat \<Rightarrow> 'a \<Rightarrow> ereal"
assumes [measurable]: "\<And>i. u i \<in> borel_measurable M" "w \<in> borel_measurable M"
assumes bounds: "\<And>i. AE x in M. 0 \<le> u i x" "\<And>i. AE x in M. u i x \<le> w x" and w: "(\<integral>\<^sup>+x. w x \<partial>M) < \<infinity>"
- shows "limsup (\<lambda>n. integral\<^sup>P M (u n)) \<le> (\<integral>\<^sup>+ x. limsup (\<lambda>n. u n x) \<partial>M)"
+ shows "limsup (\<lambda>n. integral\<^sup>N M (u n)) \<le> (\<integral>\<^sup>+ x. limsup (\<lambda>n. u n x) \<partial>M)"
proof -
have bnd: "AE x in M. \<forall>i. 0 \<le> u i x \<and> u i x \<le> w x"
using bounds by (auto simp: AE_all_countable)
@@ -1358,38 +1358,38 @@
by auto
have "(\<integral>\<^sup>+x. w x \<partial>M) - (\<integral>\<^sup>+x. limsup (\<lambda>n. u n x) \<partial>M) = (\<integral>\<^sup>+x. w x - limsup (\<lambda>n. u n x) \<partial>M)"
- proof (intro positive_integral_diff[symmetric])
+ proof (intro nn_integral_diff[symmetric])
show "AE x in M. 0 \<le> limsup (\<lambda>n. u n x)"
using bnd by (auto intro!: le_Limsup)
show "AE x in M. limsup (\<lambda>n. u n x) \<le> w x"
using bnd by (auto intro!: Limsup_le)
then have "(\<integral>\<^sup>+x. limsup (\<lambda>n. u n x) \<partial>M) < \<infinity>"
- by (intro positive_integral_mult_bounded_inf[OF _ w, of 1]) auto
+ by (intro nn_integral_mult_bounded_inf[OF _ w, of 1]) auto
then show "(\<integral>\<^sup>+x. limsup (\<lambda>n. u n x) \<partial>M) \<noteq> \<infinity>"
by simp
qed auto
also have "\<dots> = (\<integral>\<^sup>+x. liminf (\<lambda>n. w x - u n x) \<partial>M)"
using w_nonneg
- by (intro positive_integral_cong_AE, eventually_elim)
+ by (intro nn_integral_cong_AE, eventually_elim)
(auto intro!: liminf_ereal_cminus[symmetric])
also have "\<dots> \<le> liminf (\<lambda>n. \<integral>\<^sup>+x. w x - u n x \<partial>M)"
- proof (rule positive_integral_liminf)
+ proof (rule nn_integral_liminf)
fix i show "AE x in M. 0 \<le> w x - u i x"
using bounds[of i] by eventually_elim (auto intro: ereal_diff_positive)
qed simp
also have "(\<lambda>n. \<integral>\<^sup>+x. w x - u n x \<partial>M) = (\<lambda>n. (\<integral>\<^sup>+x. w x \<partial>M) - (\<integral>\<^sup>+x. u n x \<partial>M))"
- proof (intro ext positive_integral_diff)
+ proof (intro ext nn_integral_diff)
fix i have "(\<integral>\<^sup>+x. u i x \<partial>M) < \<infinity>"
- using bounds by (intro positive_integral_mult_bounded_inf[OF _ w, of 1]) auto
+ using bounds by (intro nn_integral_mult_bounded_inf[OF _ w, of 1]) auto
then show "(\<integral>\<^sup>+x. u i x \<partial>M) \<noteq> \<infinity>" by simp
qed (insert bounds, auto)
also have "liminf (\<lambda>n. (\<integral>\<^sup>+x. w x \<partial>M) - (\<integral>\<^sup>+x. u n x \<partial>M)) = (\<integral>\<^sup>+x. w x \<partial>M) - limsup (\<lambda>n. \<integral>\<^sup>+x. u n x \<partial>M)"
using w by (intro liminf_ereal_cminus) auto
finally show ?thesis
- by (rule ereal_mono_minus_cancel) (intro w positive_integral_positive)+
+ by (rule ereal_mono_minus_cancel) (intro w nn_integral_nonneg)+
qed
-lemma positive_integral_dominated_convergence:
+lemma nn_integral_dominated_convergence:
assumes [measurable]:
"\<And>i. u i \<in> borel_measurable M" "u' \<in> borel_measurable M" "w \<in> borel_measurable M"
and bound: "\<And>j. AE x in M. 0 \<le> u j x" "\<And>j. AE x in M. u j x \<le> w x"
@@ -1397,25 +1397,25 @@
and u': "AE x in M. (\<lambda>i. u i x) ----> u' x"
shows "(\<lambda>i. (\<integral>\<^sup>+x. u i x \<partial>M)) ----> (\<integral>\<^sup>+x. u' x \<partial>M)"
proof -
- have "limsup (\<lambda>n. integral\<^sup>P M (u n)) \<le> (\<integral>\<^sup>+ x. limsup (\<lambda>n. u n x) \<partial>M)"
- by (intro positive_integral_limsup[OF _ _ bound w]) auto
+ have "limsup (\<lambda>n. integral\<^sup>N M (u n)) \<le> (\<integral>\<^sup>+ x. limsup (\<lambda>n. u n x) \<partial>M)"
+ by (intro nn_integral_limsup[OF _ _ bound w]) auto
moreover have "(\<integral>\<^sup>+ x. limsup (\<lambda>n. u n x) \<partial>M) = (\<integral>\<^sup>+ x. u' x \<partial>M)"
- using u' by (intro positive_integral_cong_AE, eventually_elim) (metis tendsto_iff_Liminf_eq_Limsup sequentially_bot)
+ using u' by (intro nn_integral_cong_AE, eventually_elim) (metis tendsto_iff_Liminf_eq_Limsup sequentially_bot)
moreover have "(\<integral>\<^sup>+ x. liminf (\<lambda>n. u n x) \<partial>M) = (\<integral>\<^sup>+ x. u' x \<partial>M)"
- using u' by (intro positive_integral_cong_AE, eventually_elim) (metis tendsto_iff_Liminf_eq_Limsup sequentially_bot)
- moreover have "(\<integral>\<^sup>+x. liminf (\<lambda>n. u n x) \<partial>M) \<le> liminf (\<lambda>n. integral\<^sup>P M (u n))"
- by (intro positive_integral_liminf[OF _ bound(1)]) auto
- moreover have "liminf (\<lambda>n. integral\<^sup>P M (u n)) \<le> limsup (\<lambda>n. integral\<^sup>P M (u n))"
+ using u' by (intro nn_integral_cong_AE, eventually_elim) (metis tendsto_iff_Liminf_eq_Limsup sequentially_bot)
+ moreover have "(\<integral>\<^sup>+x. liminf (\<lambda>n. u n x) \<partial>M) \<le> liminf (\<lambda>n. integral\<^sup>N M (u n))"
+ by (intro nn_integral_liminf[OF _ bound(1)]) auto
+ moreover have "liminf (\<lambda>n. integral\<^sup>N M (u n)) \<le> limsup (\<lambda>n. integral\<^sup>N M (u n))"
by (intro Liminf_le_Limsup sequentially_bot)
ultimately show ?thesis
by (intro Liminf_eq_Limsup) auto
qed
-lemma positive_integral_null_set:
+lemma nn_integral_null_set:
assumes "N \<in> null_sets M" shows "(\<integral>\<^sup>+ x. u x * indicator N x \<partial>M) = 0"
proof -
have "(\<integral>\<^sup>+ x. u x * indicator N x \<partial>M) = (\<integral>\<^sup>+ x. 0 \<partial>M)"
- proof (intro positive_integral_cong_AE AE_I)
+ proof (intro nn_integral_cong_AE AE_I)
show "{x \<in> space M. u x * indicator N x \<noteq> 0} \<subseteq> N"
by (auto simp: indicator_def)
show "(emeasure M) N = 0" "N \<in> sets M"
@@ -1424,29 +1424,29 @@
then show ?thesis by simp
qed
-lemma positive_integral_0_iff:
+lemma nn_integral_0_iff:
assumes u: "u \<in> borel_measurable M" and pos: "AE x in M. 0 \<le> u x"
- shows "integral\<^sup>P M u = 0 \<longleftrightarrow> emeasure M {x\<in>space M. u x \<noteq> 0} = 0"
+ shows "integral\<^sup>N M u = 0 \<longleftrightarrow> emeasure M {x\<in>space M. u x \<noteq> 0} = 0"
(is "_ \<longleftrightarrow> (emeasure M) ?A = 0")
proof -
- have u_eq: "(\<integral>\<^sup>+ x. u x * indicator ?A x \<partial>M) = integral\<^sup>P M u"
- by (auto intro!: positive_integral_cong simp: indicator_def)
+ have u_eq: "(\<integral>\<^sup>+ x. u x * indicator ?A x \<partial>M) = integral\<^sup>N M u"
+ by (auto intro!: nn_integral_cong simp: indicator_def)
show ?thesis
proof
assume "(emeasure M) ?A = 0"
- with positive_integral_null_set[of ?A M u] u
- show "integral\<^sup>P M u = 0" by (simp add: u_eq null_sets_def)
+ with nn_integral_null_set[of ?A M u] u
+ show "integral\<^sup>N M u = 0" by (simp add: u_eq null_sets_def)
next
{ fix r :: ereal and n :: nat assume gt_1: "1 \<le> real n * r"
then have "0 < real n * r" by (cases r) (auto split: split_if_asm simp: one_ereal_def)
then have "0 \<le> r" by (auto simp add: ereal_zero_less_0_iff) }
note gt_1 = this
- assume *: "integral\<^sup>P M u = 0"
+ assume *: "integral\<^sup>N M u = 0"
let ?M = "\<lambda>n. {x \<in> space M. 1 \<le> real (n::nat) * u x}"
have "0 = (SUP n. (emeasure M) (?M n \<inter> ?A))"
proof -
{ fix n :: nat
- from positive_integral_Markov_inequality[OF u pos, of ?A "ereal (real n)"]
+ from nn_integral_Markov_inequality[OF u pos, of ?A "ereal (real n)"]
have "(emeasure M) (?M n \<inter> ?A) \<le> 0" unfolding u_eq * using u by simp
moreover have "0 \<le> (emeasure M) (?M n \<inter> ?A)" using u by auto
ultimately have "(emeasure M) (?M n \<inter> ?A) = 0" by auto }
@@ -1489,33 +1489,33 @@
qed
qed
-lemma positive_integral_0_iff_AE:
+lemma nn_integral_0_iff_AE:
assumes u: "u \<in> borel_measurable M"
- shows "integral\<^sup>P M u = 0 \<longleftrightarrow> (AE x in M. u x \<le> 0)"
+ shows "integral\<^sup>N M u = 0 \<longleftrightarrow> (AE x in M. u x \<le> 0)"
proof -
have sets: "{x\<in>space M. max 0 (u x) \<noteq> 0} \<in> sets M"
using u by auto
- from positive_integral_0_iff[of "\<lambda>x. max 0 (u x)"]
- have "integral\<^sup>P M u = 0 \<longleftrightarrow> (AE x in M. max 0 (u x) = 0)"
- unfolding positive_integral_max_0
+ from nn_integral_0_iff[of "\<lambda>x. max 0 (u x)"]
+ have "integral\<^sup>N M u = 0 \<longleftrightarrow> (AE x in M. max 0 (u x) = 0)"
+ unfolding nn_integral_max_0
using AE_iff_null[OF sets] u by auto
also have "\<dots> \<longleftrightarrow> (AE x in M. u x \<le> 0)" by (auto split: split_max)
finally show ?thesis .
qed
-lemma AE_iff_positive_integral:
- "{x\<in>space M. P x} \<in> sets M \<Longrightarrow> (AE x in M. P x) \<longleftrightarrow> integral\<^sup>P M (indicator {x. \<not> P x}) = 0"
- by (subst positive_integral_0_iff_AE) (auto simp: one_ereal_def zero_ereal_def
+lemma AE_iff_nn_integral:
+ "{x\<in>space M. P x} \<in> sets M \<Longrightarrow> (AE x in M. P x) \<longleftrightarrow> integral\<^sup>N M (indicator {x. \<not> P x}) = 0"
+ by (subst nn_integral_0_iff_AE) (auto simp: one_ereal_def zero_ereal_def
sets.sets_Collect_neg indicator_def[abs_def] measurable_If)
-lemma positive_integral_const_If:
+lemma nn_integral_const_If:
"(\<integral>\<^sup>+x. a \<partial>M) = (if 0 \<le> a then a * (emeasure M) (space M) else 0)"
- by (auto intro!: positive_integral_0_iff_AE[THEN iffD2])
+ by (auto intro!: nn_integral_0_iff_AE[THEN iffD2])
-lemma positive_integral_subalgebra:
+lemma nn_integral_subalgebra:
assumes f: "f \<in> borel_measurable N" "\<And>x. 0 \<le> f x"
and N: "sets N \<subseteq> sets M" "space N = space M" "\<And>A. A \<in> sets N \<Longrightarrow> emeasure N A = emeasure M A"
- shows "integral\<^sup>P N f = integral\<^sup>P M f"
+ shows "integral\<^sup>N N f = integral\<^sup>N M f"
proof -
have [simp]: "\<And>f :: 'a \<Rightarrow> ereal. f \<in> borel_measurable N \<Longrightarrow> f \<in> borel_measurable M"
using N by (auto simp: measurable_def)
@@ -1525,12 +1525,12 @@
using N by auto
from f show ?thesis
apply induct
- apply (simp_all add: positive_integral_add positive_integral_cmult positive_integral_monotone_convergence_SUP N)
- apply (auto intro!: positive_integral_cong cong: positive_integral_cong simp: N(2)[symmetric])
+ apply (simp_all add: nn_integral_add nn_integral_cmult nn_integral_monotone_convergence_SUP N)
+ apply (auto intro!: nn_integral_cong cong: nn_integral_cong simp: N(2)[symmetric])
done
qed
-lemma positive_integral_nat_function:
+lemma nn_integral_nat_function:
fixes f :: "'a \<Rightarrow> nat"
assumes "f \<in> measurable M (count_space UNIV)"
shows "(\<integral>\<^sup>+x. ereal (of_nat (f x)) \<partial>M) = (\<Sum>t. emeasure M {x\<in>space M. t < f x})"
@@ -1549,9 +1549,9 @@
ultimately have "ereal(of_nat(f x)) = (\<Sum>i. indicator (F i) x)"
by (simp add: sums_iff) }
then have "(\<integral>\<^sup>+x. ereal (of_nat (f x)) \<partial>M) = (\<integral>\<^sup>+x. (\<Sum>i. indicator (F i) x) \<partial>M)"
- by (simp cong: positive_integral_cong)
+ by (simp cong: nn_integral_cong)
also have "\<dots> = (\<Sum>i. emeasure M (F i))"
- by (simp add: positive_integral_suminf)
+ by (simp add: nn_integral_suminf)
finally show ?thesis
by (simp add: F_def)
qed
@@ -1560,17 +1560,17 @@
subsubsection {* Distributions *}
-lemma positive_integral_distr':
+lemma nn_integral_distr':
assumes T: "T \<in> measurable M M'"
and f: "f \<in> borel_measurable (distr M M' T)" "\<And>x. 0 \<le> f x"
- shows "integral\<^sup>P (distr M M' T) f = (\<integral>\<^sup>+ x. f (T x) \<partial>M)"
+ shows "integral\<^sup>N (distr M M' T) f = (\<integral>\<^sup>+ x. f (T x) \<partial>M)"
using f
proof induct
case (cong f g)
with T show ?case
- apply (subst positive_integral_cong[of _ f g])
+ apply (subst nn_integral_cong[of _ f g])
apply simp
- apply (subst positive_integral_cong[of _ "\<lambda>x. f (T x)" "\<lambda>x. g (T x)"])
+ apply (subst nn_integral_cong[of _ "\<lambda>x. f (T x)" "\<lambda>x. g (T x)"])
apply (simp add: measurable_def Pi_iff)
apply simp
done
@@ -1579,15 +1579,15 @@
then have eq: "\<And>x. x \<in> space M \<Longrightarrow> indicator A (T x) = indicator (T -` A \<inter> space M) x"
by (auto simp: indicator_def)
from set T show ?case
- by (subst positive_integral_cong[OF eq])
- (auto simp add: emeasure_distr intro!: positive_integral_indicator[symmetric] measurable_sets)
-qed (simp_all add: measurable_compose[OF T] T positive_integral_cmult positive_integral_add
- positive_integral_monotone_convergence_SUP le_fun_def incseq_def)
+ by (subst nn_integral_cong[OF eq])
+ (auto simp add: emeasure_distr intro!: nn_integral_indicator[symmetric] measurable_sets)
+qed (simp_all add: measurable_compose[OF T] T nn_integral_cmult nn_integral_add
+ nn_integral_monotone_convergence_SUP le_fun_def incseq_def)
-lemma positive_integral_distr:
- "T \<in> measurable M M' \<Longrightarrow> f \<in> borel_measurable M' \<Longrightarrow> integral\<^sup>P (distr M M' T) f = (\<integral>\<^sup>+ x. f (T x) \<partial>M)"
- by (subst (1 2) positive_integral_max_0[symmetric])
- (simp add: positive_integral_distr')
+lemma nn_integral_distr:
+ "T \<in> measurable M M' \<Longrightarrow> f \<in> borel_measurable M' \<Longrightarrow> integral\<^sup>N (distr M M' T) f = (\<integral>\<^sup>+ x. f (T x) \<partial>M)"
+ by (subst (1 2) nn_integral_max_0[symmetric])
+ (simp add: nn_integral_distr')
subsubsection {* Counting space *}
@@ -1595,26 +1595,26 @@
"simple_function (count_space A) f \<longleftrightarrow> finite (f ` A)"
unfolding simple_function_def by simp
-lemma positive_integral_count_space:
+lemma nn_integral_count_space:
assumes A: "finite {a\<in>A. 0 < f a}"
- shows "integral\<^sup>P (count_space A) f = (\<Sum>a|a\<in>A \<and> 0 < f a. f a)"
+ shows "integral\<^sup>N (count_space A) f = (\<Sum>a|a\<in>A \<and> 0 < f a. f a)"
proof -
have *: "(\<integral>\<^sup>+x. max 0 (f x) \<partial>count_space A) =
(\<integral>\<^sup>+ x. (\<Sum>a|a\<in>A \<and> 0 < f a. f a * indicator {a} x) \<partial>count_space A)"
- by (auto intro!: positive_integral_cong
+ by (auto intro!: nn_integral_cong
simp add: indicator_def if_distrib setsum_cases[OF A] max_def le_less)
also have "\<dots> = (\<Sum>a|a\<in>A \<and> 0 < f a. \<integral>\<^sup>+ x. f a * indicator {a} x \<partial>count_space A)"
- by (subst positive_integral_setsum)
+ by (subst nn_integral_setsum)
(simp_all add: AE_count_space ereal_zero_le_0_iff less_imp_le)
also have "\<dots> = (\<Sum>a|a\<in>A \<and> 0 < f a. f a)"
- by (auto intro!: setsum_cong simp: positive_integral_cmult_indicator one_ereal_def[symmetric])
- finally show ?thesis by (simp add: positive_integral_max_0)
+ by (auto intro!: setsum_cong simp: nn_integral_cmult_indicator one_ereal_def[symmetric])
+ finally show ?thesis by (simp add: nn_integral_max_0)
qed
-lemma positive_integral_count_space_finite:
+lemma nn_integral_count_space_finite:
"finite A \<Longrightarrow> (\<integral>\<^sup>+x. f x \<partial>count_space A) = (\<Sum>a\<in>A. max 0 (f a))"
- by (subst positive_integral_max_0[symmetric])
- (auto intro!: setsum_mono_zero_left simp: positive_integral_count_space less_le)
+ by (subst nn_integral_max_0[symmetric])
+ (auto intro!: setsum_mono_zero_left simp: nn_integral_count_space less_le)
lemma emeasure_UN_countable:
assumes sets: "\<And>i. i \<in> I \<Longrightarrow> X i \<in> sets M" and I: "countable I"
@@ -1623,7 +1623,7 @@
proof cases
assume "finite I" with sets disj show ?thesis
by (subst setsum_emeasure[symmetric])
- (auto intro!: setsum_cong simp add: max_def subset_eq positive_integral_count_space_finite emeasure_nonneg)
+ (auto intro!: setsum_cong simp add: max_def subset_eq nn_integral_count_space_finite emeasure_nonneg)
next
assume f: "\<not> finite I"
then have [intro]: "I \<noteq> {}" by auto
@@ -1648,15 +1648,15 @@
by (auto simp: ereal_zero_less_0_iff indicator_def from_nat_into `I \<noteq> {}` simp del: ereal_0_less_1)
have "(\<integral>\<^sup>+ ia. emeasure M (X ia) * indicator {from_nat_into I i} ia \<partial>count_space I) =
(if 0 < emeasure M (X (from_nat_into I i)) then emeasure M (X (from_nat_into I i)) else 0)"
- by (subst positive_integral_count_space) (simp_all add: eq)
+ by (subst nn_integral_count_space) (simp_all add: eq)
also have "\<dots> = emeasure M (X (from_nat_into I i))"
by (simp add: less_le emeasure_nonneg)
finally show "emeasure M (X (from_nat_into I i)) =
\<integral>\<^sup>+ ia. emeasure M (X ia) * indicator {from_nat_into I i} ia \<partial>count_space I" ..
qed
also have "\<dots> = (\<integral>\<^sup>+i. emeasure M (X i) \<partial>count_space I)"
- apply (subst positive_integral_suminf[symmetric])
- apply (auto simp: emeasure_nonneg intro!: positive_integral_cong)
+ apply (subst nn_integral_suminf[symmetric])
+ apply (auto simp: emeasure_nonneg intro!: nn_integral_cong)
proof -
fix x assume "x \<in> I"
then have "(\<Sum>i. emeasure M (X x) * indicator {from_nat_into I i} x) = (\<Sum>i\<in>{to_nat_on I x}. emeasure M (X x) * indicator {from_nat_into I i} x)"
@@ -1670,12 +1670,12 @@
subsubsection {* Measures with Restricted Space *}
-lemma positive_integral_restrict_space:
+lemma nn_integral_restrict_space:
assumes \<Omega>: "\<Omega> \<in> sets M" and f: "f \<in> borel_measurable M" "\<And>x. 0 \<le> f x" "\<And>x. x \<in> space M - \<Omega> \<Longrightarrow> f x = 0"
- shows "positive_integral (restrict_space M \<Omega>) f = positive_integral M f"
+ shows "nn_integral (restrict_space M \<Omega>) f = nn_integral M f"
using f proof (induct rule: borel_measurable_induct)
case (cong f g) then show ?case
- using positive_integral_cong[of M f g] positive_integral_cong[of "restrict_space M \<Omega>" f g]
+ using nn_integral_cong[of M f g] nn_integral_cong[of "restrict_space M \<Omega>" f g]
sets.sets_into_space[OF `\<Omega> \<in> sets M`]
by (simp add: subset_eq space_restrict_space)
next
@@ -1683,19 +1683,19 @@
then have "A \<subseteq> \<Omega>"
unfolding indicator_eq_0_iff by (auto dest: sets.sets_into_space)
with set `\<Omega> \<in> sets M` sets.sets_into_space[OF `\<Omega> \<in> sets M`] show ?case
- by (subst positive_integral_indicator')
+ by (subst nn_integral_indicator')
(auto simp add: sets_restrict_space_iff space_restrict_space
emeasure_restrict_space Int_absorb2
dest: sets.sets_into_space)
next
case (mult f c) then show ?case
- by (cases "c = 0") (simp_all add: measurable_restrict_space1 \<Omega> positive_integral_cmult)
+ by (cases "c = 0") (simp_all add: measurable_restrict_space1 \<Omega> nn_integral_cmult)
next
case (add f g) then show ?case
- by (simp add: measurable_restrict_space1 \<Omega> positive_integral_add ereal_add_nonneg_eq_0_iff)
+ by (simp add: measurable_restrict_space1 \<Omega> nn_integral_add ereal_add_nonneg_eq_0_iff)
next
case (seq F) then show ?case
- by (auto simp add: SUP_eq_iff measurable_restrict_space1 \<Omega> positive_integral_monotone_convergence_SUP)
+ by (auto simp add: SUP_eq_iff measurable_restrict_space1 \<Omega> nn_integral_monotone_convergence_SUP)
qed
subsubsection {* Measure spaces with an associated density *}
@@ -1720,14 +1720,14 @@
lemma density_cong: "f \<in> borel_measurable M \<Longrightarrow> f' \<in> borel_measurable M \<Longrightarrow>
(AE x in M. f x = f' x) \<Longrightarrow> density M f = density M f'"
- unfolding density_def by (auto intro!: measure_of_eq positive_integral_cong_AE sets.space_closed)
+ unfolding density_def by (auto intro!: measure_of_eq nn_integral_cong_AE sets.space_closed)
lemma density_max_0: "density M f = density M (\<lambda>x. max 0 (f x))"
proof -
have "\<And>x A. max 0 (f x) * indicator A x = max 0 (f x * indicator A x)"
by (auto simp: indicator_def)
then show ?thesis
- unfolding density_def by (simp add: positive_integral_max_0)
+ unfolding density_def by (simp add: nn_integral_max_0)
qed
lemma density_ereal_max_0: "density M (\<lambda>x. ereal (f x)) = density M (\<lambda>x. ereal (max 0 (f x)))"
@@ -1741,10 +1741,10 @@
proof (rule emeasure_measure_of_sigma)
show "sigma_algebra (space M) (sets M)" ..
show "positive (sets M) ?\<mu>"
- using f by (auto simp: positive_def intro!: positive_integral_positive)
+ using f by (auto simp: positive_def intro!: nn_integral_nonneg)
have \<mu>_eq: "?\<mu> = (\<lambda>A. \<integral>\<^sup>+ x. max 0 (f x) * indicator A x \<partial>M)" (is "?\<mu> = ?\<mu>'")
- apply (subst positive_integral_max_0[symmetric])
- apply (intro ext positive_integral_cong_AE AE_I2)
+ apply (subst nn_integral_max_0[symmetric])
+ apply (intro ext nn_integral_cong_AE AE_I2)
apply (auto simp: indicator_def)
done
show "countably_additive (sets M) ?\<mu>"
@@ -1756,9 +1756,9 @@
by (auto simp: set_eq_iff)
assume disj: "disjoint_family A"
have "(\<Sum>n. ?\<mu>' (A n)) = (\<integral>\<^sup>+ x. (\<Sum>n. max 0 (f x) * indicator (A n) x) \<partial>M)"
- using f * by (simp add: positive_integral_suminf)
+ using f * by (simp add: nn_integral_suminf)
also have "\<dots> = (\<integral>\<^sup>+ x. max 0 (f x) * (\<Sum>n. indicator (A n) x) \<partial>M)" using f
- by (auto intro!: suminf_cmult_ereal positive_integral_cong_AE)
+ by (auto intro!: suminf_cmult_ereal nn_integral_cong_AE)
also have "\<dots> = (\<integral>\<^sup>+ x. max 0 (f x) * indicator (\<Union>n. A n) x \<partial>M)"
unfolding suminf_indicator[OF disj] ..
finally show "(\<Sum>n. ?\<mu>' (A n)) = ?\<mu>' (\<Union>x. A x)" by simp
@@ -1771,15 +1771,15 @@
proof -
{ assume "A \<in> sets M"
have eq: "(\<integral>\<^sup>+x. f x * indicator A x \<partial>M) = (\<integral>\<^sup>+x. max 0 (f x) * indicator A x \<partial>M)"
- apply (subst positive_integral_max_0[symmetric])
- apply (intro positive_integral_cong)
+ apply (subst nn_integral_max_0[symmetric])
+ apply (intro nn_integral_cong)
apply (auto simp: indicator_def)
done
have "(\<integral>\<^sup>+x. f x * indicator A x \<partial>M) = 0 \<longleftrightarrow>
emeasure M {x \<in> space M. max 0 (f x) * indicator A x \<noteq> 0} = 0"
unfolding eq
using f `A \<in> sets M`
- by (intro positive_integral_0_iff) auto
+ by (intro nn_integral_0_iff) auto
also have "\<dots> \<longleftrightarrow> (AE x in M. max 0 (f x) * indicator A x = 0)"
using f `A \<in> sets M`
by (intro AE_iff_measurable[OF _ refl, symmetric]) auto
@@ -1814,15 +1814,15 @@
(auto elim: eventually_elim2)
qed
-lemma positive_integral_density':
+lemma nn_integral_density':
assumes f: "f \<in> borel_measurable M" "AE x in M. 0 \<le> f x"
assumes g: "g \<in> borel_measurable M" "\<And>x. 0 \<le> g x"
- shows "integral\<^sup>P (density M f) g = (\<integral>\<^sup>+ x. f x * g x \<partial>M)"
+ shows "integral\<^sup>N (density M f) g = (\<integral>\<^sup>+ x. f x * g x \<partial>M)"
using g proof induct
case (cong u v)
then show ?case
- apply (subst positive_integral_cong[OF cong(3)])
- apply (simp_all cong: positive_integral_cong)
+ apply (subst nn_integral_cong[OF cong(3)])
+ apply (simp_all cong: nn_integral_cong)
done
next
case (set A) then show ?case
@@ -1831,31 +1831,31 @@
case (mult u c)
moreover have "\<And>x. f x * (c * u x) = c * (f x * u x)" by (simp add: field_simps)
ultimately show ?case
- using f by (simp add: positive_integral_cmult)
+ using f by (simp add: nn_integral_cmult)
next
case (add u v)
then have "\<And>x. f x * (v x + u x) = f x * v x + f x * u x"
by (simp add: ereal_right_distrib)
with add f show ?case
- by (auto simp add: positive_integral_add ereal_zero_le_0_iff intro!: positive_integral_add[symmetric])
+ by (auto simp add: nn_integral_add ereal_zero_le_0_iff intro!: nn_integral_add[symmetric])
next
case (seq U)
from f(2) have eq: "AE x in M. f x * (SUP i. U i x) = (SUP i. f x * U i x)"
by eventually_elim (simp add: SUP_ereal_cmult seq)
from seq f show ?case
- apply (simp add: positive_integral_monotone_convergence_SUP)
- apply (subst positive_integral_cong_AE[OF eq])
- apply (subst positive_integral_monotone_convergence_SUP_AE)
+ apply (simp add: nn_integral_monotone_convergence_SUP)
+ apply (subst nn_integral_cong_AE[OF eq])
+ apply (subst nn_integral_monotone_convergence_SUP_AE)
apply (auto simp: incseq_def le_fun_def intro!: ereal_mult_left_mono)
done
qed
-lemma positive_integral_density:
+lemma nn_integral_density:
"f \<in> borel_measurable M \<Longrightarrow> AE x in M. 0 \<le> f x \<Longrightarrow> g' \<in> borel_measurable M \<Longrightarrow>
- integral\<^sup>P (density M f) g' = (\<integral>\<^sup>+ x. f x * g' x \<partial>M)"
- by (subst (1 2) positive_integral_max_0[symmetric])
- (auto intro!: positive_integral_cong_AE
- simp: measurable_If max_def ereal_zero_le_0_iff positive_integral_density')
+ integral\<^sup>N (density M f) g' = (\<integral>\<^sup>+ x. f x * g' x \<partial>M)"
+ by (subst (1 2) nn_integral_max_0[symmetric])
+ (auto intro!: nn_integral_cong_AE
+ simp: measurable_If max_def ereal_zero_le_0_iff nn_integral_density')
lemma emeasure_restricted:
assumes S: "S \<in> sets M" and X: "X \<in> sets M"
@@ -1864,7 +1864,7 @@
have "emeasure (density M (indicator S)) X = (\<integral>\<^sup>+x. indicator S x * indicator X x \<partial>M)"
using S X by (simp add: emeasure_density)
also have "\<dots> = (\<integral>\<^sup>+x. indicator (S \<inter> X) x \<partial>M)"
- by (auto intro!: positive_integral_cong simp: indicator_def)
+ by (auto intro!: nn_integral_cong simp: indicator_def)
also have "\<dots> = emeasure M (S \<inter> X)"
using S X by (simp add: sets.Int)
finally show ?thesis .
@@ -1880,7 +1880,7 @@
lemma emeasure_density_const:
"A \<in> sets M \<Longrightarrow> 0 \<le> c \<Longrightarrow> emeasure (density M (\<lambda>_. c)) A = c * emeasure M A"
- by (auto simp: positive_integral_cmult_indicator emeasure_density)
+ by (auto simp: nn_integral_cmult_indicator emeasure_density)
lemma measure_density_const:
"A \<in> sets M \<Longrightarrow> 0 < c \<Longrightarrow> c \<noteq> \<infinity> \<Longrightarrow> measure (density M (\<lambda>_. c)) A = real c * measure M A"
@@ -1889,7 +1889,7 @@
lemma density_density_eq:
"f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> AE x in M. 0 \<le> f x \<Longrightarrow>
density (density M f) g = density M (\<lambda>x. f x * g x)"
- by (auto intro!: measure_eqI simp: emeasure_density positive_integral_density ac_simps)
+ by (auto intro!: measure_eqI simp: emeasure_density nn_integral_density ac_simps)
lemma distr_density_distr:
assumes T: "T \<in> measurable M M'" and T': "T' \<in> measurable M' M"
@@ -1904,7 +1904,7 @@
using T inv by (auto simp: indicator_def measurable_space) }
with A T T' f show "emeasure ?R A = emeasure ?L A"
by (simp add: measurable_comp emeasure_density emeasure_distr
- positive_integral_distr measurable_sets cong: positive_integral_cong)
+ nn_integral_distr measurable_sets cong: nn_integral_cong)
qed simp
lemma density_density_divide:
@@ -1951,7 +1951,7 @@
have "{a. (a \<in> X \<longrightarrow> a \<in> A \<and> 0 < f a) \<and> a \<in> X} = {a\<in>X. 0 < f a}"
using `X \<subseteq> A` by auto
with A show ?thesis
- by (simp add: emeasure_density positive_integral_count_space ereal_zero_le_0_iff
+ by (simp add: emeasure_density nn_integral_count_space ereal_zero_le_0_iff
point_measure_def indicator_def)
qed
@@ -1973,14 +1973,14 @@
unfolding point_measure_def
by (subst AE_density) (auto simp: AE_density AE_count_space point_measure_def)
-lemma positive_integral_point_measure:
+lemma nn_integral_point_measure:
"finite {a\<in>A. 0 < f a \<and> 0 < g a} \<Longrightarrow>
- integral\<^sup>P (point_measure A f) g = (\<Sum>a|a\<in>A \<and> 0 < f a \<and> 0 < g a. f a * g a)"
+ integral\<^sup>N (point_measure A f) g = (\<Sum>a|a\<in>A \<and> 0 < f a \<and> 0 < g a. f a * g a)"
unfolding point_measure_def
apply (subst density_max_0)
- apply (subst positive_integral_density)
- apply (simp_all add: AE_count_space positive_integral_density)
- apply (subst positive_integral_count_space )
+ apply (subst nn_integral_density)
+ apply (simp_all add: AE_count_space nn_integral_density)
+ apply (subst nn_integral_count_space )
apply (auto intro!: setsum_cong simp: max_def ereal_zero_less_0_iff)
apply (rule finite_subset)
prefer 2
@@ -1988,10 +1988,10 @@
apply auto
done
-lemma positive_integral_point_measure_finite:
+lemma nn_integral_point_measure_finite:
"finite A \<Longrightarrow> (\<And>a. a \<in> A \<Longrightarrow> 0 \<le> f a) \<Longrightarrow> (\<And>a. a \<in> A \<Longrightarrow> 0 \<le> g a) \<Longrightarrow>
- integral\<^sup>P (point_measure A f) g = (\<Sum>a\<in>A. f a * g a)"
- by (subst positive_integral_point_measure) (auto intro!: setsum_mono_zero_left simp: less_le)
+ integral\<^sup>N (point_measure A f) g = (\<Sum>a\<in>A. f a * g a)"
+ by (subst nn_integral_point_measure) (auto intro!: setsum_mono_zero_left simp: less_le)
subsubsection {* Uniform measure *}
@@ -2008,10 +2008,10 @@
proof -
from A B have "emeasure (uniform_measure M A) B = (\<integral>\<^sup>+x. (1 / emeasure M A) * indicator (A \<inter> B) x \<partial>M)"
by (auto simp add: uniform_measure_def emeasure_density split: split_indicator
- intro!: positive_integral_cong)
+ intro!: nn_integral_cong)
also have "\<dots> = emeasure M (A \<inter> B) / emeasure M A"
using A B
- by (subst positive_integral_cmult_indicator) (simp_all add: sets.Int emeasure_nonneg)
+ by (subst nn_integral_cmult_indicator) (simp_all add: sets.Int emeasure_nonneg)
finally show ?thesis .
qed
--- a/src/HOL/Probability/Probability_Measure.thy Mon May 19 15:23:08 2014 +0200
+++ b/src/HOL/Probability/Probability_Measure.thy Mon May 19 16:14:08 2014 +0200
@@ -290,7 +290,7 @@
simp: disjoint_family_on_def)
also have "\<dots> = (\<integral>\<^sup>+i. \<P>(x in M. P i x) \<partial>count_space I)"
unfolding emeasure_eq_measure using disj
- by (intro positive_integral_cong ereal.inject[THEN iffD2] prob_eq_AE)
+ by (intro nn_integral_cong ereal.inject[THEN iffD2] prob_eq_AE)
(auto intro!: sets.sets_Collect_countable_Ex' sets.sets_Collect_conj sets.sets_Collect_countable_Ex1' I sets)+
finally show ?thesis .
qed
@@ -402,9 +402,9 @@
also have "\<dots> = emeasure (density (count_space A) P) {a}"
using X by (simp add: distributed_distr_eq_density)
also have "\<dots> = (\<integral>\<^sup>+x. P a * indicator {a} x \<partial>count_space A)"
- using X a by (auto simp add: emeasure_density distributed_def indicator_def intro!: positive_integral_cong)
+ using X a by (auto simp add: emeasure_density distributed_def indicator_def intro!: nn_integral_cong)
also have "\<dots> = P a"
- using X a by (subst positive_integral_cmult_indicator) (auto simp: distributed_def one_ereal_def[symmetric] AE_count_space)
+ using X a by (subst nn_integral_cmult_indicator) (auto simp: distributed_def one_ereal_def[symmetric] AE_count_space)
finally show ?thesis ..
qed
@@ -446,10 +446,10 @@
by (auto simp: distributed_AE
distributed_distr_eq_density[symmetric] emeasure_density[symmetric] emeasure_distr)
-lemma distributed_positive_integral:
+lemma distributed_nn_integral:
"distributed M N X f \<Longrightarrow> g \<in> borel_measurable N \<Longrightarrow> (\<integral>\<^sup>+x. f x * g x \<partial>N) = (\<integral>\<^sup>+x. g (X x) \<partial>M)"
by (auto simp: distributed_AE
- distributed_distr_eq_density[symmetric] positive_integral_density[symmetric] positive_integral_distr)
+ distributed_distr_eq_density[symmetric] nn_integral_density[symmetric] nn_integral_distr)
lemma distributed_integral:
"distributed M N X f \<Longrightarrow> g \<in> borel_measurable N \<Longrightarrow> (\<integral>x. f x * g x \<partial>N) = (\<integral>x. g (X x) \<partial>M)"
@@ -520,10 +520,10 @@
have "emeasure ?L E = emeasure M {x \<in> space M. X x \<in> A \<and> Y x \<in> B}"
by (auto intro!: arg_cong[where f="emeasure M"] simp add: emeasure_distr measurable_Pair)
also have "\<dots> = (\<integral>\<^sup>+x. (\<integral>\<^sup>+y. (f (x, y) * indicator B y) * indicator A x \<partial>T) \<partial>S)"
- using f by (auto simp add: eq positive_integral_multc intro!: positive_integral_cong)
+ using f by (auto simp add: eq nn_integral_multc intro!: nn_integral_cong)
also have "\<dots> = emeasure ?R E"
- by (auto simp add: emeasure_density T.positive_integral_fst[symmetric]
- intro!: positive_integral_cong split: split_indicator)
+ by (auto simp add: emeasure_density T.nn_integral_fst[symmetric]
+ intro!: nn_integral_cong split: split_indicator)
finally show "emeasure ?L E = emeasure ?R E" .
qed
qed (auto simp: f)
@@ -564,12 +564,12 @@
using Pxy A by (intro distributed_emeasure) auto
finally have "emeasure M ((\<lambda>x. (Y x, X x)) -` A \<inter> space M) =
(\<integral>\<^sup>+ x. Pxy x * indicator A (snd x, fst x) \<partial>(S \<Otimes>\<^sub>M T))"
- by (auto intro!: positive_integral_cong split: split_indicator) }
+ by (auto intro!: nn_integral_cong split: split_indicator) }
note * = this
show "distr M ?D (\<lambda>x. (Y x, X x)) = density ?D (\<lambda>(x, y). Pxy (y, x))"
apply (intro measure_eqI)
apply (simp_all add: emeasure_distr[OF 2] emeasure_density[OF 1])
- apply (subst positive_integral_distr)
+ apply (subst nn_integral_distr)
apply (auto intro!: * simp: comp_def split_beta)
done
qed
@@ -590,13 +590,13 @@
show X: "X \<in> measurable M S" by simp
show borel: "Px \<in> borel_measurable S"
- by (auto intro!: T.positive_integral_fst simp: Px_def)
+ by (auto intro!: T.nn_integral_fst simp: Px_def)
interpret Pxy: prob_space "distr M (S \<Otimes>\<^sub>M T) (\<lambda>x. (X x, Y x))"
by (intro prob_space_distr) simp
have "(\<integral>\<^sup>+ x. max 0 (- Pxy x) \<partial>(S \<Otimes>\<^sub>M T)) = (\<integral>\<^sup>+ x. 0 \<partial>(S \<Otimes>\<^sub>M T))"
using Pxy
- by (intro positive_integral_cong_AE) (auto simp: max_def dest: distributed_AE)
+ by (intro nn_integral_cong_AE) (auto simp: max_def dest: distributed_AE)
show "distr M S X = density S Px"
proof (rule measure_eqI)
@@ -608,18 +608,18 @@
using Pxy by (simp add: distributed_def)
also have "\<dots> = \<integral>\<^sup>+ x. \<integral>\<^sup>+ y. Pxy (x, y) * indicator (A \<times> space T) (x, y) \<partial>T \<partial>S"
using A borel Pxy
- by (simp add: emeasure_density T.positive_integral_fst[symmetric])
+ by (simp add: emeasure_density T.nn_integral_fst[symmetric])
also have "\<dots> = \<integral>\<^sup>+ x. Px x * indicator A x \<partial>S"
- apply (rule positive_integral_cong_AE)
+ apply (rule nn_integral_cong_AE)
using Pxy[THEN distributed_AE, THEN ST.AE_pair] AE_space
proof eventually_elim
fix x assume "x \<in> space S" "AE y in T. 0 \<le> Pxy (x, y)"
moreover have eq: "\<And>y. y \<in> space T \<Longrightarrow> indicator (A \<times> space T) (x, y) = indicator A x"
by (auto simp: indicator_def)
ultimately have "(\<integral>\<^sup>+ y. Pxy (x, y) * indicator (A \<times> space T) (x, y) \<partial>T) = (\<integral>\<^sup>+ y. Pxy (x, y) \<partial>T) * indicator A x"
- by (simp add: eq positive_integral_multc cong: positive_integral_cong)
+ by (simp add: eq nn_integral_multc cong: nn_integral_cong)
also have "(\<integral>\<^sup>+ y. Pxy (x, y) \<partial>T) = Px x"
- by (simp add: Px_def ereal_real positive_integral_positive)
+ by (simp add: Px_def ereal_real nn_integral_nonneg)
finally show "(\<integral>\<^sup>+ y. Pxy (x, y) * indicator (A \<times> space T) (x, y) \<partial>T) = Px x * indicator A x" .
qed
finally show "emeasure (distr M S X) A = emeasure (density S Px) A"
@@ -627,7 +627,7 @@
qed simp
show "AE x in S. 0 \<le> Px x"
- by (simp add: Px_def positive_integral_positive real_of_ereal_pos)
+ by (simp add: Px_def nn_integral_nonneg real_of_ereal_pos)
qed
lemma (in prob_space) distr_marginal2:
@@ -727,10 +727,10 @@
intro!: arg_cong[where f=prob])
also have "\<dots> = (\<integral>\<^sup>+x. ereal (P' a) * indicator {a} x \<partial>S)"
using A X a
- by (subst positive_integral_cmult_indicator)
+ by (subst nn_integral_cmult_indicator)
(auto simp: S_def P'_def simple_distributed_def simple_functionD measure_nonneg)
also have "\<dots> = (\<integral>\<^sup>+x. ereal (P' x) * indicator {a} x \<partial>S)"
- by (auto simp: indicator_def intro!: positive_integral_cong)
+ by (auto simp: indicator_def intro!: nn_integral_cong)
also have "\<dots> = emeasure (density S P') {a}"
using a A by (intro emeasure_density[symmetric]) (auto simp: S_def)
finally show "emeasure (distr M S X) {a} = emeasure (density S P') {a}" .
@@ -866,7 +866,7 @@
Pxy[THEN simple_distributed, THEN distributed_real_AE]
show ?thesis
unfolding AE_count_space
- apply (auto simp add: positive_integral_count_space_finite * intro!: setsum_cong split: split_max)
+ apply (auto simp add: nn_integral_count_space_finite * intro!: setsum_cong split: split_max)
done
qed
--- a/src/HOL/Probability/Radon_Nikodym.thy Mon May 19 15:23:08 2014 +0200
+++ b/src/HOL/Probability/Radon_Nikodym.thy Mon May 19 16:14:08 2014 +0200
@@ -44,7 +44,7 @@
qed fact
lemma (in sigma_finite_measure) Ex_finite_integrable_function:
- shows "\<exists>h\<in>borel_measurable M. integral\<^sup>P M h \<noteq> \<infinity> \<and> (\<forall>x\<in>space M. 0 < h x \<and> h x < \<infinity>) \<and> (\<forall>x. 0 \<le> h x)"
+ shows "\<exists>h\<in>borel_measurable M. integral\<^sup>N M h \<noteq> \<infinity> \<and> (\<forall>x\<in>space M. 0 < h x \<and> h x < \<infinity>) \<and> (\<forall>x. 0 \<le> h x)"
proof -
obtain A :: "nat \<Rightarrow> 'a set" where
range[measurable]: "range A \<subseteq> sets M" and
@@ -67,8 +67,8 @@
proof (safe intro!: bexI[of _ ?h] del: notI)
have "\<And>i. A i \<in> sets M"
using range by fastforce+
- then have "integral\<^sup>P M ?h = (\<Sum>i. n i * emeasure M (A i))" using pos
- by (simp add: positive_integral_suminf positive_integral_cmult_indicator)
+ then have "integral\<^sup>N M ?h = (\<Sum>i. n i * emeasure M (A i))" using pos
+ by (simp add: nn_integral_suminf nn_integral_cmult_indicator)
also have "\<dots> \<le> (\<Sum>i. (1 / 2)^Suc i)"
proof (rule suminf_le_pos)
fix N
@@ -82,7 +82,7 @@
finally show "n N * emeasure M (A N) \<le> (1 / 2) ^ Suc N" .
show "0 \<le> n N * emeasure M (A N)" using n[of N] `A N \<in> sets M` by (simp add: emeasure_nonneg)
qed
- finally show "integral\<^sup>P M ?h \<noteq> \<infinity>" unfolding suminf_half_series_ereal by auto
+ finally show "integral\<^sup>N M ?h \<noteq> \<infinity>" unfolding suminf_half_series_ereal by auto
next
{ fix x assume "x \<in> space M"
then obtain i where "x \<in> A i" using space[symmetric] by auto
@@ -317,7 +317,7 @@
(\<integral>\<^sup>+x. g x * indicator (?A \<inter> A) x \<partial>M) +
(\<integral>\<^sup>+x. f x * indicator ((space M - ?A) \<inter> A) x \<partial>M)"
using f g sets unfolding G_def
- by (auto cong: positive_integral_cong intro!: positive_integral_add)
+ by (auto cong: nn_integral_cong intro!: nn_integral_add)
also have "\<dots> \<le> N (?A \<inter> A) + N ((space M - ?A) \<inter> A)"
using f g sets unfolding G_def by (auto intro!: add_mono)
also have "\<dots> = N A"
@@ -338,31 +338,31 @@
fix A assume "A \<in> sets M"
have "(\<integral>\<^sup>+x. (SUP i. f i x) * indicator A x \<partial>M) =
(\<integral>\<^sup>+x. (SUP i. f i x * indicator A x) \<partial>M)"
- by (intro positive_integral_cong) (simp split: split_indicator)
+ by (intro nn_integral_cong) (simp split: split_indicator)
also have "\<dots> = (SUP i. (\<integral>\<^sup>+x. f i x * indicator A x \<partial>M))"
using `incseq f` f `A \<in> sets M`
- by (intro positive_integral_monotone_convergence_SUP)
+ by (intro nn_integral_monotone_convergence_SUP)
(auto simp: G_def incseq_Suc_iff le_fun_def split: split_indicator)
finally show "(\<integral>\<^sup>+x. (SUP i. f i x) * indicator A x \<partial>M) \<le> N A"
using f `A \<in> sets M` by (auto intro!: SUP_least simp: G_def)
qed }
note SUP_in_G = this
- let ?y = "SUP g : G. integral\<^sup>P M g"
+ let ?y = "SUP g : G. integral\<^sup>N M g"
have y_le: "?y \<le> N (space M)" unfolding G_def
proof (safe intro!: SUP_least)
fix g assume "\<forall>A\<in>sets M. (\<integral>\<^sup>+x. g x * indicator A x \<partial>M) \<le> N A"
- from this[THEN bspec, OF sets.top] show "integral\<^sup>P M g \<le> N (space M)"
- by (simp cong: positive_integral_cong)
+ from this[THEN bspec, OF sets.top] show "integral\<^sup>N M g \<le> N (space M)"
+ by (simp cong: nn_integral_cong)
qed
- from SUP_countable_SUP [OF `G \<noteq> {}`, of "integral\<^sup>P M"] guess ys .. note ys = this
- then have "\<forall>n. \<exists>g. g\<in>G \<and> integral\<^sup>P M g = ys n"
+ from SUP_countable_SUP [OF `G \<noteq> {}`, of "integral\<^sup>N M"] guess ys .. note ys = this
+ then have "\<forall>n. \<exists>g. g\<in>G \<and> integral\<^sup>N M g = ys n"
proof safe
- fix n assume "range ys \<subseteq> integral\<^sup>P M ` G"
- hence "ys n \<in> integral\<^sup>P M ` G" by auto
- thus "\<exists>g. g\<in>G \<and> integral\<^sup>P M g = ys n" by auto
+ fix n assume "range ys \<subseteq> integral\<^sup>N M ` G"
+ hence "ys n \<in> integral\<^sup>N M ` G" by auto
+ thus "\<exists>g. g\<in>G \<and> integral\<^sup>N M g = ys n" by auto
qed
- from choice[OF this] obtain gs where "\<And>i. gs i \<in> G" "\<And>n. integral\<^sup>P M (gs n) = ys n" by auto
- hence y_eq: "?y = (SUP i. integral\<^sup>P M (gs i))" using ys by auto
+ from choice[OF this] obtain gs where "\<And>i. gs i \<in> G" "\<And>n. integral\<^sup>N M (gs n) = ys n" by auto
+ hence y_eq: "?y = (SUP i. integral\<^sup>N M (gs i))" using ys by auto
let ?g = "\<lambda>i x. Max ((\<lambda>n. gs n x) ` {..i})"
def f \<equiv> "\<lambda>x. SUP i. ?g i x"
let ?F = "\<lambda>A x. f x * indicator A x"
@@ -380,17 +380,17 @@
by (auto intro!: incseq_SucI le_funI simp add: atMost_Suc)
from SUP_in_G[OF this g_in_G] have [measurable]: "f \<in> G" unfolding f_def .
then have [simp, intro]: "f \<in> borel_measurable M" unfolding G_def by auto
- have "integral\<^sup>P M f = (SUP i. integral\<^sup>P M (?g i))" unfolding f_def
+ have "integral\<^sup>N M f = (SUP i. integral\<^sup>N M (?g i))" unfolding f_def
using g_in_G `incseq ?g`
- by (auto intro!: positive_integral_monotone_convergence_SUP simp: G_def)
+ by (auto intro!: nn_integral_monotone_convergence_SUP simp: G_def)
also have "\<dots> = ?y"
proof (rule antisym)
- show "(SUP i. integral\<^sup>P M (?g i)) \<le> ?y"
+ show "(SUP i. integral\<^sup>N M (?g i)) \<le> ?y"
using g_in_G by (auto intro: SUP_mono)
- show "?y \<le> (SUP i. integral\<^sup>P M (?g i))" unfolding y_eq
- by (auto intro!: SUP_mono positive_integral_mono Max_ge)
+ show "?y \<le> (SUP i. integral\<^sup>N M (?g i))" unfolding y_eq
+ by (auto intro!: SUP_mono nn_integral_mono Max_ge)
qed
- finally have int_f_eq_y: "integral\<^sup>P M f = ?y" .
+ finally have int_f_eq_y: "integral\<^sup>N M f = ?y" .
have "\<And>x. 0 \<le> f x"
unfolding f_def using `\<And>i. gs i \<in> G`
by (auto intro!: SUP_upper2 Max_ge_iff[THEN iffD2] simp: G_def)
@@ -401,12 +401,12 @@
have emeasure_M: "\<And>A. A \<in> sets M \<Longrightarrow> emeasure ?M A = ?t A"
proof (subst emeasure_diff_measure)
from f_le_N[of "space M"] show "finite_measure N" "finite_measure (density M f)"
- by (auto intro!: finite_measureI simp: emeasure_density cong: positive_integral_cong)
+ by (auto intro!: finite_measureI simp: emeasure_density cong: nn_integral_cong)
next
fix B assume "B \<in> sets N" with f_le_N[of B] show "emeasure (density M f) B \<le> emeasure N B"
- by (auto simp: sets_eq emeasure_density cong: positive_integral_cong)
+ by (auto simp: sets_eq emeasure_density cong: nn_integral_cong)
qed (auto simp: sets_eq emeasure_density)
- from emeasure_M[of "space M"] N.finite_emeasure_space positive_integral_positive[of M "?F (space M)"]
+ from emeasure_M[of "space M"] N.finite_emeasure_space nn_integral_nonneg[of M "?F (space M)"]
interpret M': finite_measure ?M
by (auto intro!: finite_measureI simp: sets_eq_imp_space_eq[OF sets_eq] N.emeasure_eq_measure ereal_minus_eq_PInfty_iff)
@@ -417,7 +417,7 @@
unfolding absolutely_continuous_def by auto
moreover from A_M A_N have "(\<integral>\<^sup>+ x. ?F A x \<partial>M) \<le> N A" using `f \<in> G` by (auto simp: G_def)
ultimately have "N A - (\<integral>\<^sup>+ x. ?F A x \<partial>M) = 0"
- using positive_integral_positive[of M] by (auto intro!: antisym)
+ using nn_integral_nonneg[of M] by (auto intro!: antisym)
then show "A \<in> null_sets ?M"
using A_M by (simp add: emeasure_M null_sets_def sets_eq)
qed
@@ -462,11 +462,11 @@
hence "A \<inter> A0 \<in> sets M" using `A0 \<in> sets M` by auto
have "(\<integral>\<^sup>+x. ?f0 x * indicator A x \<partial>M) =
(\<integral>\<^sup>+x. f x * indicator A x + b * indicator (A \<inter> A0) x \<partial>M)"
- by (auto intro!: positive_integral_cong split: split_indicator)
+ by (auto intro!: nn_integral_cong split: split_indicator)
hence "(\<integral>\<^sup>+x. ?f0 x * indicator A x \<partial>M) =
(\<integral>\<^sup>+x. f x * indicator A x \<partial>M) + b * emeasure M (A \<inter> A0)"
using `A0 \<in> sets M` `A \<inter> A0 \<in> sets M` A b `f \<in> G`
- by (simp add: positive_integral_add positive_integral_cmult_indicator G_def) }
+ by (simp add: nn_integral_add nn_integral_cmult_indicator G_def) }
note f0_eq = this
{ fix A assume A: "A \<in> sets M"
hence "A \<inter> A0 \<in> sets M" using `A0 \<in> sets M` by auto
@@ -480,11 +480,11 @@
by (auto intro!: add_left_mono simp: sets_eq)
also have "\<dots> \<le> N A"
unfolding emeasure_M[OF `A \<in> sets M`]
- using f_le_v N.emeasure_eq_measure[of A] positive_integral_positive[of M "?F A"]
+ using f_le_v N.emeasure_eq_measure[of A] nn_integral_nonneg[of M "?F A"]
by (cases "\<integral>\<^sup>+x. ?F A x \<partial>M", cases "N A") auto
finally have "(\<integral>\<^sup>+x. ?f0 x * indicator A x \<partial>M) \<le> N A" . }
hence "?f0 \<in> G" using `A0 \<in> sets M` b `f \<in> G` by (auto simp: G_def)
- have int_f_finite: "integral\<^sup>P M f \<noteq> \<infinity>"
+ have int_f_finite: "integral\<^sup>N M f \<noteq> \<infinity>"
by (metis N.emeasure_finite ereal_infty_less_eq2(1) int_f_eq_y y_le)
have "0 < ?M (space M) - emeasure ?Mb (space M)"
using pos_t
@@ -503,13 +503,13 @@
by (auto simp: absolutely_continuous_def null_sets_def)
then have "0 < emeasure M A0" using emeasure_nonneg[of M A0] by auto
hence "0 < b * emeasure M A0" using b by (auto simp: ereal_zero_less_0_iff)
- with int_f_finite have "?y + 0 < integral\<^sup>P M f + b * emeasure M A0" unfolding int_f_eq_y
+ with int_f_finite have "?y + 0 < integral\<^sup>N M f + b * emeasure M A0" unfolding int_f_eq_y
using `f \<in> G`
- by (intro ereal_add_strict_mono) (auto intro!: SUP_upper2 positive_integral_positive)
- also have "\<dots> = integral\<^sup>P M ?f0" using f0_eq[OF sets.top] `A0 \<in> sets M` sets.sets_into_space
- by (simp cong: positive_integral_cong)
- finally have "?y < integral\<^sup>P M ?f0" by simp
- moreover from `?f0 \<in> G` have "integral\<^sup>P M ?f0 \<le> ?y" by (auto intro!: SUP_upper)
+ by (intro ereal_add_strict_mono) (auto intro!: SUP_upper2 nn_integral_nonneg)
+ also have "\<dots> = integral\<^sup>N M ?f0" using f0_eq[OF sets.top] `A0 \<in> sets M` sets.sets_into_space
+ by (simp cong: nn_integral_cong)
+ finally have "?y < integral\<^sup>N M ?f0" by simp
+ moreover from `?f0 \<in> G` have "integral\<^sup>N M ?f0 \<le> ?y" by (auto intro!: SUP_upper)
ultimately show False by auto
qed
let ?f = "\<lambda>x. max 0 (f x)"
@@ -520,7 +520,7 @@
fix A assume A: "A\<in>sets (density M ?f)"
then show "emeasure (density M ?f) A = emeasure N A"
using `f \<in> G` A upper_bound[THEN bspec, of A] N.emeasure_eq_measure[of A]
- by (cases "integral\<^sup>P M (?F A)")
+ by (cases "integral\<^sup>N M (?F A)")
(auto intro!: antisym simp add: emeasure_density G_def emeasure_M density_max_0[symmetric])
qed auto
qed
@@ -669,10 +669,10 @@
proof (intro allI finite_measure.Radon_Nikodym_finite_measure)
fix i
from Q show "finite_measure (?M i)"
- by (auto intro!: finite_measureI cong: positive_integral_cong
+ by (auto intro!: finite_measureI cong: nn_integral_cong
simp add: emeasure_density subset_eq sets_eq)
from Q have "emeasure (?N i) (space N) = emeasure N (Q i)"
- by (simp add: sets_eq[symmetric] emeasure_density subset_eq cong: positive_integral_cong)
+ by (simp add: sets_eq[symmetric] emeasure_density subset_eq cong: nn_integral_cong)
with Q_fin show "finite_measure (?N i)"
by (auto intro!: finite_measureI)
show "sets (?N i) = sets (?M i)" by (simp add: sets_eq)
@@ -688,8 +688,8 @@
by force
{ fix A i assume A: "A \<in> sets M"
with Q borel have "(\<integral>\<^sup>+x. f i x * indicator (Q i \<inter> A) x \<partial>M) = emeasure (density (?M i) (f i)) A"
- by (auto simp add: emeasure_density positive_integral_density subset_eq
- intro!: positive_integral_cong split: split_indicator)
+ by (auto simp add: emeasure_density nn_integral_density subset_eq
+ intro!: nn_integral_cong split: split_indicator)
also have "\<dots> = emeasure N (Q i \<inter> A)"
using A Q by (simp add: f_density emeasure_restricted subset_eq sets_eq)
finally have "emeasure N (Q i \<inter> A) = (\<integral>\<^sup>+x. f i x * indicator (Q i \<inter> A) x \<partial>M)" .. }
@@ -709,13 +709,13 @@
"\<And>i. AE x in M. 0 \<le> f i x * indicator (Q i \<inter> A) x"
using borel Qi Q0(1) `A \<in> sets M` by (auto intro!: borel_measurable_ereal_times)
have "(\<integral>\<^sup>+x. ?f x * indicator A x \<partial>M) = (\<integral>\<^sup>+x. (\<Sum>i. f i x * indicator (Q i \<inter> A) x) + \<infinity> * indicator (Q0 \<inter> A) x \<partial>M)"
- using borel by (intro positive_integral_cong) (auto simp: indicator_def)
+ using borel by (intro nn_integral_cong) (auto simp: indicator_def)
also have "\<dots> = (\<integral>\<^sup>+x. (\<Sum>i. f i x * indicator (Q i \<inter> A) x) \<partial>M) + \<infinity> * emeasure M (Q0 \<inter> A)"
using borel Qi Q0(1) `A \<in> sets M`
- by (subst positive_integral_add) (auto simp del: ereal_infty_mult
- simp add: positive_integral_cmult_indicator sets.Int intro!: suminf_0_le)
+ by (subst nn_integral_add) (auto simp del: ereal_infty_mult
+ simp add: nn_integral_cmult_indicator sets.Int intro!: suminf_0_le)
also have "\<dots> = (\<Sum>i. N (Q i \<inter> A)) + \<infinity> * emeasure M (Q0 \<inter> A)"
- by (subst integral_eq[OF `A \<in> sets M`], subst positive_integral_suminf) auto
+ by (subst integral_eq[OF `A \<in> sets M`], subst nn_integral_suminf) auto
finally have "(\<integral>\<^sup>+x. ?f x * indicator A x \<partial>M) = (\<Sum>i. N (Q i \<inter> A)) + \<infinity> * emeasure M (Q0 \<inter> A)" .
moreover have "(\<Sum>i. N (Q i \<inter> A)) = N ((\<Union>i. Q i) \<inter> A)"
using Q Q_sets `A \<in> sets M`
@@ -742,7 +742,7 @@
shows "\<exists>f \<in> borel_measurable M. (\<forall>x. 0 \<le> f x) \<and> density M f = N"
proof -
from Ex_finite_integrable_function
- obtain h where finite: "integral\<^sup>P M h \<noteq> \<infinity>" and
+ obtain h where finite: "integral\<^sup>N M h \<noteq> \<infinity>" and
borel: "h \<in> borel_measurable M" and
nn: "\<And>x. 0 \<le> h x" and
pos: "\<And>x. x \<in> space M \<Longrightarrow> 0 < h x" and
@@ -750,7 +750,7 @@
let ?T = "\<lambda>A. (\<integral>\<^sup>+x. h x * indicator A x \<partial>M)"
let ?MT = "density M h"
from borel finite nn interpret T: finite_measure ?MT
- by (auto intro!: finite_measureI cong: positive_integral_cong simp: emeasure_density)
+ by (auto intro!: finite_measureI cong: nn_integral_cong simp: emeasure_density)
have "absolutely_continuous ?MT N" "sets N = sets ?MT"
proof (unfold absolutely_continuous_def, safe)
fix A assume "A \<in> null_sets ?MT"
@@ -774,7 +774,7 @@
lemma finite_density_unique:
assumes borel: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
assumes pos: "AE x in M. 0 \<le> f x" "AE x in M. 0 \<le> g x"
- and fin: "integral\<^sup>P M f \<noteq> \<infinity>"
+ and fin: "integral\<^sup>N M f \<noteq> \<infinity>"
shows "density M f = density M g \<longleftrightarrow> (AE x in M. f x = g x)"
proof (intro iffI ballI)
fix A assume eq: "AE x in M. f x = g x"
@@ -786,19 +786,19 @@
with borel have eq: "\<forall>A\<in>sets M. ?P f A = ?P g A"
by (simp add: emeasure_density[symmetric])
from this[THEN bspec, OF sets.top] fin
- have g_fin: "integral\<^sup>P M g \<noteq> \<infinity>" by (simp cong: positive_integral_cong)
+ have g_fin: "integral\<^sup>N M g \<noteq> \<infinity>" by (simp cong: nn_integral_cong)
{ fix f g assume borel: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
and pos: "AE x in M. 0 \<le> f x" "AE x in M. 0 \<le> g x"
- and g_fin: "integral\<^sup>P M g \<noteq> \<infinity>" and eq: "\<forall>A\<in>sets M. ?P f A = ?P g A"
+ and g_fin: "integral\<^sup>N M g \<noteq> \<infinity>" and eq: "\<forall>A\<in>sets M. ?P f A = ?P g A"
let ?N = "{x\<in>space M. g x < f x}"
have N: "?N \<in> sets M" using borel by simp
- have "?P g ?N \<le> integral\<^sup>P M g" using pos
- by (intro positive_integral_mono_AE) (auto split: split_indicator)
+ have "?P g ?N \<le> integral\<^sup>N M g" using pos
+ by (intro nn_integral_mono_AE) (auto split: split_indicator)
then have Pg_fin: "?P g ?N \<noteq> \<infinity>" using g_fin by auto
have "?P (\<lambda>x. (f x - g x)) ?N = (\<integral>\<^sup>+x. f x * indicator ?N x - g x * indicator ?N x \<partial>M)"
- by (auto intro!: positive_integral_cong simp: indicator_def)
+ by (auto intro!: nn_integral_cong simp: indicator_def)
also have "\<dots> = ?P f ?N - ?P g ?N"
- proof (rule positive_integral_diff)
+ proof (rule nn_integral_diff)
show "(\<lambda>x. f x * indicator ?N x) \<in> borel_measurable M" "(\<lambda>x. g x * indicator ?N x) \<in> borel_measurable M"
using borel N by auto
show "AE x in M. g x * indicator ?N x \<le> f x * indicator ?N x"
@@ -806,10 +806,10 @@
using pos by (auto split: split_indicator)
qed fact
also have "\<dots> = 0"
- unfolding eq[THEN bspec, OF N] using positive_integral_positive[of M] Pg_fin by auto
+ unfolding eq[THEN bspec, OF N] using nn_integral_nonneg[of M] Pg_fin by auto
finally have "AE x in M. f x \<le> g x"
- using pos borel positive_integral_PInf_AE[OF borel(2) g_fin]
- by (subst (asm) positive_integral_0_iff_AE)
+ using pos borel nn_integral_PInf_AE[OF borel(2) g_fin]
+ by (subst (asm) nn_integral_0_iff_AE)
(auto split: split_indicator simp: not_less ereal_minus_le_iff) }
from this[OF borel pos g_fin eq] this[OF borel(2,1) pos(2,1) fin] eq
show "AE x in M. f x = g x" by auto
@@ -856,9 +856,9 @@
using borel Q0(1) by auto
have "?N (?A i) \<le> (\<integral>\<^sup>+x. (i::ereal) * indicator (?A i) x \<partial>M)"
unfolding eq[OF `?A i \<in> sets M`]
- by (auto intro!: positive_integral_mono simp: indicator_def)
+ by (auto intro!: nn_integral_mono simp: indicator_def)
also have "\<dots> = i * emeasure M (?A i)"
- using `?A i \<in> sets M` by (auto intro!: positive_integral_cmult_indicator)
+ using `?A i \<in> sets M` by (auto intro!: nn_integral_cmult_indicator)
also have "\<dots> < \<infinity>" using emeasure_real[of "?A i"] by simp
finally have "?N (?A i) \<noteq> \<infinity>" by simp
then show "?A i \<in> null_sets M" using in_Q0[OF `?A i \<in> sets M`] `?A i \<in> sets M` by auto
@@ -888,35 +888,35 @@
shows "AE x in M. f x = f' x"
proof -
obtain h where h_borel: "h \<in> borel_measurable M"
- and fin: "integral\<^sup>P M h \<noteq> \<infinity>" and pos: "\<And>x. x \<in> space M \<Longrightarrow> 0 < h x \<and> h x < \<infinity>" "\<And>x. 0 \<le> h x"
+ and fin: "integral\<^sup>N M h \<noteq> \<infinity>" and pos: "\<And>x. x \<in> space M \<Longrightarrow> 0 < h x \<and> h x < \<infinity>" "\<And>x. 0 \<le> h x"
using Ex_finite_integrable_function by auto
then have h_nn: "AE x in M. 0 \<le> h x" by auto
let ?H = "density M h"
interpret h: finite_measure ?H
using fin h_borel pos
- by (intro finite_measureI) (simp cong: positive_integral_cong emeasure_density add: fin)
+ by (intro finite_measureI) (simp cong: nn_integral_cong emeasure_density add: fin)
let ?fM = "density M f"
let ?f'M = "density M f'"
{ fix A assume "A \<in> sets M"
then have "{x \<in> space M. h x * indicator A x \<noteq> 0} = A"
using pos(1) sets.sets_into_space by (force simp: indicator_def)
then have "(\<integral>\<^sup>+x. h x * indicator A x \<partial>M) = 0 \<longleftrightarrow> A \<in> null_sets M"
- using h_borel `A \<in> sets M` h_nn by (subst positive_integral_0_iff) auto }
+ using h_borel `A \<in> sets M` h_nn by (subst nn_integral_0_iff) auto }
note h_null_sets = this
{ fix A assume "A \<in> sets M"
have "(\<integral>\<^sup>+x. f x * (h x * indicator A x) \<partial>M) = (\<integral>\<^sup>+x. h x * indicator A x \<partial>?fM)"
using `A \<in> sets M` h_borel h_nn f f'
- by (intro positive_integral_density[symmetric]) auto
+ by (intro nn_integral_density[symmetric]) auto
also have "\<dots> = (\<integral>\<^sup>+x. h x * indicator A x \<partial>?f'M)"
by (simp_all add: density_eq)
also have "\<dots> = (\<integral>\<^sup>+x. f' x * (h x * indicator A x) \<partial>M)"
using `A \<in> sets M` h_borel h_nn f f'
- by (intro positive_integral_density) auto
+ by (intro nn_integral_density) auto
finally have "(\<integral>\<^sup>+x. h x * (f x * indicator A x) \<partial>M) = (\<integral>\<^sup>+x. h x * (f' x * indicator A x) \<partial>M)"
by (simp add: ac_simps)
then have "(\<integral>\<^sup>+x. (f x * indicator A x) \<partial>?H) = (\<integral>\<^sup>+x. (f' x * indicator A x) \<partial>?H)"
using `A \<in> sets M` h_borel h_nn f f'
- by (subst (asm) (1 2) positive_integral_density[symmetric]) auto }
+ by (subst (asm) (1 2) nn_integral_density[symmetric]) auto }
then have "AE x in ?H. f x = f' x" using h_borel h_nn f f'
by (intro h.density_unique_finite_measure absolutely_continuous_AE[of M])
(auto simp add: AE_density)
@@ -975,17 +975,17 @@
assume "sigma_finite_measure ?N"
then interpret N: sigma_finite_measure ?N .
from N.Ex_finite_integrable_function obtain h where
- h: "h \<in> borel_measurable M" "integral\<^sup>P ?N h \<noteq> \<infinity>" and
+ h: "h \<in> borel_measurable M" "integral\<^sup>N ?N h \<noteq> \<infinity>" and
h_nn: "\<And>x. 0 \<le> h x" and
fin: "\<forall>x\<in>space M. 0 < h x \<and> h x < \<infinity>" by auto
have "AE x in M. f x * h x \<noteq> \<infinity>"
proof (rule AE_I')
- have "integral\<^sup>P ?N h = (\<integral>\<^sup>+x. f x * h x \<partial>M)" using f h h_nn
- by (auto intro!: positive_integral_density)
+ have "integral\<^sup>N ?N h = (\<integral>\<^sup>+x. f x * h x \<partial>M)" using f h h_nn
+ by (auto intro!: nn_integral_density)
then have "(\<integral>\<^sup>+x. f x * h x \<partial>M) \<noteq> \<infinity>"
using h(2) by simp
then show "(\<lambda>x. f x * h x) -` {\<infinity>} \<inter> space M \<in> null_sets M"
- using f h(1) by (auto intro!: positive_integral_PInf borel_measurable_vimage)
+ using f h(1) by (auto intro!: nn_integral_PInf borel_measurable_vimage)
qed auto
then show "AE x in M. f x \<noteq> \<infinity>"
using fin by (auto elim!: AE_Ball_mp)
@@ -1036,14 +1036,14 @@
case 0
have "AE x in M. f x * indicator (A i \<inter> Q j) x = 0"
using AE by (auto simp: A_def `i = 0`)
- from positive_integral_cong_AE[OF this] show ?thesis by simp
+ from nn_integral_cong_AE[OF this] show ?thesis by simp
next
case (Suc n)
then have "(\<integral>\<^sup>+x. f x * indicator (A i \<inter> Q j) x \<partial>M) \<le>
(\<integral>\<^sup>+x. (Suc n :: ereal) * indicator (Q j) x \<partial>M)"
- by (auto intro!: positive_integral_mono simp: indicator_def A_def real_eq_of_nat)
+ by (auto intro!: nn_integral_mono simp: indicator_def A_def real_eq_of_nat)
also have "\<dots> = Suc n * emeasure M (Q j)"
- using Q by (auto intro!: positive_integral_cmult_indicator)
+ using Q by (auto intro!: nn_integral_cmult_indicator)
also have "\<dots> < \<infinity>"
using Q by (auto simp: real_eq_of_nat[symmetric])
finally show ?thesis by simp
@@ -1109,15 +1109,15 @@
"absolutely_continuous M N \<Longrightarrow> sets N = sets M \<Longrightarrow> density M (RN_deriv M N) = N"
by (metis RN_derivI Radon_Nikodym)
-lemma (in sigma_finite_measure) RN_deriv_positive_integral:
+lemma (in sigma_finite_measure) RN_deriv_nn_integral:
assumes N: "absolutely_continuous M N" "sets N = sets M"
and f: "f \<in> borel_measurable M"
- shows "integral\<^sup>P N f = (\<integral>\<^sup>+x. RN_deriv M N x * f x \<partial>M)"
+ shows "integral\<^sup>N N f = (\<integral>\<^sup>+x. RN_deriv M N x * f x \<partial>M)"
proof -
- have "integral\<^sup>P N f = integral\<^sup>P (density M (RN_deriv M N)) f"
+ have "integral\<^sup>N N f = integral\<^sup>N (density M (RN_deriv M N)) f"
using N by (simp add: density_RN_deriv)
also have "\<dots> = (\<integral>\<^sup>+x. RN_deriv M N x * f x \<partial>M)"
- using f by (simp add: positive_integral_density RN_deriv_nonneg)
+ using f by (simp add: nn_integral_density RN_deriv_nonneg)
finally show ?thesis by simp
qed
@@ -1261,9 +1261,9 @@
have "N (?RN \<infinity>) = (\<integral>\<^sup>+ x. RN_deriv M N x * indicator (?RN \<infinity>) x \<partial>M)"
using RN(1,3) by (subst RN(2)[symmetric]) (auto simp: emeasure_density)
also have "\<dots> = (\<integral>\<^sup>+ x. \<infinity> * indicator (?RN \<infinity>) x \<partial>M)"
- by (intro positive_integral_cong) (auto simp: indicator_def)
+ by (intro nn_integral_cong) (auto simp: indicator_def)
also have "\<dots> = \<infinity> * emeasure M (?RN \<infinity>)"
- using RN by (intro positive_integral_cmult_indicator) auto
+ using RN by (intro nn_integral_cmult_indicator) auto
finally have eq: "N (?RN \<infinity>) = \<infinity> * emeasure M (?RN \<infinity>)" .
moreover
have "emeasure M (?RN \<infinity>) = 0"
@@ -1287,7 +1287,7 @@
have "N (?RN 0) = (\<integral>\<^sup>+ x. RN_deriv M N x * indicator (?RN 0) x \<partial>M)"
using RN(1,3) by (subst RN(2)[symmetric]) (auto simp: emeasure_density)
also have "\<dots> = (\<integral>\<^sup>+ x. 0 \<partial>M)"
- by (intro positive_integral_cong) (auto simp: indicator_def)
+ by (intro nn_integral_cong) (auto simp: indicator_def)
finally have "AE x in N. RN_deriv M N x \<noteq> 0"
using RN by (subst AE_iff_measurable[OF _ refl]) (auto simp: ac cong: sets_eq_imp_space_eq)
with RN(3) eq show "AE x in N. 0 < real (RN_deriv M N x)"
@@ -1301,9 +1301,9 @@
proof -
from `{x} \<in> sets M`
have "density M (RN_deriv M N) {x} = (\<integral>\<^sup>+w. RN_deriv M N x * indicator {x} w \<partial>M)"
- by (auto simp: indicator_def emeasure_density intro!: positive_integral_cong)
+ by (auto simp: indicator_def emeasure_density intro!: nn_integral_cong)
with x density_RN_deriv[OF ac] RN_deriv_nonneg[of M N] show ?thesis
- by (auto simp: positive_integral_cmult_indicator)
+ by (auto simp: nn_integral_cmult_indicator)
qed
end