# HG changeset patch # User Andreas Lochbihler # Date 1429013539 -7200 # Node ID 63124d48a2eeae7bc5e9a29d4b1e8b31cd7ba8f6 # Parent 81835db730e8ade7a41d89f4b565f53951b00947 add lemma about monotone convergence for countable integrals over arbitrary sequences diff -r 81835db730e8 -r 63124d48a2ee src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy --- a/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy Tue Apr 14 14:11:01 2015 +0200 +++ b/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy Tue Apr 14 14:12:19 2015 +0200 @@ -758,6 +758,9 @@ lemma nn_integral_le_0[simp]: "integral\<^sup>N M f \ 0 \ integral\<^sup>N M f = 0" using nn_integral_nonneg[of M f] by auto +lemma nn_integral_not_less_0 [simp]: "\ nn_integral M f < 0" +by(simp add: not_less nn_integral_nonneg) + lemma nn_integral_not_MInfty[simp]: "integral\<^sup>N M f \ -\" using nn_integral_nonneg[of M f] by auto @@ -1648,6 +1651,15 @@ subsection {* Integral under concrete measures *} +lemma nn_integral_empty: + assumes "space M = {}" + shows "nn_integral M f = 0" +proof - + have "(\\<^sup>+ x. f x \M) = (\\<^sup>+ x. 0 \M)" + by(rule nn_integral_cong)(simp add: assms) + thus ?thesis by simp +qed + subsubsection {* Distributions *} lemma nn_integral_distr': @@ -1854,6 +1866,143 @@ finally show "emeasure M A = emeasure N A" .. qed simp +lemma nn_integral_monotone_convergence_SUP_nat': + fixes f :: "'a \ nat \ ereal" + assumes chain: "Complete_Partial_Order.chain op \ (f ` Y)" + and nonempty: "Y \ {}" + and nonneg: "\i n. i \ Y \ f i n \ 0" + shows "(\\<^sup>+ x. (SUP i:Y. f i x) \count_space UNIV) = (SUP i:Y. (\\<^sup>+ x. f i x \count_space UNIV))" + (is "?lhs = ?rhs" is "integral\<^sup>N ?M _ = _") +proof (rule order_class.order.antisym) + show "?rhs \ ?lhs" + by (auto intro!: SUP_least SUP_upper nn_integral_mono) +next + have "\x. \g. incseq g \ range g \ (\i. f i x) ` Y \ (SUP i:Y. f i x) = (SUP i. g i)" + unfolding Sup_class.SUP_def by(rule Sup_countable_SUP[unfolded Sup_class.SUP_def])(simp add: nonempty) + then obtain g where incseq: "\x. incseq (g x)" + and range: "\x. range (g x) \ (\i. f i x) ` Y" + and sup: "\x. (SUP i:Y. f i x) = (SUP i. g x i)" by moura + from incseq have incseq': "incseq (\i x. g x i)" + by(blast intro: incseq_SucI le_funI dest: incseq_SucD) + + have "?lhs = \\<^sup>+ x. (SUP i. g x i) \?M" by(simp add: sup) + also have "\ = (SUP i. \\<^sup>+ x. g x i \?M)" using incseq' + by(rule nn_integral_monotone_convergence_SUP) simp + also have "\ \ (SUP i:Y. \\<^sup>+ x. f i x \?M)" + proof(rule SUP_least) + fix n + have "\x. \i. g x n = f i x \ i \ Y" using range by blast + then obtain I where I: "\x. g x n = f (I x) x" "\x. I x \ Y" by moura + + { fix x + from range[of x] obtain i where "i \ Y" "g x n = f i x" by auto + hence "g x n \ 0" using nonneg[of i x] by simp } + note nonneg_g = this + then have "(\\<^sup>+ x. g x n \count_space UNIV) = (\x. g x n)" + by(rule nn_integral_count_space_nat) + also have "\ = (SUP m. \x \ (SUP i:Y. \\<^sup>+ x. f i x \?M)" + proof(rule SUP_mono) + fix m + show "\m'\Y. (\x (\\<^sup>+ x. f m' x \?M)" + proof(cases "m > 0") + case False + thus ?thesis using nonempty by(auto simp add: nn_integral_nonneg) + next + case True + let ?Y = "I ` {.. f ` Y" using I by auto + with chain have chain': "Complete_Partial_Order.chain op \ (f ` ?Y)" by(rule chain_subset) + hence "Sup (f ` ?Y) \ f ` ?Y" + by(rule ccpo_class.in_chain_finite)(auto simp add: True lessThan_empty_iff) + then obtain m' where "m' < m" and m': "(SUP i:?Y. f i) = f (I m')" by auto + have "I m' \ Y" using I by blast + have "(\x (\x {.. \ (SUP i:?Y. f i) x" unfolding SUP_def Sup_fun_def image_image + using \x \ {.. by(rule Sup_upper[OF imageI]) + also have "\ = f (I m') x" unfolding m' by simp + finally show "g x n \ f (I m') x" . + qed + also have "\ \ (SUP m. (\x = (\x. f (I m') x)" + by(rule suminf_ereal_eq_SUP[symmetric])(simp add: nonneg \I m' \ Y\) + also have "\ = (\\<^sup>+ x. f (I m') x \?M)" + by(rule nn_integral_count_space_nat[symmetric])(simp add: nonneg \I m' \ Y\) + finally show ?thesis using \I m' \ Y\ by blast + qed + qed + finally show "(\\<^sup>+ x. g x n \count_space UNIV) \ \" . + qed + finally show "?lhs \ ?rhs" . +qed + +lemma nn_integral_monotone_convergence_SUP_nat: + fixes f :: "'a \ nat \ ereal" + assumes nonempty: "Y \ {}" + and chain: "Complete_Partial_Order.chain op \ (f ` Y)" + shows "(\\<^sup>+ x. (SUP i:Y. f i x) \count_space UNIV) = (SUP i:Y. (\\<^sup>+ x. f i x \count_space UNIV))" + (is "?lhs = ?rhs") +proof - + let ?f = "\i x. max 0 (f i x)" + have chain': "Complete_Partial_Order.chain op \ (?f ` Y)" + proof(rule chainI) + fix g h + assume "g \ ?f ` Y" "h \ ?f ` Y" + then obtain g' h' where gh: "g' \ Y" "h' \ Y" "g = ?f g'" "h = ?f h'" by blast + hence "f g' \ f ` Y" "f h' \ f ` Y" by blast+ + with chain have "f g' \ f h' \ f h' \ f g'" by(rule chainD) + thus "g \ h \ h \ g" + proof + assume "f g' \ f h'" + hence "g \ h" using gh order_trans by(auto simp add: le_fun_def max_def) + thus ?thesis .. + next + assume "f h' \ f g'" + hence "h \ g" using gh order_trans by(auto simp add: le_fun_def max_def) + thus ?thesis .. + qed + qed + have "?lhs = (\\<^sup>+ x. max 0 (SUP i:Y. f i x) \count_space UNIV)" + by(simp add: nn_integral_max_0) + also have "\ = (\\<^sup>+ x. (SUP i:Y. ?f i x) \count_space UNIV)" + proof(rule nn_integral_cong) + fix x + have "max 0 (SUP i:Y. f i x) \ (SUP i:Y. ?f i x)" + proof(cases "0 \ (SUP i:Y. f i x)") + case True + have "(SUP i:Y. f i x) \ (SUP i:Y. ?f i x)" by(rule SUP_mono)(auto intro: rev_bexI) + with True show ?thesis by simp + next + case False + have "0 \ (SUP i:Y. ?f i x)" using nonempty by(auto intro: SUP_upper2) + thus ?thesis using False by simp + qed + moreover have "\ \ max 0 (SUP i:Y. f i x)" + proof(cases "(SUP i:Y. f i x) \ 0") + case True + show ?thesis + by(rule SUP_least)(auto simp add: True max_def intro: SUP_upper) + next + case False + hence "(SUP i:Y. f i x) \ 0" by simp + hence less: "\i\Y. f i x \ 0" by(simp add: SUP_le_iff) + show ?thesis by(rule SUP_least)(auto simp add: max_def less intro: SUP_upper) + qed + ultimately show "\ = (SUP i:Y. ?f i x)" by(rule order.antisym) + qed + also have "\ = (SUP i:Y. (\\<^sup>+ x. ?f i x \count_space UNIV))" + using chain' nonempty by(rule nn_integral_monotone_convergence_SUP_nat') simp + also have "\ = ?rhs" by(simp add: nn_integral_max_0) + finally show ?thesis . +qed + subsubsection {* Measures with Restricted Space *} lemma simple_function_iff_borel_measurable: