--- a/src/HOL/Complete_Lattice.thy Mon Aug 23 19:35:57 2010 +0200
+++ b/src/HOL/Complete_Lattice.thy Tue Aug 24 14:41:37 2010 +0200
@@ -88,6 +88,26 @@
lemma le_Inf_iff: "b \<sqsubseteq> Inf A \<longleftrightarrow> (\<forall>a\<in>A. b \<sqsubseteq> a)"
by (auto intro: Inf_greatest dest: Inf_lower)
+lemma Sup_mono:
+ assumes "\<And>a. a \<in> A \<Longrightarrow> \<exists>b\<in>B. a \<le> b"
+ shows "Sup A \<le> Sup B"
+proof (rule Sup_least)
+ fix a assume "a \<in> A"
+ with assms obtain b where "b \<in> B" and "a \<le> b" by blast
+ from `b \<in> B` have "b \<le> Sup B" by (rule Sup_upper)
+ with `a \<le> b` show "a \<le> Sup B" by auto
+qed
+
+lemma Inf_mono:
+ assumes "\<And>b. b \<in> B \<Longrightarrow> \<exists>a\<in>A. a \<le> b"
+ shows "Inf A \<le> Inf B"
+proof (rule Inf_greatest)
+ fix b assume "b \<in> B"
+ with assms obtain a where "a \<in> A" and "a \<le> b" by blast
+ from `a \<in> A` have "Inf A \<le> a" by (rule Inf_lower)
+ with `a \<le> b` show "Inf A \<le> b" by auto
+qed
+
definition SUPR :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
"SUPR A f = \<Squnion> (f ` A)"
@@ -144,8 +164,25 @@
lemma INF_const[simp]: "A \<noteq> {} \<Longrightarrow> (INF i:A. M) = M"
by (auto intro: antisym INF_leI le_INFI)
+lemma SUP_mono:
+ "(\<And>n. n \<in> A \<Longrightarrow> \<exists>m\<in>B. f n \<le> g m) \<Longrightarrow> (SUP n:A. f n) \<le> (SUP n:B. g n)"
+ by (force intro!: Sup_mono simp: SUPR_def)
+
+lemma INF_mono:
+ "(\<And>m. m \<in> B \<Longrightarrow> \<exists>n\<in>A. f n \<le> g m) \<Longrightarrow> (INF n:A. f n) \<le> (INF n:B. g n)"
+ by (force intro!: Inf_mono simp: INFI_def)
+
end
+lemma less_Sup_iff:
+ fixes a :: "'a\<Colon>{complete_lattice,linorder}"
+ shows "a < Sup S \<longleftrightarrow> (\<exists>x\<in>S. a < x)"
+ unfolding not_le[symmetric] Sup_le_iff by auto
+
+lemma Inf_less_iff:
+ fixes a :: "'a\<Colon>{complete_lattice,linorder}"
+ shows "Inf S < a \<longleftrightarrow> (\<exists>x\<in>S. x < a)"
+ unfolding not_le[symmetric] le_Inf_iff by auto
subsection {* @{typ bool} and @{typ "_ \<Rightarrow> _"} as complete lattice *}
@@ -204,6 +241,18 @@
end
+lemma SUPR_fun_expand:
+ fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c\<Colon>{complete_lattice}"
+ shows "(SUP y:A. f y) = (\<lambda>x. SUP y:A. f y x)"
+ by (auto intro!: arg_cong[where f=Sup] ext[where 'a='b]
+ simp: SUPR_def Sup_fun_def)
+
+lemma INFI_fun_expand:
+ fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c\<Colon>{complete_lattice}"
+ shows "(INF y:A. f y) x = (INF y:A. f y x)"
+ by (auto intro!: arg_cong[where f=Inf] ext[where 'a='b]
+ simp: INFI_def Inf_fun_def)
+
lemma Inf_empty_fun:
"\<Sqinter>{} = (\<lambda>_. \<Sqinter>{})"
by (simp add: Inf_fun_def)
--- a/src/HOL/Orderings.thy Mon Aug 23 19:35:57 2010 +0200
+++ b/src/HOL/Orderings.thy Tue Aug 24 14:41:37 2010 +0200
@@ -1154,7 +1154,7 @@
have "\<And>y. P y \<Longrightarrow> x \<le> y"
proof (rule classical)
fix y
- assume "P y" and "\<not> x \<le> y"
+ assume "P y" and "\<not> x \<le> y"
with less have "P (LEAST a. P a)" and "(LEAST a. P a) \<le> y"
by (auto simp add: not_le)
with assm have "x < (LEAST a. P a)" and "(LEAST a. P a) \<le> y"
@@ -1181,13 +1181,25 @@
"\<exists>a. P a \<Longrightarrow> (\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> Q (Least P)"
by (blast intro: LeastI_ex)
+lemma LeastI2_wellorder:
+ assumes "P a"
+ and "\<And>a. \<lbrakk> P a; \<forall>b. P b \<longrightarrow> a \<le> b \<rbrakk> \<Longrightarrow> Q a"
+ shows "Q (Least P)"
+proof (rule LeastI2_order)
+ show "P (Least P)" using `P a` by (rule LeastI)
+next
+ fix y assume "P y" thus "Least P \<le> y" by (rule Least_le)
+next
+ fix x assume "P x" "\<forall>y. P y \<longrightarrow> x \<le> y" thus "Q x" by (rule assms(2))
+qed
+
lemma not_less_Least: "k < (LEAST x. P x) \<Longrightarrow> \<not> P k"
apply (simp (no_asm_use) add: not_le [symmetric])
apply (erule contrapos_nn)
apply (erule Least_le)
done
-end
+end
subsection {* Order on bool *}
--- a/src/HOL/Probability/Borel.thy Mon Aug 23 19:35:57 2010 +0200
+++ b/src/HOL/Probability/Borel.thy Tue Aug 24 14:41:37 2010 +0200
@@ -1238,7 +1238,7 @@
proof safe
fix a
have "{x\<in>space M. a < ?sup x} = (\<Union>i\<in>A. {x\<in>space M. a < f i x})"
- by (auto simp: less_Sup_iff SUPR_def[where 'a=pinfreal] SUPR_fun_expand[where 'b=pinfreal])
+ by (auto simp: less_Sup_iff SUPR_def[where 'a=pinfreal] SUPR_fun_expand[where 'c=pinfreal])
then show "{x\<in>space M. a < ?sup x} \<in> sets M"
using assms by auto
qed
--- a/src/HOL/Probability/Lebesgue_Integration.thy Mon Aug 23 19:35:57 2010 +0200
+++ b/src/HOL/Probability/Lebesgue_Integration.thy Tue Aug 24 14:41:37 2010 +0200
@@ -57,7 +57,7 @@
shows "f x = (\<Sum>y \<in> f ` space M. y * indicator (f -` {y} \<inter> space M) x)"
(is "?l = ?r")
proof -
- have "?r = (\<Sum>y \<in> f ` space M.
+ have "?r = (\<Sum>y \<in> f ` space M.
(if y = f x then y * indicator (f -` {y} \<inter> space M) x else 0))"
by (auto intro!: setsum_cong2)
also have "... = f x * indicator (f -` {f x} \<inter> space M) x"
@@ -222,19 +222,6 @@
by (simp add: if_distrib setsum_cases[OF `finite P`])
qed
-lemma LeastI2_wellorder:
- fixes a :: "_ :: wellorder"
- assumes "P a"
- and "\<And>a. \<lbrakk> P a; \<forall>b. P b \<longrightarrow> a \<le> b \<rbrakk> \<Longrightarrow> Q a"
- shows "Q (Least P)"
-proof (rule LeastI2_order)
- show "P (Least P)" using `P a` by (rule LeastI)
-next
- fix y assume "P y" thus "Least P \<le> y" by (rule Least_le)
-next
- fix x assume "P x" "\<forall>y. P y \<longrightarrow> x \<le> y" thus "Q x" by (rule assms(2))
-qed
-
lemma (in sigma_algebra) borel_measurable_implies_simple_function_sequence:
fixes u :: "'a \<Rightarrow> pinfreal"
assumes u: "u \<in> borel_measurable M"
@@ -399,7 +386,8 @@
let ?N = "max n (natfloor r + 1)"
have "u t < of_nat ?N" "n \<le> ?N"
using ge_natfloor_plus_one_imp_gt[of r n] preal
- by (auto simp: max_def real_Suc_natfloor)
+ using real_natfloor_add_one_gt
+ by (auto simp: max_def real_of_nat_Suc)
from lower[OF this(1)]
have "r < (real (f t ?N) + 1) / 2 ^ ?N" unfolding less_divide_eq
using preal by (auto simp add: power_le_zero_eq zero_le_mult_iff real_of_nat_Suc split: split_if_asm)
@@ -875,7 +863,7 @@
moreover
have "a * (SUP i. simple_integral (?uB i)) \<le> ?S"
unfolding pinfreal_SUP_cmult[symmetric]
- proof (safe intro!: SUP_mono)
+ proof (safe intro!: SUP_mono bexI)
fix i
have "a * simple_integral (?uB i) = simple_integral (\<lambda>x. a * ?uB i x)"
using B `simple_function u`
@@ -890,7 +878,7 @@
qed
finally show "a * simple_integral (?uB i) \<le> positive_integral (f i)"
by auto
- qed
+ qed simp
ultimately show "a * simple_integral u \<le> ?S" by simp
qed
@@ -1056,16 +1044,17 @@
by (auto intro!: borel_measurable_SUP borel_measurable_INF assms)
have "(\<lambda>n. INF m. u (m + n)) \<up> (SUP n. INF m. u (m + n))"
- proof (unfold isoton_def, safe)
- fix i show "(INF m. u (m + i)) \<le> (INF m. u (m + Suc i))"
- by (rule INF_mono[where N=Suc]) simp
- qed
+ proof (unfold isoton_def, safe intro!: INF_mono bexI)
+ fix i m show "u (Suc m + i) \<le> u (m + Suc i)" by simp
+ qed simp
from positive_integral_isoton[OF this] assms
have "positive_integral (SUP n. INF m. u (m + n)) =
(SUP n. positive_integral (INF m. u (m + n)))"
unfolding isoton_def by (simp add: borel_measurable_INF)
also have "\<dots> \<le> (SUP n. INF m. positive_integral (u (m + n)))"
- by (auto intro!: SUP_mono[where N="\<lambda>x. x"] INFI_bound positive_integral_mono INF_leI simp: INFI_fun_expand)
+ apply (rule SUP_mono)
+ apply (rule_tac x=n in bexI)
+ by (auto intro!: positive_integral_mono INFI_bound INF_leI exI simp: INFI_fun_expand)
finally show ?thesis .
qed
@@ -1123,10 +1112,10 @@
have "?I = (SUP i. positive_integral (\<lambda>x. min (of_nat i) (u x) * indicator N x))"
unfolding isoton_def using borel `N \<in> sets M` by (simp add: borel_measurable_indicator)
also have "\<dots> \<le> (SUP i. positive_integral (\<lambda>x. of_nat i * indicator N x))"
- proof (rule SUP_mono, rule positive_integral_mono)
+ proof (rule SUP_mono, rule bexI, rule positive_integral_mono)
fix x i show "min (of_nat i) (u x) * indicator N x \<le> of_nat i * indicator N x"
by (cases "x \<in> N") auto
- qed
+ qed simp
also have "\<dots> = 0"
using `N \<in> null_sets` by (simp add: positive_integral_cmult_indicator)
finally show ?thesis by simp
@@ -1967,46 +1956,37 @@
unfolding finite_measure_space_def finite_measure_space_axioms_def
using assms by simp
-lemma (in finite_measure_space) borel_measurable_finite[intro, simp]:
- fixes f :: "'a \<Rightarrow> real"
- shows "f \<in> borel_measurable M"
+lemma (in finite_measure_space) borel_measurable_finite[intro, simp]: "f \<in> borel_measurable M"
unfolding measurable_def sets_eq_Pow by auto
+lemma (in finite_measure_space) simple_function_finite: "simple_function f"
+ unfolding simple_function_def sets_eq_Pow using finite_space by auto
+
+lemma (in finite_measure_space) positive_integral_finite_eq_setsum:
+ "positive_integral f = (\<Sum>x \<in> space M. f x * \<mu> {x})"
+proof -
+ have *: "positive_integral f = positive_integral (\<lambda>x. \<Sum>y\<in>space M. f y * indicator {y} x)"
+ by (auto intro!: positive_integral_cong simp add: indicator_def if_distrib setsum_cases[OF finite_space])
+ show ?thesis unfolding * using borel_measurable_finite[of f]
+ by (simp add: positive_integral_setsum positive_integral_cmult_indicator sets_eq_Pow)
+qed
+
lemma (in finite_measure_space) integral_finite_singleton:
shows "integrable f"
and "integral f = (\<Sum>x \<in> space M. f x * real (\<mu> {x}))" (is ?I)
proof -
- have 1: "f \<in> borel_measurable M"
- unfolding measurable_def sets_eq_Pow by auto
-
- have 2: "finite (f`space M)" using finite_space by simp
-
- have 3: "\<And>x. x \<noteq> 0 \<Longrightarrow> \<mu> (f -` {x} \<inter> space M) \<noteq> \<omega>"
- using finite_measure[unfolded sets_eq_Pow] by simp
-
- show "integrable f"
- by (rule integral_on_finite(1)[OF 1 2 3]) simp
+ have [simp]:
+ "positive_integral (\<lambda>x. Real (f x)) = (\<Sum>x \<in> space M. Real (f x) * \<mu> {x})"
+ "positive_integral (\<lambda>x. Real (- f x)) = (\<Sum>x \<in> space M. Real (- f x) * \<mu> {x})"
+ unfolding positive_integral_finite_eq_setsum by auto
- { fix r let ?x = "f -` {r} \<inter> space M"
- have "?x \<subseteq> space M" by auto
- with finite_space sets_eq_Pow finite_single_measure
- have "real (\<mu> ?x) = (\<Sum>i \<in> ?x. real (\<mu> {i}))"
- using real_measure_setsum_singleton[of ?x] by auto }
- note measure_eq_setsum = this
+ show "integrable f" using finite_space finite_measure
+ by (simp add: setsum_\<omega> integrable_def sets_eq_Pow)
- have "integral f = (\<Sum>r\<in>f`space M. r * real (\<mu> (f -` {r} \<inter> space M)))"
- by (rule integral_on_finite(2)[OF 1 2 3]) simp
- also have "\<dots> = (\<Sum>x \<in> space M. f x * real (\<mu> {x}))"
- unfolding measure_eq_setsum setsum_right_distrib
- apply (subst setsum_Sigma)
- apply (simp add: finite_space)
- apply (simp add: finite_space)
- proof (rule setsum_reindex_cong[symmetric])
- fix a assume "a \<in> Sigma (f ` space M) (\<lambda>x. f -` {x} \<inter> space M)"
- thus "(\<lambda>(x, y). x * real (\<mu> {y})) a = f (snd a) * real (\<mu> {snd a})"
- by auto
- qed (auto intro!: image_eqI inj_onI)
- finally show ?I .
+ show ?I using finite_measure
+ apply (simp add: integral_def sets_eq_Pow real_of_pinfreal_setsum[symmetric]
+ real_of_pinfreal_mult[symmetric] setsum_subtractf[symmetric])
+ by (rule setsum_cong) (simp_all split: split_if)
qed
end
--- a/src/HOL/Probability/Positive_Infinite_Real.thy Mon Aug 23 19:35:57 2010 +0200
+++ b/src/HOL/Probability/Positive_Infinite_Real.thy Tue Aug 24 14:41:37 2010 +0200
@@ -6,53 +6,20 @@
imports Complex_Main Nat_Bijection Multivariate_Analysis
begin
-lemma less_Sup_iff:
- fixes a :: "'x\<Colon>{complete_lattice,linorder}"
- shows "a < Sup S \<longleftrightarrow> (\<exists> x \<in> S. a < x)"
- unfolding not_le[symmetric] Sup_le_iff by auto
-
-lemma Inf_less_iff:
- fixes a :: "'x\<Colon>{complete_lattice,linorder}"
- shows "Inf S < a \<longleftrightarrow> (\<exists> x \<in> S. x < a)"
- unfolding not_le[symmetric] le_Inf_iff by auto
-
-lemma SUPR_fun_expand: "(SUP y:A. f y) = (\<lambda>x. SUP y:A. f y x)"
- unfolding SUPR_def expand_fun_eq Sup_fun_def
- by (auto intro!: arg_cong[where f=Sup])
-
-lemma real_Suc_natfloor: "r < real (Suc (natfloor r))"
-proof cases
- assume "0 \<le> r"
- from floor_correct[of r]
- have "r < real (\<lfloor>r\<rfloor> + 1)" by auto
- also have "\<dots> = real (Suc (natfloor r))"
- using `0 \<le> r` by (auto simp: real_of_nat_Suc natfloor_def)
- finally show ?thesis .
-next
- assume "\<not> 0 \<le> r"
- hence "r < 0" by auto
- also have "0 < real (Suc (natfloor r))" by auto
- finally show ?thesis .
+lemma (in complete_lattice) Sup_start:
+ assumes *: "\<And>x. f x \<le> f 0"
+ shows "(SUP n. f n) = f 0"
+proof (rule antisym)
+ show "f 0 \<le> (SUP n. f n)" by (rule le_SUPI) auto
+ show "(SUP n. f n) \<le> f 0" by (rule SUP_leI[OF *])
qed
-lemma (in complete_lattice) Sup_mono:
- assumes "\<And>a. a \<in> A \<Longrightarrow> \<exists>b\<in>B. a \<le> b"
- shows "Sup A \<le> Sup B"
-proof (rule Sup_least)
- fix a assume "a \<in> A"
- with assms obtain b where "b \<in> B" and "a \<le> b" by auto
- hence "b \<le> Sup B" by (auto intro: Sup_upper)
- with `a \<le> b` show "a \<le> Sup B" by auto
-qed
-
-lemma (in complete_lattice) Inf_mono:
- assumes "\<And>b. b \<in> B \<Longrightarrow> \<exists>a\<in>A. a \<le> b"
- shows "Inf A \<le> Inf B"
-proof (rule Inf_greatest)
- fix b assume "b \<in> B"
- with assms obtain a where "a \<in> A" and "a \<le> b" by auto
- hence "Inf A \<le> a" by (auto intro: Inf_lower)
- with `a \<le> b` show "Inf A \<le> b" by auto
+lemma (in complete_lattice) Inf_start:
+ assumes *: "\<And>x. f 0 \<le> f x"
+ shows "(INF n. f n) = f 0"
+proof (rule antisym)
+ show "(INF n. f n) \<le> f 0" by (rule INF_leI) simp
+ show "f 0 \<le> (INF n. f n)" by (rule le_INFI[OF *])
qed
lemma (in complete_lattice) Sup_mono_offset:
@@ -77,12 +44,18 @@
apply (rule Sup_mono_offset)
by (auto intro!: order.lift_Suc_mono_le[of "op \<le>" "op <" f, OF _ *]) default
-lemma (in complete_lattice) Inf_start:
- assumes *: "\<And>x. f 0 \<le> f x"
- shows "(INF n. f n) = f 0"
+lemma (in complete_lattice) Inf_mono_offset:
+ fixes f :: "'b :: {ordered_ab_semigroup_add,monoid_add} \<Rightarrow> 'a"
+ assumes *: "\<And>x y. x \<le> y \<Longrightarrow> f y \<le> f x" and "0 \<le> k"
+ shows "(INF n . f (k + n)) = (INF n. f n)"
proof (rule antisym)
- show "(INF n. f n) \<le> f 0" by (rule INF_leI) simp
- show "f 0 \<le> (INF n. f n)" by (rule le_INFI[OF *])
+ show "(INF n. f n) \<le> (INF n. f (k + n))"
+ by (auto intro!: Inf_mono simp: INFI_def)
+ { fix n :: 'b
+ have "0 + n \<le> k + n" using `0 \<le> k` by (rule add_right_mono)
+ with * have "f (k + n) \<le> f n" by simp }
+ thus "(INF n. f (k + n)) \<le> (INF n. f n)"
+ by (auto intro!: Inf_mono exI simp: INFI_def)
qed
lemma (in complete_lattice) isotone_converge:
@@ -99,28 +72,6 @@
ultimately show ?thesis by simp
qed
-lemma (in complete_lattice) Inf_mono_offset:
- fixes f :: "'b :: {ordered_ab_semigroup_add,monoid_add} \<Rightarrow> 'a"
- assumes *: "\<And>x y. x \<le> y \<Longrightarrow> f y \<le> f x" and "0 \<le> k"
- shows "(INF n . f (k + n)) = (INF n. f n)"
-proof (rule antisym)
- show "(INF n. f n) \<le> (INF n. f (k + n))"
- by (auto intro!: Inf_mono simp: INFI_def)
- { fix n :: 'b
- have "0 + n \<le> k + n" using `0 \<le> k` by (rule add_right_mono)
- with * have "f (k + n) \<le> f n" by simp }
- thus "(INF n. f (k + n)) \<le> (INF n. f n)"
- by (auto intro!: Inf_mono exI simp: INFI_def)
-qed
-
-lemma (in complete_lattice) Sup_start:
- assumes *: "\<And>x. f x \<le> f 0"
- shows "(SUP n. f n) = f 0"
-proof (rule antisym)
- show "f 0 \<le> (SUP n. f n)" by (rule le_SUPI) auto
- show "(SUP n. f n) \<le> f 0" by (rule SUP_leI[OF *])
-qed
-
lemma (in complete_lattice) antitone_converges:
fixes f :: "nat \<Rightarrow> 'a" assumes "\<And>x y. x \<le> y \<Longrightarrow> f y \<le> f x"
shows "(INF n. SUP m. f (n + m)) = (SUP n. INF m. f (n + m))"
@@ -1657,15 +1608,6 @@
"1 \<le> Real p \<longleftrightarrow> 1 \<le> p"
by (simp_all add: one_pinfreal_def del: Real_1)
-lemma SUP_mono:
- assumes "\<And>n. f n \<le> g (N n)"
- shows "(SUP n. f n) \<le> (SUP n. g n)"
-proof (safe intro!: SUPR_bound)
- fix n note assms[of n]
- also have "g (N n) \<le> (SUP n. g n)" by (auto intro!: le_SUPI)
- finally show "f n \<le> (SUP n. g n)" .
-qed
-
lemma isoton_Sup:
assumes "f \<up> u"
shows "f i \<le> u"
@@ -2563,20 +2505,6 @@
shows "x \<le> (INF n. f n)"
using assms by (simp add: INFI_def le_Inf_iff)
-lemma INF_mono:
- assumes "\<And>n. f (N n) \<le> g n"
- shows "(INF n. f n) \<le> (INF n. g n)"
-proof (safe intro!: INFI_bound)
- fix n
- have "(INF n. f n) \<le> f (N n)" by (auto intro!: INF_leI)
- also note assms[of n]
- finally show "(INF n. f n) \<le> g n" .
-qed
-
-lemma INFI_fun_expand: "(INF y:A. f y) = (\<lambda>x. INF y:A. f y x)"
- unfolding INFI_def expand_fun_eq Inf_fun_def
- by (auto intro!: arg_cong[where f=Inf])
-
lemma LIMSEQ_imp_lim_INF:
assumes pos: "\<And>i. 0 \<le> X i" and lim: "X ----> x"
shows "(SUP n. INF m. Real (X (n + m))) = Real x"
@@ -2596,11 +2524,11 @@
proof safe
fix x y :: nat assume "x \<le> y"
have "Real (r x) \<le> Real (r y)" unfolding r(1)[symmetric] using pos
- proof (safe intro!: INF_mono)
+ proof (safe intro!: INF_mono bexI)
fix m have "x + (m + y - x) = y + m"
using `x \<le> y` by auto
thus "Real (X (x + (m + y - x))) \<le> Real (X (y + m))" by simp
- qed
+ qed simp
thus "r x \<le> r y" using r by auto
qed
show "\<And>n. 0 \<le> r n" by fact
@@ -2646,7 +2574,6 @@
qed
qed
-
lemma real_of_pinfreal_strict_mono_iff:
"real a < real b \<longleftrightarrow> (b \<noteq> \<omega> \<and> ((a = \<omega> \<and> 0 < b) \<or> (a < b)))"
proof (cases a)
--- a/src/HOL/Probability/Product_Measure.thy Mon Aug 23 19:35:57 2010 +0200
+++ b/src/HOL/Probability/Product_Measure.thy Tue Aug 24 14:41:37 2010 +0200
@@ -87,22 +87,6 @@
shows "sigma_finite_measure (prod_measure_space M N) (prod_measure M \<mu> N \<nu>)"
oops
-lemma (in finite_measure_space) simple_function_finite:
- "simple_function f"
- unfolding simple_function_def sets_eq_Pow using finite_space by auto
-
-lemma (in finite_measure_space) borel_measurable_finite[intro, simp]: "f \<in> borel_measurable M"
- unfolding measurable_def sets_eq_Pow by auto
-
-lemma (in finite_measure_space) positive_integral_finite_eq_setsum:
- "positive_integral f = (\<Sum>x \<in> space M. f x * \<mu> {x})"
-proof -
- have *: "positive_integral f = positive_integral (\<lambda>x. \<Sum>y\<in>space M. f y * indicator {y} x)"
- by (auto intro!: positive_integral_cong simp add: indicator_def if_distrib setsum_cases[OF finite_space])
- show ?thesis unfolding * using borel_measurable_finite[of f]
- by (simp add: positive_integral_setsum positive_integral_cmult_indicator sets_eq_Pow)
-qed
-
lemma (in finite_measure_space) finite_prod_measure_times:
assumes "finite_measure_space N \<nu>"
and "A1 \<in> sets M" "A2 \<in> sets N"