--- a/src/HOL/Probability/Binary_Product_Measure.thy Thu Apr 14 12:17:44 2016 +0200
+++ b/src/HOL/Probability/Binary_Product_Measure.thy Thu Apr 14 15:48:11 2016 +0200
@@ -110,8 +110,8 @@
shows "f \<in> measurable M (M1 \<Otimes>\<^sub>M M2)"
using measurable_Pair[OF assms] by simp
-lemma
- assumes f[measurable]: "f \<in> measurable M (N \<Otimes>\<^sub>M P)"
+lemma
+ assumes f[measurable]: "f \<in> measurable M (N \<Otimes>\<^sub>M P)"
shows measurable_fst': "(\<lambda>x. fst (f x)) \<in> measurable M N"
and measurable_snd': "(\<lambda>x. snd (f x)) \<in> measurable M P"
by simp_all
@@ -134,7 +134,7 @@
finally have "a \<times> b \<in> sets (Sup_sigma {?fst, ?snd})" . }
moreover have "sets ?fst \<subseteq> sets (A \<Otimes>\<^sub>M B)"
by (rule sets_image_in_sets) (auto simp: space_pair_measure[symmetric])
- moreover have "sets ?snd \<subseteq> sets (A \<Otimes>\<^sub>M B)"
+ moreover have "sets ?snd \<subseteq> sets (A \<Otimes>\<^sub>M B)"
by (rule sets_image_in_sets) (auto simp: space_pair_measure)
ultimately show ?thesis
by (intro antisym[of "sets A" for A] sets_Sup_in_sets sets_pair_in_sets )
@@ -143,7 +143,7 @@
lemma measurable_pair_iff:
"f \<in> measurable M (M1 \<Otimes>\<^sub>M M2) \<longleftrightarrow> (fst \<circ> f) \<in> measurable M M1 \<and> (snd \<circ> f) \<in> measurable M M2"
- by (auto intro: measurable_pair[of f M M1 M2])
+ by (auto intro: measurable_pair[of f M M1 M2])
lemma measurable_split_conv:
"(\<lambda>(x, y). f x y) \<in> measurable A B \<longleftrightarrow> (\<lambda>x. f (fst x) (snd x)) \<in> measurable A B"
@@ -190,7 +190,7 @@
shows "(\<lambda>y. f (x, y)) \<in> measurable M2 M"
using measurable_comp[OF measurable_Pair1' f, OF x]
by (simp add: comp_def)
-
+
lemma measurable_Pair1:
assumes f: "f \<in> measurable (M1 \<Otimes>\<^sub>M M2) M" and y: "y \<in> space M2"
shows "(\<lambda>x. f (x, y)) \<in> measurable M1 M"
@@ -279,7 +279,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 nn_integral_nonneg)
+ by (auto simp: positive_def)
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>"
@@ -291,7 +291,7 @@
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: nn_integral_suminf[symmetric] vimage_UN suminf_emeasure emeasure_nonneg
+ by (auto simp add: nn_integral_suminf[symmetric] vimage_UN suminf_emeasure
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)"
@@ -315,7 +315,7 @@
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!: nn_integral_cong simp: emeasure_pair_measure_alt)
also have "\<dots> = emeasure M B * emeasure N A"
- using A by (simp add: emeasure_nonneg nn_integral_cmult_indicator)
+ using A by (simp add: nn_integral_cmult_indicator)
finally show ?thesis
by (simp add: ac_simps)
qed
@@ -373,9 +373,8 @@
next
fix i
from F1 F2 have "F1 i \<in> sets M1" "F2 i \<in> sets M2" by auto
- with F1 F2 emeasure_nonneg[of M1 "F1 i"] emeasure_nonneg[of M2 "F2 i"]
- show "emeasure (M1 \<Otimes>\<^sub>M M2) (F1 i \<times> F2 i) \<noteq> \<infinity>"
- by (auto simp add: emeasure_pair_measure_Times)
+ with F1 F2 show "emeasure (M1 \<Otimes>\<^sub>M M2) (F1 i \<times> F2 i) \<noteq> \<infinity>"
+ by (auto simp add: emeasure_pair_measure_Times ennreal_mult_eq_top_iff)
qed
qed
@@ -386,8 +385,7 @@
ultimately show
"\<exists>A. countable A \<and> A \<subseteq> sets (M1 \<Otimes>\<^sub>M M2) \<and> \<Union>A = space (M1 \<Otimes>\<^sub>M M2) \<and> (\<forall>a\<in>A. emeasure (M1 \<Otimes>\<^sub>M M2) a \<noteq> \<infinity>)"
by (intro exI[of _ "(\<lambda>(a, b). a \<times> b) ` (F1 \<times> F2)"] conjI)
- (auto simp: M2.emeasure_pair_measure_Times space_pair_measure set_eq_iff subset_eq
- dest: sets.sets_into_space)
+ (auto simp: M2.emeasure_pair_measure_Times space_pair_measure set_eq_iff subset_eq ennreal_mult_eq_top_iff)
qed
lemma sigma_finite_pair_measure:
@@ -455,9 +453,9 @@
proof (rule AE_I)
from N measurable_emeasure_Pair1[OF \<open>N \<in> sets (M1 \<Otimes>\<^sub>M M2)\<close>]
show "emeasure M1 {x\<in>space M1. emeasure M2 (Pair x -` N) \<noteq> 0} = 0"
- by (auto simp: M2.emeasure_pair_measure_alt nn_integral_0_iff emeasure_nonneg)
+ by (auto simp: M2.emeasure_pair_measure_alt nn_integral_0_iff)
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)
+ by (intro borel_measurable_eq measurable_emeasure_Pair1 N sets.sets_Collect_neg N) simp
{ fix x assume "x \<in> space M1" "emeasure M2 (Pair x -` N) = 0"
have "AE y in M2. Q (x, y)"
proof (rule AE_I)
@@ -523,8 +521,8 @@
"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_nn_integral_fst':
- assumes f: "f \<in> borel_measurable (M1 \<Otimes>\<^sub>M M)" "\<And>x. 0 \<le> f x"
+lemma (in sigma_finite_measure) borel_measurable_nn_integral_fst:
+ assumes f: "f \<in> borel_measurable (M1 \<Otimes>\<^sub>M M)"
shows "(\<lambda>x. \<integral>\<^sup>+ y. f (x, y) \<partial>M) \<in> borel_measurable M1"
using f proof induct
case (cong u v)
@@ -547,8 +545,8 @@
nn_integral_monotone_convergence_SUP incseq_def le_fun_def
cong: measurable_cong)
-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"
+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>N (M1 \<Otimes>\<^sub>M M) f" (is "?I f = _")
using f proof induct
case (cong u v)
@@ -557,26 +555,16 @@
with cong show ?case
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
+ nn_integral_monotone_convergence_SUP measurable_compose_Pair1
+ borel_measurable_nn_integral_fst nn_integral_mono incseq_def le_fun_def
cong: nn_integral_cong)
-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>N (M1 \<Otimes>\<^sub>M M) f"
- using f
- 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_nn_integral[measurable (raw)]:
"case_prod 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_nn_integral_fst'[of "\<lambda>x. max 0 (case_prod f x)" N]
- by (simp add: nn_integral_max_0)
+ using borel_measurable_nn_integral_fst[of "case_prod f" N] by simp
lemma (in pair_sigma_finite) nn_integral_snd:
- assumes f: "f \<in> borel_measurable (M1 \<Otimes>\<^sub>M M2)"
+ assumes f[measurable]: "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>N (M1 \<Otimes>\<^sub>M M2) f"
proof -
note measurable_pair_swap[OF f]
@@ -584,8 +572,7 @@
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>N (M1 \<Otimes>\<^sub>M M2) f"
- by (subst distr_pair_swap)
- (auto simp: nn_integral_distr[OF measurable_pair_swap' f] intro!: nn_integral_cong)
+ by (subst distr_pair_swap) (auto simp add: nn_integral_distr intro!: nn_integral_cong)
finally show ?thesis .
qed
@@ -610,13 +597,13 @@
have [simp]: "snd \<in> X \<times> Y \<rightarrow> Y" "fst \<in> X \<times> Y \<rightarrow> X"
by auto
let ?XY = "{{fst -` a \<inter> X \<times> Y | a. a \<in> A}, {snd -` b \<inter> X \<times> Y | b. b \<in> B}}"
- have "sets ?P =
+ have "sets ?P =
sets (\<Squnion>\<^sub>\<sigma> xy\<in>?XY. sigma (X \<times> Y) xy)"
by (simp add: vimage_algebra_sigma sets_pair_eq_sets_fst_snd A B)
also have "\<dots> = sets (sigma (X \<times> Y) (\<Union>?XY))"
by (intro Sup_sigma_sigma arg_cong[where f=sets]) auto
also have "\<dots> = sets ?S"
- proof (intro arg_cong[where f=sets] sigma_eqI sigma_sets_eqI)
+ proof (intro arg_cong[where f=sets] sigma_eqI sigma_sets_eqI)
show "\<Union>?XY \<subseteq> Pow (X \<times> Y)" "{a \<times> b |a b. a \<in> A \<and> b \<in> B} \<subseteq> Pow (X \<times> Y)"
using A B by auto
next
@@ -710,20 +697,17 @@
with A B have fin_Pair: "\<And>x. finite (Pair x -` X)"
by (intro finite_subset[OF _ B]) auto
have fin_X: "finite X" using X_subset by (rule finite_subset) (auto simp: A B)
+ have pos_card: "(0::ennreal) < of_nat (card (Pair x -` X)) \<longleftrightarrow> Pair x -` X \<noteq> {}" for x
+ by (auto simp: card_eq_0_iff fin_Pair) blast
+
show "emeasure ?P X = emeasure ?C X"
+ using X_subset A fin_Pair fin_X
apply (subst B.emeasure_pair_measure_alt[OF X])
apply (subst emeasure_count_space)
- using X_subset apply auto []
- apply (simp add: fin_Pair emeasure_count_space X_subset fin_X)
- apply (subst nn_integral_count_space)
- using A apply simp
- apply (simp del: of_nat_setsum add: of_nat_setsum[symmetric])
- apply (subst card_gt_0_iff)
- apply (simp add: fin_Pair)
- apply (subst card_SigmaI[symmetric])
- using A apply simp
- using fin_Pair apply simp
- using X_subset apply (auto intro!: arg_cong[where f=card])
+ apply (auto simp add: emeasure_count_space nn_integral_count_space
+ pos_card of_nat_setsum[symmetric] card_SigmaI[symmetric]
+ simp del: of_nat_setsum card_SigmaI
+ intro!: arg_cong[where f=card])
done
qed
@@ -732,16 +716,15 @@
assumes A: "A \<in> sets (count_space UNIV \<Otimes>\<^sub>M M)" (is "A \<in> sets (?A \<Otimes>\<^sub>M ?B)")
shows "emeasure (?A \<Otimes>\<^sub>M ?B) A = (\<integral>\<^sup>+ x. \<integral>\<^sup>+ y. indicator A (x, y) \<partial>?B \<partial>?A)"
by (rule emeasure_measure_of[OF pair_measure_def])
- (auto simp: countably_additive_def positive_def suminf_indicator nn_integral_nonneg A
+ (auto simp: countably_additive_def positive_def suminf_indicator A
nn_integral_suminf[symmetric] dest: sets.sets_into_space)
lemma emeasure_prod_count_space_single[simp]: "emeasure (count_space UNIV \<Otimes>\<^sub>M count_space UNIV) {x} = 1"
proof -
- have [simp]: "\<And>a b x y. indicator {(a, b)} (x, y) = (indicator {a} x * indicator {b} y::ereal)"
+ have [simp]: "\<And>a b x y. indicator {(a, b)} (x, y) = (indicator {a} x * indicator {b} y::ennreal)"
by (auto split: split_indicator)
show ?thesis
- by (cases x)
- (auto simp: emeasure_prod_count_space nn_integral_cmult sets_Pair nn_integral_max_0 one_ereal_def[symmetric])
+ by (cases x) (auto simp: emeasure_prod_count_space nn_integral_cmult sets_Pair)
qed
lemma emeasure_count_space_prod_eq:
@@ -771,17 +754,16 @@
also have "emeasure (?A \<Otimes>\<^sub>M ?B) C = emeasure (count_space UNIV) C"
using \<open>countable C\<close> by (rule *)
finally show ?thesis
- using \<open>infinite C\<close> \<open>infinite A\<close> by simp
+ using \<open>infinite C\<close> \<open>infinite A\<close> by (simp add: top_unique)
qed
qed
-lemma nn_intergal_count_space_prod_eq':
- assumes [simp]: "\<And>x. 0 \<le> f x"
- shows "nn_integral (count_space UNIV \<Otimes>\<^sub>M count_space UNIV) f = nn_integral (count_space UNIV) f"
+lemma nn_integral_count_space_prod_eq:
+ "nn_integral (count_space UNIV \<Otimes>\<^sub>M count_space UNIV) f = nn_integral (count_space UNIV) f"
(is "nn_integral ?P f = _")
proof cases
assume cntbl: "countable {x. f x \<noteq> 0}"
- have [simp]: "\<And>x. ereal (real (card ({x} \<inter> {x. f x \<noteq> 0}))) = indicator {x. f x \<noteq> 0} x"
+ have [simp]: "\<And>x. card ({x} \<inter> {x. f x \<noteq> 0}) = (indicator {x. f x \<noteq> 0} x::ennreal)"
by (auto split: split_indicator)
have [measurable]: "\<And>y. (\<lambda>x. indicator {y} x) \<in> borel_measurable ?P"
by (rule measurable_discrete_difference[of "\<lambda>x. 0" _ borel "{y}" "\<lambda>x. indicator {y} x" for y])
@@ -799,9 +781,9 @@
by (auto simp add: nn_integral_count_space_indicator intro!: nn_integral_cong split: split_indicator)
next
{ fix x assume "f x \<noteq> 0"
- with \<open>0 \<le> f x\<close> have "(\<exists>r. 0 < r \<and> f x = ereal r) \<or> f x = \<infinity>"
- by (cases "f x") (auto simp: less_le)
- then have "\<exists>n. ereal (1 / real (Suc n)) \<le> f x"
+ then have "(\<exists>r\<ge>0. 0 < r \<and> f x = ennreal r) \<or> f x = \<infinity>"
+ by (cases "f x" rule: ennreal_cases) (auto simp: less_le)
+ then have "\<exists>n. ennreal (1 / real (Suc n)) \<le> f x"
by (auto elim!: nat_approx_posE intro!: less_imp_le) }
note * = this
@@ -816,25 +798,21 @@
have [measurable]: "C \<in> sets ?P"
using sets.countable[OF _ \<open>countable C\<close>, of ?P] by (auto simp: sets_Pair)
- have "(\<integral>\<^sup>+x. ereal (1/Suc n) * indicator C x \<partial>?P) \<le> nn_integral ?P f"
+ have "(\<integral>\<^sup>+x. ennreal (1/Suc n) * indicator C x \<partial>?P) \<le> nn_integral ?P f"
using C by (intro nn_integral_mono) (auto split: split_indicator simp: zero_ereal_def[symmetric])
- moreover have "(\<integral>\<^sup>+x. ereal (1/Suc n) * indicator C x \<partial>?P) = \<infinity>"
- using \<open>infinite C\<close> by (simp add: nn_integral_cmult emeasure_count_space_prod_eq)
- moreover have "(\<integral>\<^sup>+x. ereal (1/Suc n) * indicator C x \<partial>count_space UNIV) \<le> nn_integral (count_space UNIV) f"
+ moreover have "(\<integral>\<^sup>+x. ennreal (1/Suc n) * indicator C x \<partial>?P) = \<infinity>"
+ using \<open>infinite C\<close> by (simp add: nn_integral_cmult emeasure_count_space_prod_eq ennreal_mult_top)
+ moreover have "(\<integral>\<^sup>+x. ennreal (1/Suc n) * indicator C x \<partial>count_space UNIV) \<le> nn_integral (count_space UNIV) f"
using C by (intro nn_integral_mono) (auto split: split_indicator simp: zero_ereal_def[symmetric])
- moreover have "(\<integral>\<^sup>+x. ereal (1/Suc n) * indicator C x \<partial>count_space UNIV) = \<infinity>"
- using \<open>infinite C\<close> by (simp add: nn_integral_cmult)
+ moreover have "(\<integral>\<^sup>+x. ennreal (1/Suc n) * indicator C x \<partial>count_space UNIV) = \<infinity>"
+ using \<open>infinite C\<close> by (simp add: nn_integral_cmult ennreal_mult_top)
ultimately show ?thesis
- by simp
+ by (simp add: top_unique)
qed
-lemma nn_intergal_count_space_prod_eq:
- "nn_integral (count_space UNIV \<Otimes>\<^sub>M count_space UNIV) f = nn_integral (count_space UNIV) f"
- by (subst (1 2) nn_integral_max_0[symmetric]) (auto intro!: nn_intergal_count_space_prod_eq')
-
lemma pair_measure_density:
- assumes f: "f \<in> borel_measurable M1" "AE x in M1. 0 \<le> f x"
- assumes g: "g \<in> borel_measurable M2" "AE x in M2. 0 \<le> g x"
+ assumes f: "f \<in> borel_measurable M1"
+ assumes g: "g \<in> borel_measurable M2"
assumes "sigma_finite_measure M2" "sigma_finite_measure (density M2 g)"
shows "density M1 f \<Otimes>\<^sub>M density M2 g = density (M1 \<Otimes>\<^sub>M M2) (\<lambda>(x,y). f x * g y)" (is "?L = ?R")
proof (rule measure_eqI)
@@ -916,7 +894,7 @@
by simp
qed
qed
-
+
lemma sets_pair_countable:
assumes "countable S1" "countable S2"
assumes M: "sets M = Pow S1" and N: "sets N = Pow S2"
@@ -948,25 +926,22 @@
by (subst sets_pair_countable[OF assms]) auto
next
fix A B assume "A \<in> sets (count_space S1)" "B \<in> sets (count_space S2)"
- then show "emeasure (count_space S1) A * emeasure (count_space S2) B =
+ then show "emeasure (count_space S1) A * emeasure (count_space S2) B =
emeasure (count_space (S1 \<times> S2)) (A \<times> B)"
- by (subst (1 2 3) emeasure_count_space) (auto simp: finite_cartesian_product_iff)
+ by (subst (1 2 3) emeasure_count_space) (auto simp: finite_cartesian_product_iff ennreal_mult_top ennreal_top_mult)
qed
-lemma nn_integral_fst_count_space':
- assumes nonneg: "\<And>xy. 0 \<le> f xy"
- shows "(\<integral>\<^sup>+ x. \<integral>\<^sup>+ y. f (x, y) \<partial>count_space UNIV \<partial>count_space UNIV) = integral\<^sup>N (count_space UNIV) f"
+lemma nn_integral_fst_count_space:
+ "(\<integral>\<^sup>+ x. \<integral>\<^sup>+ y. f (x, y) \<partial>count_space UNIV \<partial>count_space UNIV) = integral\<^sup>N (count_space UNIV) f"
(is "?lhs = ?rhs")
proof(cases)
assume *: "countable {xy. f xy \<noteq> 0}"
let ?A = "fst ` {xy. f xy \<noteq> 0}"
let ?B = "snd ` {xy. f xy \<noteq> 0}"
from * have [simp]: "countable ?A" "countable ?B" by(rule countable_image)+
- from nonneg have f_neq_0: "\<And>xy. f xy \<noteq> 0 \<longleftrightarrow> f xy > 0"
- by(auto simp add: order.order_iff_strict)
have "?lhs = (\<integral>\<^sup>+ x. \<integral>\<^sup>+ y. f (x, y) \<partial>count_space UNIV \<partial>count_space ?A)"
by(rule nn_integral_count_space_eq)
- (auto simp add: f_neq_0 nn_integral_0_iff_AE AE_count_space not_le intro: rev_image_eqI)
+ (auto simp add: nn_integral_0_iff_AE AE_count_space not_le intro: rev_image_eqI)
also have "\<dots> = (\<integral>\<^sup>+ x. \<integral>\<^sup>+ y. f (x, y) \<partial>count_space ?B \<partial>count_space ?A)"
by(intro nn_integral_count_space_eq nn_integral_cong)(auto intro: rev_image_eqI)
also have "\<dots> = (\<integral>\<^sup>+ xy. f xy \<partial>count_space (?A \<times> ?B))"
@@ -977,9 +952,9 @@
finally show ?thesis .
next
{ fix xy assume "f xy \<noteq> 0"
- with \<open>0 \<le> f xy\<close> have "(\<exists>r. 0 < r \<and> f xy = ereal r) \<or> f xy = \<infinity>"
- by (cases "f xy") (auto simp: less_le)
- then have "\<exists>n. ereal (1 / real (Suc n)) \<le> f xy"
+ then have "(\<exists>r\<ge>0. 0 < r \<and> f xy = ennreal r) \<or> f xy = \<infinity>"
+ by (cases "f xy" rule: ennreal_cases) (auto simp: less_le)
+ then have "\<exists>n. ennreal (1 / real (Suc n)) \<le> f xy"
by (auto elim!: nat_approx_posE intro!: less_imp_le) }
note * = this
@@ -991,15 +966,15 @@
then obtain C where C: "C \<subseteq> {xy. 1/Suc n \<le> f xy}" and "countable C" "infinite C"
by (metis infinite_countable_subset')
- have "\<infinity> = (\<integral>\<^sup>+ xy. ereal (1 / Suc n) * indicator C xy \<partial>count_space UNIV)"
- using \<open>infinite C\<close> by(simp add: nn_integral_cmult)
+ have "\<infinity> = (\<integral>\<^sup>+ xy. ennreal (1 / Suc n) * indicator C xy \<partial>count_space UNIV)"
+ using \<open>infinite C\<close> by(simp add: nn_integral_cmult ennreal_mult_top)
also have "\<dots> \<le> ?rhs" using C
- by(intro nn_integral_mono)(auto split: split_indicator simp add: nonneg)
- finally have "?rhs = \<infinity>" by simp
+ by(intro nn_integral_mono)(auto split: split_indicator)
+ finally have "?rhs = \<infinity>" by (simp add: top_unique)
moreover have "?lhs = \<infinity>"
proof(cases "finite (fst ` C)")
case True
- then obtain x C' where x: "x \<in> fst ` C"
+ then obtain x C' where x: "x \<in> fst ` C"
and C': "C' = fst -` {x} \<inter> C"
and "infinite C'"
using \<open>infinite C\<close> by(auto elim!: inf_img_fin_domE')
@@ -1007,37 +982,33 @@
from C' \<open>infinite C'\<close> have "infinite (snd ` C')"
by(auto dest!: finite_imageD simp add: inj_on_def)
- then have "\<infinity> = (\<integral>\<^sup>+ y. ereal (1 / Suc n) * indicator (snd ` C') y \<partial>count_space UNIV)"
- by(simp add: nn_integral_cmult)
- also have "\<dots> = (\<integral>\<^sup>+ y. ereal (1 / Suc n) * indicator C' (x, y) \<partial>count_space UNIV)"
+ then have "\<infinity> = (\<integral>\<^sup>+ y. ennreal (1 / Suc n) * indicator (snd ` C') y \<partial>count_space UNIV)"
+ by(simp add: nn_integral_cmult ennreal_mult_top)
+ also have "\<dots> = (\<integral>\<^sup>+ y. ennreal (1 / Suc n) * indicator C' (x, y) \<partial>count_space UNIV)"
by(rule nn_integral_cong)(force split: split_indicator intro: rev_image_eqI simp add: C')
- also have "\<dots> = (\<integral>\<^sup>+ x'. (\<integral>\<^sup>+ y. ereal (1 / Suc n) * indicator C' (x, y) \<partial>count_space UNIV) * indicator {x} x' \<partial>count_space UNIV)"
- by(simp add: one_ereal_def[symmetric] nn_integral_nonneg max_def)
- also have "\<dots> \<le> (\<integral>\<^sup>+ x. \<integral>\<^sup>+ y. ereal (1 / Suc n) * indicator C' (x, y) \<partial>count_space UNIV \<partial>count_space UNIV)"
- by(rule nn_integral_mono)(simp split: split_indicator add: nn_integral_nonneg)
+ also have "\<dots> = (\<integral>\<^sup>+ x'. (\<integral>\<^sup>+ y. ennreal (1 / Suc n) * indicator C' (x, y) \<partial>count_space UNIV) * indicator {x} x' \<partial>count_space UNIV)"
+ by(simp add: one_ereal_def[symmetric])
+ also have "\<dots> \<le> (\<integral>\<^sup>+ x. \<integral>\<^sup>+ y. ennreal (1 / Suc n) * indicator C' (x, y) \<partial>count_space UNIV \<partial>count_space UNIV)"
+ by(rule nn_integral_mono)(simp split: split_indicator)
also have "\<dots> \<le> ?lhs" using **
- by(intro nn_integral_mono)(auto split: split_indicator simp add: nonneg)
- finally show ?thesis by simp
+ by(intro nn_integral_mono)(auto split: split_indicator)
+ finally show ?thesis by (simp add: top_unique)
next
case False
def C' \<equiv> "fst ` C"
- have "\<infinity> = \<integral>\<^sup>+ x. ereal (1 / Suc n) * indicator C' x \<partial>count_space UNIV"
- using C'_def False by(simp add: nn_integral_cmult)
- also have "\<dots> = \<integral>\<^sup>+ x. \<integral>\<^sup>+ y. ereal (1 / Suc n) * indicator C' x * indicator {SOME y. (x, y) \<in> C} y \<partial>count_space UNIV \<partial>count_space UNIV"
+ have "\<infinity> = \<integral>\<^sup>+ x. ennreal (1 / Suc n) * indicator C' x \<partial>count_space UNIV"
+ using C'_def False by(simp add: nn_integral_cmult ennreal_mult_top)
+ also have "\<dots> = \<integral>\<^sup>+ x. \<integral>\<^sup>+ y. ennreal (1 / Suc n) * indicator C' x * indicator {SOME y. (x, y) \<in> C} y \<partial>count_space UNIV \<partial>count_space UNIV"
by(auto simp add: one_ereal_def[symmetric] max_def intro: nn_integral_cong)
- also have "\<dots> \<le> \<integral>\<^sup>+ x. \<integral>\<^sup>+ y. ereal (1 / Suc n) * indicator C (x, y) \<partial>count_space UNIV \<partial>count_space UNIV"
+ also have "\<dots> \<le> \<integral>\<^sup>+ x. \<integral>\<^sup>+ y. ennreal (1 / Suc n) * indicator C (x, y) \<partial>count_space UNIV \<partial>count_space UNIV"
by(intro nn_integral_mono)(auto simp add: C'_def split: split_indicator intro: someI)
also have "\<dots> \<le> ?lhs" using C
- by(intro nn_integral_mono)(auto split: split_indicator simp add: nonneg)
- finally show ?thesis by simp
+ by(intro nn_integral_mono)(auto split: split_indicator)
+ finally show ?thesis by (simp add: top_unique)
qed
ultimately show ?thesis by simp
qed
-lemma nn_integral_fst_count_space:
- "(\<integral>\<^sup>+ x. \<integral>\<^sup>+ y. f (x, y) \<partial>count_space UNIV \<partial>count_space UNIV) = integral\<^sup>N (count_space UNIV) f"
-by(subst (2 3) nn_integral_max_0[symmetric])(rule nn_integral_fst_count_space', simp)
-
lemma nn_integral_snd_count_space:
"(\<integral>\<^sup>+ y. \<integral>\<^sup>+ x. f (x, y) \<partial>count_space UNIV \<partial>count_space UNIV) = integral\<^sup>N (count_space UNIV) f"
(is "?lhs = ?rhs")
@@ -1118,7 +1089,7 @@
interpret M: finite_measure M by fact
interpret N: finite_measure N by fact
show "emeasure (N \<Otimes>\<^sub>M M) (space (N \<Otimes>\<^sub>M M)) \<noteq> \<infinity>"
- by (auto simp: space_pair_measure M.emeasure_pair_measure_Times)
+ by (auto simp: space_pair_measure M.emeasure_pair_measure_Times ennreal_mult_eq_top_iff)
qed
end